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

Мы изложили нотацию ТТЧ; остается только превратить ТТЧ в ту амбициозную систему, которую мы только что описали. Если нам это удастся, это будет значить, что интерпретация, которую мы дали символам, была правильна. До тех пор, однако, наши интерпретации не более оправданы, чем интерпретация «лошадь — яблоко — счастливая» для символов системы pr.

Можно было бы предложить следующий способ для построения ТТЧ: (1) Не использовать никаких правил вывода — они не нужны, так как (2) мы будем считать за аксиомы все истинные суждения теории чисел (записанные нотацией ТТЧ). Какой простой рецепт! К несчастью, он начисто лишен смысла, как нам и подсказывает наша первая реакция. Часть (2), разумеется, не является типографским описанием строчек, в то время как целью ТТЧ является именно типографское описание истинных высказываний.

Пять аксиом и первое правило ТТЧ

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

Она может быть выведена так же, как <P V ~ P >. Прежде чем приводить правила, давайте запишем пять аксиом. ТТЧ:

АКСИОМА 1: Aa:~Sa=0

АКСИОМА 2: Aa:(a+0)=a

АКСИОМА 3: Aa:Ab:(a+Sb)=S(a+b)

АКСИОМА 4: Aa:(a*0)=0

АКСИОМА 5: Aa:Ab:(a*Sb)=((a*b)+a)

(В строгой версии вместо b используйте a'.) Все они очень просты. Аксиома 1 сообщает что-то о числе 0; аксиомы 2 и 3 говорят о свойствах сложения; аксиомы 4 и 5 говорят о свойствах умножения и о его отношении к сложению.

Пять постулатов Пеано

Интерпретация первой аксиомы — «Нуль не следует ни за каким натуральным числом» — это одно из пяти знаменитых свойств натуральных чисел, впервые выраженных математиком и логиком Джузеппе Пеано в 1889 году. Излагая свои постулаты, Пеано следовал за Эвклидом в том смысле, что он не пытался формализовать принципы логических рассуждений. Вместо этого он хотел дать небольшой набор свойств натуральных чисел, из которого можно было бы вывести все остальные путем логических рассуждений. Таким образом, попытка Пеано может быть названа «полуформальной.» Работа Пеано оказала на математиков большое влияние, поэтому я приведу здесь его постулаты. Поскольку Пеано пытался определить именно «натуральное число», мы не будем использовать знакомый и вызывающий ассоциации термин «натуральное число» — вместо него мы будем пользоваться неопределенным термином гений — словом свежим и свободным от математических ассоциаций. Итак, пять постулатов Пеано устанавливают пять ограничений для гениев. Другие неопределенные термины, которыми мы будем пользоваться — джинн и мета. Читатель может догадаться сам, какие знакомые понятия скрываются за этими двумя терминами. Далее следуют пять постулатов Пеано:

(1) Джинн — это Гений.

(2) Каждый Гений имеет мету (которая тоже является Гением).

(3) Джинн не является метой никакого Гения.

(4) Различные Гении имеют различные меты.

(5) Если джинн имеет X и каждый Гений передает X своей мете, тогда все Гении получают X.

В свете ламп «Маленького гармонического лабиринта» мы должны наименовать множество всех Гениев «БОГом». Это напоминает нам о знаменитом высказывании немецкого математика и логика Леопольда Кроникера, архиврага Георга Кантора: «Бог сотворил натуральные числа; все остальное — работа человека.»

Вы можете узнать в пятом постулате Пеано принцип математической индукции — другой термин для «наследственного» доказательства. Пеано надеялся, что его ограничения понятий «джинна», «Гения» и «меты» были так сильны, что эти понятия были бы идентичны для всех людей и формировали бы у них в сознании совершенно изоморфные структуры. Например, для любого человека существовало бы бесконечное число различных Гениев. И, предположительно, каждый согласился бы с тем, что ни один Гений не совпадает со своей метой или мета-метой… и т. д.

В своих пяти постулатах Пеано хотел выразить сущность натуральных чисел. Математики обычно считают, что ему это удалось; однако это не уменьшает важности вопроса «каким образом можно отличить истинное высказывание о натуральных числах от ложного?» Ответа на этот вопрос математики ищут в формальных системах, подобных ТТЧ. Вы найдете в ТТЧ влияние Пеано, поскольку все его постулаты так или иначе вошли в эту систему.

Новые правила ТТЧ: спецификация и обобщение

Мы подошли к новым правилам ТТЧ. Многие из них позволят нам забраться внутрь этой системы и поменять внутреннюю структуру ее атомов. В этом смысле эти правила имеют дело с «микроскопическими» особенностями строчек в большей степени, чем правила исчисления высказываний, обращающиеся с атомами как с неделимыми. Например, было бы хорошо, если бы мы могли выделить строчку ~S0=0 из первой аксиомы. Для этого нам понадобилось бы правило, позволяющее опустить общий квантор и при необходимости одновременно поменять внутреннюю структуру остающейся строчки. Вот это правило: