在本文的上半部分钓株，我們了解了TNT系統(tǒng)如何形式化數(shù)論的却紧，下面讓我們來深入的了解一下TNT系統(tǒng)。
TNT系統(tǒng)擁有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）
它還擁有幾條條規(guī)則：特稱規(guī)則：如果對于所有u：x是一條定理翻诉，那么x也是一條定理炮姨。
概括規(guī)則：如果x是一條定理，u作為變元是自由出現(xiàn)的碰煌，那么對于所有u：x也是一條定理舒岸。
互換規(guī)則：對于所有u：～與不存在u可以互換。
存在規(guī)則：假設一個項在定理中出現(xiàn)芦圾，那么這個項可以用不出現(xiàn)在定理中的變元表示蛾派，相應的存在量詞必須出現(xiàn)在最前面。
等號規(guī)則：對稱性和傳遞性
后繼規(guī)則：去S和加S个少。
到目前為止我們的規(guī)則已經(jīng)有點復雜了洪乍，開始它依然解決不了一些串的證明，這種問題我們稱之為歐米茄不完備：如果一個系統(tǒng)中的所有串都是定理稍算，而全量化后不是定理典尾。
為了加強我們的TNT系統(tǒng)現(xiàn)在我們加入一個新規(guī)則——歸納規(guī)則：設u是一個變元，X「u」是一個u在其中自由出現(xiàn)的良構(gòu)公式糊探，如果對于所有u：<X「u」->X「Su/u」>以及X「0/u」都是定理钾埂，那么對于所有u：X「u」也是定理。
通過TNT系統(tǒng)我們可以看到一個非常典型的形式推導結(jié)構(gòu)科平，但毫無疑問它是不完全的褥紫，在更廣闊的語境中，TNT會在不同的新的改進版本中發(fā)揮作用瞪慧。換句話說髓考，如果TNT是完全的，那么數(shù)論專家們就可以提前退休了弃酌。
希爾伯特期望利用一個“有窮方法”集去證明類TNT系統(tǒng)的一致性氨菇，這是注定要失敗的，哥德爾證明了妓湘，想要證明TNT系統(tǒng)的一致性查蓉，我們需要一個至少和TNT一樣強大的強的系統(tǒng)，在計算機程序設計中榜贴，我們稱之為死循環(huán)豌研。
