Типографская теория чисел ( ТТЧ ) — формальная аксиоматическая система, описывающая натуральные числа , которая появляется в книге Дугласа Хофштадтера « Гёдель, Эшер, Бах» . Это реализация арифметики Пеано , которую Хофштадтер использует для объяснения теорем Гёделя о неполноте .
Как и любая система, реализующая аксиомы Пеано, ТНТ способна ссылаться на себя (она самореферентна ).
TNT не использует отдельный символ для каждого натурального числа . Вместо этого он использует простой, единообразный способ присвоения составного символа каждому натуральному числу:
Символ S можно интерпретировать как «последующее» или «число после». Однако, поскольку это теория чисел, такие интерпретации полезны, но не строги. Нельзя сказать, что поскольку четыре является последующим за тремя, то четыре есть SSSS0 , но скорее, поскольку три является последующим за двумя, которые являются последующими за единицей, которая является последующим за нулем, который был описан как 0 , то четыре можно «доказать», что это SSSS0 . TNT разработана таким образом, что все должно быть доказано, прежде чем можно будет сказать, что это правда.
Для обозначения неопределенных терминов TNT использует пять переменных . Это
Можно создать больше переменных, добавив после них символ «штрих» , например:
В более жесткой версии TNT, известной как «строгий» TNT, только
В типографской теории чисел используются обычные символы "+" для сложения и "·" для умножения. Таким образом, чтобы написать "b плюс c", нужно написать
и «a умножить на d» пишется как
Скобки обязательны. Любая неточность нарушит систему формирования ТНТ (хотя тривиально доказано, что этот формализм не нужен для операций, которые являются как коммутативными, так и ассоциативными). Кроме того, одновременно можно оперировать только двумя терминами. Поэтому, чтобы написать "a плюс b плюс c", нужно написать либо
или
Оператор «Равно» используется для обозначения эквивалентности. Он определяется символом «=» и имеет примерно то же значение, что и в математике. Например,
— это утверждение теоремы в ТНТ, имеющее интерпретацию «3 плюс 3 равно 6».
В типографской теории чисел отрицание , т. е. превращение утверждения в его противоположность, обозначается знаком «~» или оператором отрицания. Например,
— теорема в ТТЧ, интерпретируемая как «3 плюс 3 не равно 7».
Под отрицанием подразумевается отрицание в булевой логике ( логическое отрицание ), а не просто противоположность. Например, если бы я сказал «Я ем грейпфрут», противоположностью было бы «Я не ем грейпфрут», а не «Я ем что-то иное, чем грейпфрут». Аналогично «Телевизор включен» отрицается на «Телевизор не включен», а не на «Телевизор выключен», потому что, например, он может быть сломан. Это тонкое, но важное различие.
Если x и y — правильно построенные формулы, и при условии, что ни одна переменная, свободная в одной из них, не квантифицируется в другой, то все следующие формулы являются правильно построенными:
<x∧y>, <x∨y>, <x⊃y>Примеры:
<0=0∧~0=0><b=b∨~∃c:c=b><S0=0⊃∀c:~∃b:(b+b)=c>Количественный статус переменной здесь не меняется.
Используются два квантификатора: ∀и ∃.
Обратите внимание, что в отличие от большинства других логических систем , где квантификаторы по множествам требуют упоминания существования элемента в множестве, в ТНТ это не требуется, поскольку все числа и термины являются строго натуральными числами или логическими булевыми утверждениями. Поэтому это эквивалентно тому, чтобы сказать ∀a:(a∈N):∀b:(b∈N):(a+b)=(b+a)и∀a:∀b:(a+b)=(b+a)
∃означает «существует»∀означает «Для каждого» или «Для всех»:используется для отделения квантификатора от других квантификаторов или от остальной части формулы. Обычно читается как «такой, что»Например:
∀a:∀b:(a+b)=(b+a)(«Для каждого числа a и каждого числа b, a плюс b равно b плюс a», или, выражаясь более образно, «Сложение коммутативно».)
~∃c:Sc=0(«Не существует числа c, такого, что c плюс один равняется нулю», или, выражаясь более образно, «Ноль не является последующим числом ни одного (натурального) числа».)
Все символы исчисления высказываний, за исключением символов атома, используются в типографской теории чисел и сохраняют свои интерпретации.
Атомы здесь определяются как строки, которые представляют собой утверждения равенства, например:
2 плюс 3 равно пяти:
2 плюс 2 равно 4: