I. Стоящая отдельно исходная константа есть ппф.
10iii. Если G и D суть ппф, то [G É D] есть ппф.
Для того чтобы завершить определение ппф (= правильно построенных формул) и исчисления Р1, мы добавляем, что формула является ппф тогда и только тогда, когда это следует из приведенных трех правил построения. Другими словами, класс ппф исчисления Р1 — это наименьший класс формул, содержащий все формулы, описанные в 10i и 10ii, и замкнутый относительно правила 10iii. Если формула является ппф и состоит из более чем одного символа, то ее единственным образом можно представить в виде [А É В]. При этом А является антецедентом, В — консеквентом, а знак É между А и В — главным знаком импликации.
Правилами вывода являются следующие два:
*100. Из [ A É В ] и А следует В (правило модус поненс)
*101. Если b — переменная, то из А следует S b/B A | (правило подстановки)
При задании *101 вводится знак „ S | " для обозначения преобразования (операции подстановки) ппф А в ппф S b/B A |, которая является результатом замещения каждого вхождения переменной b в А ппф В.
Аксиомами системы P1 являются три следующие:
+102. [р É [q É p].
+103. [[s É [p É q]] É [[s É p] É [s É q]]].
+104. [[[p É f] É f] É p]
Первая из этих аксиом (+102) или ее эквивалент в других формулировках пропозиционального исчисления (независимо от того, является ли он аксиомой) называется законом утверждения консеквента. Аналогично вторая аксиома называется законом самодистрибутивности (материальной) импликации. Наконец, третья аксиома носит название закона двойного отрицания.
Доказательством в системе P1 называется конечная последовательность, состоящая из одной или нескольких правильно построенных формул, из которых каждая либо является одной из трех аксиом, либо (непосредственно) выводится из двух предыдущих ппф последовательности по модус поненс, либо (непосредственно) выводится из одной предыдущей ппф последовательности посредством подстановки. Доказательство называется доказательством последней ппф последовательности, и ппф называется теоремой, если она имеет доказательство.
~~~~~~~~~~~~~~
Для удобства изложения мы будем применять некоторые сокращения ппф системы P1.
В частности, можно опускать внешние скобки у ппф, так что мы будем, например, писать в качестве сокращения ппф +102. Мы будем опускать также и другие скобки, уславливаясь при восстановлении их производить группировку влево. Так, р É f É f É р является сокращением для +104, в то время как р É [f É f] É р есть сокращение ппф [[р É [f É f]] É р].
В тех же случаях, когда мы, опуская пару скобок, вставляем в выражение большую точку «<» мы уславливаемся, что при восстановлении скобок (вместо группировки влево) большая точка должна быть заменена левой скобкой [, а правая скобка ] должна быть помещена непосредственно перед ближайшей правой скобкой, которая сама стоит правее заменяемой большой точки, но не имеет правее этой большой точки парной с нею левой скобки; если же правее большой точки нужной правой скобки нет, то восстанавливаемая правая скобка должна быть помещена в конце выражения. Так, например, мы будем использовать выражение p É < q É p в качестве сокращения для +102 и выражение [p É < f É f] É p в качестве другого сокращения ппф, для которой мы выше указали сокращение р É [f É f] É р.
~~~~~~~~~~~~~~~~~~~~~
В качестве первого примера теоремы исчисления P1 мы докажем +120. р É р [Закон рефлексивности импликации]. Ее доказательством является следующая последовательность 9-ти формул:
s É [p É q] É < s É p É < s É q
s É [r É q] É < s É r É < s É q
s É [r É p] É < s É r É < s É p
p É [r É p] É < p É r É < p É p
p É [q É p] É < p É q É < p É p
p É < q É p
p É q É < p É p
p É [q É p] É < p É p
p É p
Так как имеются эффективные методы проверки, то теоретически достаточно просто выписать само доказательство без дополнительных пояснений, как это и сделано выше. Однако в помощь читателю мы дадим ниже подробное разъяснение. Первая из этих девяти ппф есть +103. Следующую ппф мы получаем из первой посредством *101, подставляя r вместо р. Далее, третья ппф получена из второй подстановкой р вместо q. Четвертая получена из третьей подстановкой р вместо s. Пятая получена из четвертой подстановкой q вместо r. Шестая ппф есть +102. Седьмая получается по модус поненс из пятой как большой посылки и из шестой как малой посылки. Затем восьмая ппф получается из седьмой опять посредством применения *101, причем q É p подставляется вместо q. Наконец, p É p получается по модус поненс из восьмой и шестой ппф как большой и малой посылок соответственно.
Удобно считать, что пятая ппф доказательства получена из первой посредством одновременной подстановки, а именно подстановки р, q, р вместо s, p, q соответственно. Мы обобщим обозначение для подстановки следующим образом: S b1/B1 b2/B2 …bn/Bn A | будет формулой, которая получается одновременной подстановкой формул В1, В2,..., Вn вместо переменных b1, b2,..., bn в формулу А. Подстановка должна быть проведена для всех вхождений переменных b1, b2,..., bn в А. Требуется чтобы все b1, b2,..., bn были различны (в противном — результат подстановки не существует), но не требуется, чтобы все из b1, b2,..., bn действительно входили в формулу А.
Упражнения. (доказательства должны быть проведены так же, как это сделано выше)
12.3. Докажите q É r É < p É q É < p É r как теорему в Р1. Используйте эту теорему для того, чтобы дать доказательства теорем +122 и +l23, которые были бы короче приведенных выше в том смысле, что они могут быть короче изложены.
12.4. Воспользуйтесь результатом упражнения 12.3 для доказательства закона транзитивности (материальной) импликации p É q É < q É r É < p É r как теоремы системы Р1. (Один из методов состоит в применении закона самодистрибутивности к результату упражнения 12.3 и в использовании затем p É q É < q É r É < p É q)
12.5. Докажите p É q É p É < p É f É p как теорему исчисления Р1. (Используйте +123, 12.4.)
12.6. Докажите как теорему в Р1 закон Пирса: p É q É p É p. (Примените закон самодистрибутивности к p É f É < p É f и используйте результат из 12.5)
12.7. Пусть Рw — логистическая система, которая имеет те же исходные символы, правила построения и правила вывода, что и Р1 и аксиомами которой являются (1) закон транзитивности импликации, (2) закон Пирса, (3) + 102 (4) + 122. Вначале докажите последовательно как теоремы в Рw приведенные ниже формулы, а затем покажите, что Рw и Р1 эквивалентны в том смысле, что они содержат одни и те же теоремы:
12.7.1. [p É < p É q] É < p É q
12.7.2. p É < p É q É q (закон утверждения)
12.7.3. [p É < q É r] É < q É < p É r (закон коммутации)
12.7.4. q É r É < p É q É < p É r (= 12.3)
12.7.5. s É [p É q] É < s É p É < s É q (= +103)
12.7.6. p É f É f É p (= +104)
Проведите доказательство таким образом, чтобы не использовать четвертую аксиому, +122, нигде, кроме доказательства последней теоремы.
12.8. Докажите как теоремы в Рw не используя при этом четвертую аксиому, +122:
12.8.1. q É r É r É < p É q É r É r
12.8.2. r É < p É < q É r
12.8.3. p É r É r É < q É r É < p É q É r
12.8.4. q É r É < p É q É r É r