ГЕДЕЛЬ, ЭШЕР, БАХ: эта бесконечная гирлянда

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)

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

Почему спецификация и общность ограничены