印符数论（，简称），是一种用来描述自然数的形式公理系统，由侯世达在《哥德尔、埃舍尔、巴赫》一书中提出。TNT是皮亚诺算术的一种实现，侯世达以此来解释哥德尔不完备定理。
如同其他实现皮亚诺公理的系统，TNT是自指的。
数字
TNT并没有对每一自然数指定不同的符号，而是使用一种统一的方式来表示所有自然数。其中符号S可理解为“后继”之意。
:
变元
为了表示不定项，TNT中使用了五个变元，分别为：
:a, b, c, d, e
通过添加撇号可以构造出更多的变元，如：
:a', b', c', a, a*
另外一种“简朴的”版本的TNT仅使用a与撇号表示变元：
:a', a, a*, ...
操作符
加法与乘法
TNT中使用“+”表示加法、“·”表示乘法。因此“b加c”可表示为
:(b + c)
而“a乘d”则可以写为
:(a·d)
其中括号是必须的。此外加法与乘法都是二元运算，因而“a加b加c”改须写为
:((a + b) + c)
或
:(a + (b + c))
等于
“=”在TNT中表示“等于”的概念，例如
:(SSS0 + SSS0) = SSSSSS0
在TNT中是一个真命题，表示“3加3等于6”。
否定
“~”表示否定之意，例如
:~(SSS0 + SSS0) = SSSSSSS0
在TNT中是一个真命题，表示“3加3不等于7”。
其中否定是指逻辑非，例如“我在吃葡萄柚”的否定是“我不在吃葡萄柚”，而不是“我在吃葡萄柚以外的东西”。又比如，“电视开着”的否定是“电视没有开着”，而不是“电视关着”。
量词
TNT中使用了∀（全称量词，表示“任何”）与∃（存在量词，表示“存在”）两个量词。例如，
:∀a:∀b:[ (a + b) = (b + a) ]
（“对任意数a与数b，a加b等于b加a”，或用更概括的说法为“加法是可交换的”）
:~∃c:Sc = 0
（“不存在数c使得c加一等于零”，或用更概括的说法为“零不是任何数的后继”）
原子与命题陈述
命题演算中除原子符号外的所有符号都被用于TNT之中，并保持原来的解释。
原子则被关于相等陈述的串替代，如
1不等于2：
:~ S0=SS0
2加3等于5：
:(SS0 + SSS0) = SSSSS0
2加2不等于3：
:~[ (SS0 + SS0) = SSS0 ]
参考文献
*
评论 (0)