在本文的上半部分，我们了解了TNT系统如何形式化数论的，下面让我们来深入的了解一下TNT系统。
TNT系统拥有5条公理：1，对于所有a：～Sa=0，2，对于所有a：（a+0）=a，3，对于所有a，b：（ａ+Sb）=S（a+b），4，对于所有a：（a*0）=05，对于所有a，b：（a*Sb）=（（a*b）+a）
它还拥有几条条规则：特称规则：如果对于所有u：x是一条定理，那么x也是一条定理。
概括规则：如果x是一条定理，u作为变元是自由出现的，那么对于所有u：x也是一条定理。
互换规则：对于所有u：～与不存在u可以互换。
存在规则：假设一个项在定理中出现，那么这个项可以用不出现在定理中的变元表示，相应的存在量词必须出现在最前面。
等号规则：对称性和传递性
后继规则：去S和加S。
到目前为止我们的规则已经有点复杂了，开始它依然解决不了一些串的证明，这种问题我们称之为欧米茄不完备：如果一个系统中的所有串都是定理，而全量化后不是定理。
为了加强我们的TNT系统现在我们加入一个新规则——归纳规则：设u是一个变元，X「u」是一个u在其中自由出现的良构公式，如果对于所有u：<X「u」->X「Su/u」>以及X「0/u」都是定理，那么对于所有u：X「u」也是定理。
通过TNT系统我们可以看到一个非常典型的形式推导结构，但毫无疑问它是不完全的，在更广阔的语境中，TNT会在不同的新的改进版本中发挥作用。换句话说，如果TNT是完全的，那么数论专家们就可以提前退休了。
希尔伯特期望利用一个“有穷方法”集去证明类TNT系统的一致性，这是注定要失败的，哥德尔证明了，想要证明TNT系统的一致性，我们需要一个至少和TNT一样强大的强的系统，在计算机程序设计中，我们称之为死循环。
