Правило спецификации позволяет нам выделить нужную строчку из Аксиомы

1. Это одноступенчатая деривация:

Aa:~Sa=0  аксиома 1

~S0=0  спецификация

Обратите внимание, что правило спецификации позволяет некоторым формулам, содержащим свободные переменные (то есть, открытым формулам), стать теоремами. Например, следующие строчки также могут быть выведены из аксиомы 1 при помощи спецификации:

~Sa=0

~S(c+SS0)=0

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

Ac:~S(c+SS0)=0

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

ПРАВИЛО ОБОБЩЕНИЯ: Предположим, что x — теорема, в которой встречается свободная переменная u. Тогда Au:x — тоже теорема.

(Ограничение: к переменным, которые встречаются в свободном виде в посылках фантазий, обобщение неприложимо.)

Вскоре я ясно покажу, почему эти два правила нуждаются в ограничениях. Кстати, это обобщение — то же самое, о котором я упомянул в главе II в Эвклидовом доказательстве бесконечного количества простых чисел. Уже отсюда видно, как правила, манипулирующие символами, начинают приближаться к типу рассуждений, используемых математиками.

Два предыдущих правила объяснили нам, как можно убрать квантор общности и вернуть его на место; следующие два правила покажут, как обращаться с кванторами существования.

ПРАВИЛО ОБМЕНА: Представьте, что u — переменная. Тогда строчки Au:~ и ~Eu: взаимозаменимы везде внутри системы.

Давайте, например, применим это правило к аксиоме 1:

Aa:~Sa=0  аксиома 1

~Ea:Sa=0  обмен

Кстати, вы можете заметить, что обе эти строчки — естественный перифраз в ТТЧ высказывания «Нуль не следует ни за одним из натуральных чисел.» Следовательно, хорошо, что они могут быть с легкостью превращены одна в другую.

Следующее правило еще более интуитивно. Оно соответствует весьма простому типу рассуждений, который мы употребляем, переходя от утверждения «2 — простое число» к утверждению «существует простое число.» Название этого правила говорит само за себя:

ПРАВИЛО СУЩЕСТВОВАНИЯ: Предположим, что некий терм (могущий содержать свободные переменные), появляется один или много раз в теореме. Тогда каждый (или несколько, или все) из этих термов может быть заменен на переменную, которая больше нигде в теореме не встречается, и предварен соответствующим квантором существования.

Давайте применим, как обычно, это правило к аксиоме 1:

Aa:~Sa=0  аксиома 1 

Eb:Aa:~Sa=b  существование

Вы можете поиграть с символами и при помощи данных правил получить теорему: ~Ab:Ea:Sa=b

Мы привели правила, объясняющие, как обращаться с кванторами — но пока ни одно из них не сказало нам, как обращаться с символами «=» и «S». Сейчас мы это сделаем; в следующих правилах r, s и t — произвольные термы.

ПРАВИЛА РАВЕНСТВА:

СИММЕТРИЯ: Если r = s — теорема, то s = r также является теоремой.

ТРАНЗИТИВНОСТЬ: Если r = s и s = t — теоремы, то r = t также является теоремой.

ПРАВИЛА СЛЕДОВАНИЯ:

ДОБАВЛЕНИЕ S: Если r = t — теорема, то Sr = St также является теоремой.

ВЫЧИТАНИЕ S: Если Sr = St — теорема, то r = t также является теоремой.

Теперь у нас есть правила, которые могут дать нам фантастическое разнообразие теорем. Например, результатом следующих дериваций являются фундаментальные теоремы:

(1) Aa:Ab:(a+Sb)=S(a+b)     аксиома 3

(2) Ab:(S0+Sb)=S(S0+b)      спецификация (S0 для а)

(3) (S0+S0)=S(S0+0) спецификация (0 для b)

(4) Aa:(a+0)=a     аксиома 2

(5) (S0+0)=S0     спецификация (S0 для а)

(6) S(S0+0)=SS0    добавление S

