我终于明白了为什么老荷（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
作者 具体的步骤照下来供大家参考。
选择“Disable on www.wenxuecity.com”
选择“don't run on pages on this domain”
