我終於明白了為什麽老荷（D R Hofstadter) 在G E B中要把無門關和小歌放一起了。
這個公式（簡稱 G），是老荷用來說明Gödel 證明的科普版。
這裏T N T 是一個跟老羅（素）＂數學原理＂類似的公理係統。
前麵我們提到過，小歌天才地把推理數字化，
這樣公式就有了兩層意思，一個是在數字層麵，一個在推理層麵。
TNT Proof Pair 是指 a和a‘是兩個公式的推理操作
在數字層麵，它表達公式的數字的這個基本性質：
給定a和a‘兩個公式數字表達（Gödel 數），我們可以在有限步內，
根據已有的數字函數（定理）回答出能不能從a倒推回a’。
回答N o，推理不正確。
回答Yes, 從a' Gödel 數 能推出 a Gödel 數。
注意所有推理公式都是＂簡單＂函數，這些操作隻跟自然數操作計算有關。
因為公式的 數字 是不是 Gödel數 和 公式 有一一對應關係，
所以在推理層麵,我們可以說 T N T Proof Pair 就是在說：
a 公式是不是a‘ 公式推導出來的。
ArithmoQuine 是自指操作：
這裏a” 是有一個自由變量的公式的數字，
a‘ 是把上麵公式的自由變量用a” 帶入後得到的公式的數字，
比如 b=0 ，或者 彐b’：b’=b，它們的自由變量是b，
它們都有一個a” 數字，把b置換成a” ，就可算出a’ 代表的數。
在數字層麵，它是說 a’ 就是 ：the arithmoquinification of a” 。
這個反推操作在數字層麵也是＂簡單＂數字操作，
可以在有限步內獲得明確答案。
在推理層麵，它就是在說，a‘ 就是"Quine" a” ：）
（參見 Quine Paradox)
我理解，這個操作就是＂自指＂的 數字表達。
因為這裏把自由變量換成自己的公式的數字實際上就是＂自指＂：）
根據老荷的推導，這個公式會導出＂兩頭堵＂：）
＊感謝 youdecide 網友指出 下列描述的錯誤*
*G的數字有兩種可能，是不是Gödel 數。
*G的公式也有兩種可能，是不是定理。
*根據小歌的構造，定理一定對應Gödel 數。
*假設G的數字是 Gödel 數，那麽就會導出 G不是定理: 矛盾
*這對應：G is not theorem of TNT。
如果G是定理，那麽上述G就必然產生＂真＂的結果，
但是根據分析，上述G的＂還原＂結果是 ＂G不是定理＂
如果結果是真，正好矛盾：）
如果你認為G不是定理O K，這本身不是問題，也不會導致矛盾。
但因為G描述了一個真實，你就必須承認公理係統
有局限性，不能推出所有真實公式。
那你可能會想用～G代替G，恭喜你，在這種情況下，～G的Gödel 數為真，
～G公式就變成了＂無用的＂的真理（思考題：Why:）
這是老荷關於無門關的第一關 ＂趙州狗子佛性＂的感悟：
它精確地概括了什麽叫＂Undecidable “，
它和G是不是定理有異曲同工之妙：）
Escher 的 左右互博也很好表現了G http://M.C. Escher (Drawing Hands) Art Poster Print - 26x22 Art Poster Print by M. C. Escher, 26x22 Art Poster Print by M. C. Escher, 26x22
作者 具體的步驟照下來供大家參考。
