В своих пяти постулатах Пеано хотел выразить сущность натуральных чисел. Математики обычно считают, что ему это удалось; однако это не уменьшает важности вопроса «каким образом можно отличить истинное высказывание о натуральных числах от ложного?» Ответа на этот вопрос математики ищут в формальных системах, подобных ТТЧ. Вы найдете в ТТЧ влияние Пеано, поскольку все его постулаты так или иначе вошли в эту систему.
Новые правила ТТЧ: спецификация и обобщение
Мы подошли к новым правилам ТТЧ. Многие из них позволят нам забраться внутрь этой системы и поменять внутреннюю структуру ее атомов. В этом смысле эти правила имеют дело с «микроскопическими» особенностями строчек в большей степени, чем правила исчисления высказываний, обращающиеся с атомами как с неделимыми. Например, было бы хорошо, если бы мы могли выделить строчку ~S0=0 из первой аксиомы. Для этого нам понадобилось бы правило, позволяющее опустить общий квантор и при необходимости одновременно поменять внутреннюю структуру остающейся строчки. Вот это правило:
ПРАВИЛО СПЕЦИФИКАЦИИ. Предположим, что 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
(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) <a=0эSa=0> правило фантазии
(7) Aa:<a=0эSa=0 обобщение
(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, где средняя и правая группы тире возрастали одновременно.)
