Войти
Типографская теория чисел ( TNT) - это формальная аксиоматическая система, описывающая натуральные числа, которая встречается в книге Дугласа Хофштадтера « Гедель, Эшер, Бах». Это реализация арифметики Пеано, которую Хофштадтер использует для объяснения теорем Гёделя о неполноте.
Как и любая система, реализующая аксиомы Пеано, TNT способна ссылаться на себя (она является самореферентной ).
TNT не использует отдельный символ для каждого натурального числа. Вместо этого он использует простой и единообразный способ присвоения составного символа каждому натуральному числу:
| нуль | 0 |
| один | S0 |
| два | SS0 |
| три | SSS0 |
| четыре | SSSS0 |
| пять | SSSSS0 |
Символ S можно интерпретировать как «преемник» или «число после». Однако, поскольку это теория чисел, такие интерпретации полезны, но не строги. Нельзя сказать, что, поскольку четыре является преемником трех, что четыре является SSSS0, скорее, поскольку три является преемником двух, который является преемником одного, который является преемником нуля, который был описан как 0, четыре может быть «доказано» как SSSS0. TNT устроен так, что все должно быть доказано, прежде чем можно будет сказать, что это правда.
Для обозначения неопределенных терминов TNT использует пять переменных. Эти
Можно создать больше переменных, добавив после них символ штриха; Например,
В более жесткой версии TNT, известной как «строгий» TNT, только
В теории типографских чисел используются обычные символы «+» для сложения и «» для умножения. Таким образом, написать «b плюс c» значит написать
а «а раз d» записывается как
Скобки обязательны. Любая слабость нарушила бы систему формирования TNT (хотя тривиально доказано, что этот формализм не нужен для операций, которые являются как коммутативными, так и ассоциативными). Также одновременно можно оперировать только двумя терминами. Следовательно, написать «а плюс б плюс с» означает написать либо
или
Оператор «Равно» используется для обозначения эквивалентности. Он определяется символом «=» и имеет примерно то же значение, что и в математике. Например,
это утверждение теоремы в TNT с интерпретацией «3 плюс 3 равно 6».
В теории типографских чисел отрицание, т. Е. Обращение высказывания к его противоположности, обозначается оператором «~» или отрицанием. Например,
это теорема в TNT, интерпретируемая как «3 плюс 3 не равно 7».
Под отрицанием это означает отрицание в булевой логике ( логическое отрицание ), а не просто противоположное. Например, если бы я сказал «Я ем грейпфрут», получилось бы наоборот: «Я не ем грейпфрут», а не «Я ем что-то другое, кроме грейпфрута». Точно так же «Телевидение включено» заменяется «Телевидение выключено», а не «Телевидение выключено». Это небольшая разница, но важная.
Если x и y являются правильно построенными формулами и при условии, что никакая переменная, свободная в одной, не определяется количественно в другой, то все следующие формулы являются правильно сформированными.
lt;x∧ygt;, lt;x∨ygt;, lt;x⊃ygt;Примеры:
lt;0=0∧~0=0gt;lt;b=b∨~∃c:c=bgt;lt;S0=0⊃∀c:~∃b:(b+b)=cgt;Статус количественной оценки переменной здесь не меняется.
Используются два квантификатора: ∀ и ∃ .
Обратите внимание, что в отличие от большинства других логических систем, где кванторы над наборами требуют упоминания о существовании элемента в наборе, это не требуется в TNT, потому что все числа и термины являются строго натуральными числами или логическими логическими операторами. Следовательно, это эквивалентно сказать ∀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:
