Читаем Гёдель, Эшер, Бах. Эта бесконечная гирлянда полностью

Гёдель, Эшер, Бах. Эта бесконечная гирлянда

Дуглас Роберт Хофштадтер , Дуглас Р. Хофштадтер , Марина А. Эскина

ПРАВИЛО СПЕЦИФИКАЦИИ. Предположим, что u — переменная, встречающаяся внутри строчки x. Если строчка Au:x — теорема, то x — тоже теорема, как и все строчки, получающиеся из x путем замены и на любой (один и тот же) терм.

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

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

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