Существует некое простое число, большее d.
Ee:~Eb:Ec:(d+Se)=(SSb*SSc)
Осталось только добавить, что это свойство верно всегда, вне зависимости от d. Для этого мы должны добавить квантор общности для d:
Ad:Ee:~Eb:Ec:(d+Se)=(SSb*SSc)
Перед нами — перевод высказывания 5!
Мы завершили упражнение на перевод шести типичных высказываний теории чисел. Однако это еще не гарантирует, что вы стали экспертом в нотации ТТЧ. Остается усвоить несколько тонкостей. Следующие шесть правильно сформированных формул послужат проверкой того, насколько вы овладели нотацией ТТЧ. Что эти формулы означают? Является ли их интерпретация истинными или ложными высказываниями? (Подсказка читателю: при работе с этим упражнением лучше всего двигаться справа налево. Сначала переведите атомы; затем подумайте, что получится, если добавить квантор или тильду; затем, двигаясь налево, добавьте еще один квантор или тильду; снова продвиньтесь налево и опять повторите этот процесс.)
~Ac:Eb:(SS0*b)=c
Ac:~Eb:(SS0*b)=c
Ac:Eb:~(SS0*b)=c
~Eb:Ac:(SS0*b)=c
Eb:~Ac:(SS0*b)=c
Eb:Ac:~(SS0*b)=c
(Еще одна подсказка, либо четыре из них истинны и два ложны, либо, наоборот, два истинны и четыре ложны.)
Теперь давайте на минуту остановимся и переведем дыхание — а заодно подумаем, что означало бы иметь такую формальную систему, которая могла бы отличить все истинные высказывания от ложных. Для такой системы все эти строчки были бы просто некими формальными конструкциями, лишенными содержания (в то время как мы видим в них высказывания). Эта система была бы словно решето, сквозь которое проходили бы только конструкции определенного стиля — «стиля истины». Если вы сами имели дело с шестью формулами выше и отделили истинные от ложных, размышляя об их значении, вы сможете оценить, насколько тонкой должна быть система, которая сможет проделать то же самое, но чисто типографским путем! Граница, отделяющая истинные высказывания от ложных (записанных нотацией ТТЧ) вовсе не пряма — это граница со множеством предательских извилин (вспомните рис. 18). Математики смогли установить некоторые отрезки этой границы, работая над этим сотни лет. Представьте себе, как было бы здорово иметь типографский метод, который с гарантией мог бы поставить любую формулу по правильную сторону границы!
Полезно иметь таблицу Правил Образования для правильно сформированных формул Такая таблица приведена ниже. На подготовительных этапах определяются символы чисел, переменные и термы. Эти три класса строчек являются ингредиентами правильно сформированных формул, но сами они не являются правильно сформированными. Минимальные правильно сформированные формулы — это атомы; существуют способы для соединения атомов. Многие из этих правил — рекурсивные и удлиняющие: в качестве вводных данных они берут элемент определенного класса и производят более длинный элемент того же класса. В этой таблице я использую «x» и «у» как символы для правильно сформированных формул и «s», «t» и «u» — как символы для всех остальных строчек ТТЧ. Нет нужды говорить, что никакой из этих пяти символов сам по себе не является символом ТТЧ.
СИМВОЛЫ ЧИСЕЛ
0 — это символ числа.
Символ числа, слева от которого стоит S — также символ числа.
Примеры: 0 S0 SS0 SSS0 SSSS0 SSSSS0
ПЕРЕМЕННЫЕ
a — это переменная Если забыть об аскетизме, то b, c, d, и e — тоже переменные. Переменная со штрихом справа — также переменная.
Примеры: а b' c" d''' e''''
ТЕРМЫ
Термами являются символы чисел и переменные. Терм, слева от которого стоит S — это также терм.
Если s и t — термы, то (s+t) и (s*t) — также термы.
Примеры: 0 b SSa' (S0*(SS0)+c)) S(Sa*(SbSc))
ТЕРМЫ могут быть подразделены на две категории:
(1) ОПРЕДЕЛЕННЫЕ термы. В них нет переменных.
Примеры: 0 (S0+S0) SS((S0*SS0)+(S0*S0))
(2) НЕОПРЕДЕЛЕННЫЕ термы. В них есть переменные.
Примеры: b Sa(b+S0) (((S0+S0)+S0)+e)
Приведенные выше правила объясняют нам, как получить части правильно сформированных формул; остальные правила говорят нам, как получить полные правильно сформированные формулы.
АТОМЫ
Если s и t — термы, то s+t — атом.
Примеры: S0=0 (SS0+SS0)=SSSS0 S(b+c)=((c*d)*e)
Если атом содержит переменную u, то u в нем свободна.
Таким образом, в последнем примере есть четыре свободных переменных.
ОТРИЦАНИЯ.
Правильно сформированная формула перед которой стоит тильда также правильно сформирована.
Примеры: ~S0=0 ~Eb:(b+b)=S0 ~<0=0эS0=0> ~b=S0
Кванторный статус переменной (говорящий нам, свободна или квантифицирована эта переменная) не меняется при отрицании.
СОСТАВНЫЕ.
Если x и у — правильно сформированные формулы и при этом ни одна переменная, свободная в одной из них, не квантифицирована в другой, тогда все следующие формулы правильно сформированы: <xΛy>, <x V y>,<x э y>
Примеры: <0=0э~0=0>
Кванторный статус переменной здесь не меняется.
КВАНТИФИКАЦИЯ.
Если u — переменная и x — правильно сформированная формула, в которой и свободна, то следующие строчки — также правильно сформированные формулы:Eu:x и Au:x
Примеры: Ab:
ОТКРЫТЫЕ ФОРМУЛЫ содержат по крайней мере одну свободную переменную.
Примеры: ~c=c b=b
ЗАМКНУТАЯ ФОРМУЛА (суждение) не содержит свободных переменных.
Примеры: S0=0 ~Ad:d=0 Ec:
Это дает нам полную таблицу Правил Образования для правильно сформированных формул ТТЧ.
Вот еще несколько упражнений для вас, чтобы проверить, насколько вы поняли нотацию ТТЧ. Попробуйте перевести первые четыре из приведенных ниже высказываний Ч в высказывания ТТЧ, а последнее — в открытую правильно сформированную формулу.
Все натуральные числа равны 4.
Ни одно натуральное число не равно собственному квадрату.
Различные натуральные числа имеют различные последующие элементы.
Если 1 равняется 0, то любое число нечетно.
b — это степень 2.
Последнее может показаться вам трудным. Однако это еще цветочки по сравнению со следующим:
b — это степень 10.
Как это ни странно, чтобы записать это выражение в нашей нотации, требуется большая ловкость. Приступайте к нему только в том случае, если вы готовы просидеть над ним несколько часов — и если при этом вы уже хорошо знакомы с теорией чисел.
Мы изложили нотацию ТТЧ; остается только превратить ТТЧ в ту амбициозную систему, которую мы только что описали. Если нам это удастся, это будет значить, что интерпретация, которую мы дали символам, была правильна. До тех пор, однако, наши интерпретации не более оправданы, чем интерпретация «лошадь — яблоко — счастливая» для символов системы 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 году. Излагая свои постулаты, Пеано следовал за Эвклидом в том смысле, что он не пытался формализовать принципы логических рассуждений. Вместо этого он хотел дать небольшой набор свойств натуральных чисел, из которого можно было бы вывести все остальные путем логических рассуждений. Таким образом, попытка Пеано может быть названа «полуформальной.» Работа Пеано оказала на математиков большое влияние, поэтому я приведу здесь его постулаты. Поскольку Пеано пытался определить именно «натуральное число», мы не будем использовать знакомый и вызывающий ассоциации термин «натуральное число» — вместо него мы будем пользоваться неопределенным термином гений — словом свежим и свободным от математических ассоциаций. Итак, пять постулатов Пеано устанавливают пять ограничений для гениев. Другие неопределенные термины, которыми мы будем пользоваться —