(7) (S0+S0)=SS0    транзитивность (строчки 3,6)

*****

(1) Aa:Ab:(a*Sb)=((a*b)+a)    аксиома 5

(2) Ab:(S0*Sb)=((S0*b)+S0)    спецификация (S0 для а)

(3) (S0*S0)=((S0*0)+S0)      спецификация (0 для b)

(4) Aa:Ab:(a+Sb)=S(a+b)    аксиома 3

(5) Ab:((S0*0)+Sb)=S((S0*0)+b спецификация ((S0*0) для а)

(6) ((S0*0)+S0)=S((S0*0)+0)    спецификация (0 для b)

(7) Aa:(a+0)=a         аксиома 2

(8) ((S0*0)+0)=(S0*0)       спецификация ((S0*0) для а)

(9) Aa:(a*0)=0         аксиома 4

(10) (S0*0)=0         спецификация (S0 для а)

(11) ((S0*0)+0)=0                   транзитивность (строчки 8,10)

(12)  S((S0*0)+0)=S0      добавление S

(13)  ((S0*0)+S0)=S0      транзитивность (строчки 6,12)

(14)  (S0*S0)=S0                      транзитивность (строчки 3,13)

Возникает интересный вопрос: «Каким образом мы можем вывести строчку 0=0?» Кажется, что очевидным способом было бы сначала вывести строчку Aa:a=a и затем использовать спецификацию. Как вы думаете, где ошибка в нижеследующем «выводе» Aa:a=a... Можете ли вы ее исправить?

(1) Aa:(a+0)=a   аксиома 2

(2) Aa:a=(a+0)   симметрия

(3) Aa:a=a транзитивность (строчки 2,1)

Я привел это маленькое упражнение, чтобы указать на следующий простой факт: при манипуляции хорошо знакомыми символами, такими, как «=», мы не должны торопиться. Мы должны следовать правилам, а не нашему знанию пассивных значений символов. (Тем не менее, это знание весьма ценно, чтобы помочь нам направить вывод по верному пути.)

Давайте выясним, почему и спецификация, и общность нуждаются в ограничениях Взгляните на следующие две деривации; в каждой из них одно из ограничений нарушено. Обратите внимание, к каким печальным последствиям это привело.

(1)  [                    проталкивание

(2)     a=0             посылка

(3)     Aa:a=0        обобщение (ложно!)

(4)     Sa=0           спецификация

(5)  ]                   выталкивание

(6)        правило фантазии

(7)  Aa:

(8)  <0=0эS0=0>      спецификация

(9)  0=0               предыдущая теорема

(10) S0=0             отделение (строчки 9,8)

Это первое из печальных последствий. Другое получается из неверной спецификации.

(1) Aa:a=a предыдущая теорема

(2) Sa=Sa спецификация

(3) Eb:b=Sa существование

(4) Aa:Eb:b=Sa обобщение

(5) Eb:b=Sb спецификация (ложно!)

Теперь вы убедились, почему необходимы ограничения. Вот простая задачка: переведите (если вы этого уже не сделали раньше) четвертый постулат Пеано в нотацию ТТЧ, и затем выведите эту строчку как теорему.

Если вы поэкспериментируете с теми правилами и аксиомами ТТЧ, которые я привел до сих пор, вы обнаружите, что возможно вывести следующую пирамидальную семью теорем (множество строчек, отлитых из одной формы и отличающихся только тем, что символы чисел 0, S0, SS0, и так далее, идут по нарастающей):

(0+0)=0

(0+S0)=S0

(0+SS0)=SS0

(0+SSS0)=SSS0

(0+SSSS0)=SSSS0

и так далее.

Каждая из теорем этой семьи может быть выведена из предыдущей теоремы с помощью коротенькой, всего лишь в пару строчек, деривации. Результатом является нечто вроде каскада теорем, каждая из которых вызывает к жизни следующую. (Эти теоремы напоминают теоремы pr, где средняя и правая группы тире возрастали одновременно.)

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