p É [q É p] É < p É q É < 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 соответственно. Из доказательства видно в деталях, как результат такой одновременной подстановки может быть получен посредством четырех последовательных простых подстановок.

Мы обобщим обозначение для подстановки, введенное в § 10, следующим образом:

S ^b¹/_B₁^b²/_B₂ …^bⁿ/_B_n A |

будет формулой, которая получается одновременной подстановкой формул В_1, В₂, ..., В_n вместо переменных b_1, b₂, ..., b_n в формулу А. Подстановка должна быть проведена для всех вхождений переменных b_1, b₂, ..., b_n в А. Требуется чтобы все b_1, b₂, ..., b_n были различны (в противном случае результат подстановки не существует), но, конечно, не требуется, чтобы все или хотя бы некоторые из b_1, b₂, ..., b_n действительно входили в формулу А. Результат одновременной подстановки

S ^b¹/_B₁^b²/_B₂ …^bⁿ/_B_n A |

где b_1, b₂, ..., b_n — отличные друг от друга переменные, всегда может быть получен с помощью 2n последовательных простых подстановок, т. е. с помощью 2n последовательных применений *101. В некоторых случаях это возможно с меньшим чем 2n числом подстановок, но во всяком случае с помощью 2n подстановок это всегда можно сделать следующим образом. Пусть с, с₂, ..., с_n суть п первых в алфавитном порядке переменных, которые не входят ни в одну из пп-формул В_1,В₂, ..., В_n А (такие всегда найдутся вследствие бесконечности числа переменных). Тогда мы подставляем в А последовательно с₁ вместо b₁ с₂ вместо b₂, ..., с_n вместо b_n, B₁ вместо с₁, В₂ вместо с₂, В_nвместо с_n.

= пропуск правки =

стр. 78 — 79: там доказывается метатеорема *121 о возможности одновременной подстановки

Мы будем использовать знак h в качестве синтаксического обозначения для выражения того, что некоторая ппф есть теорема (системы р! или, в дальнейшем, другой логистической системы). Таким образом, „hpZ5p" является сокращением для „рЭр есть теорема", и т. д. (Ср. примечание 65. )

С помощью этого обозначения мы можем сформулировать следующую метатеорему, доказательство которой мы только что наметили:

Мы будем использовать эту метатеорему в качестве производного правила вывода, т. е. в доказательствах будем непосредственно переходить от А к не приводя деталей промежуточных шагов, а просто ссылаясь на *121 (или на „одновременную подстановку", или на „подстановку" ).

Такое использование производных правил — так же как и использование определений и иных сокращений (§ 11) — оправдывается тем, что они являются только приемами изложения и от них в принципе можно было бы отказаться. В этом отношении, однако, существенно, чтобы доказательство производного правила вывода было эффективным (ср. §§ 07, 08) в смысле наличия эффективного метода, всегда позволяющего из данного доказательства посылок производного правила получить доказательство его заключения. Ибо мы должны быть уверены в том, что всякий раз, когда подвергается сомнению некоторое доказательство, проведенное с помощью производных правил вывода, мы можем отвести это сомнение, приведя полное доказательство. Иными словами, мы заботимся о наличии механически осуществляемой процедуры, позволяющей, если это требуется, восстановить несокращенное доказательство. На этом основании мы просим читателя всегда представлять себе выписанными полностью (а в случае необходимости самому выписывать полностью) те доказательства конкретных теорем логистических систем, которые мы будем в действительности давать с использованием производных правил.

Доказательство метатеоремы *121 является, конечно, эффективным, как читатель легко заметит, просмотрев его заново.

Используя *121 как производное правило, с помощью некоторых других очевидных сокращений мы можем теперь следующим образом представить доказательство т 120.

Одновременной подстановкой в +103:

По +102 и модус поненс:

Подстановкой q 1Э р вместо q:

Наконец, по tt02 и модус поненс:

(Таким образом, изложение доказательства и некоторых относящихся к нему технических разъяснений занимает столько же места, сколько выше потребовалось для одного только несокращенного доказательства. )

= продолжение правки =

Переходим к доказательству двух следующих теорем системы Р₁ .

+122. f É р

Одновременной подстановкой в +102:

⇐ Предыдущая 1 2 3 4 567 8 Следующая ⇒