关于G E B的科普证明，有一点我没有讲清楚，只好再啰嗦一下：）
在这个公式中，最关键的是 TNT ProofPair和ArithemoQuine 函数，
它们应该是能在一个在公理系统中能严格推导出来的。
因为是科普，作者就用了 ＂太复杂＂ 一笔带过：）
作为参考，为了推出 a + b = b + a，TNT 用了56个步骤。
小歌的原版应该用的是不同的构造方式并且附有严格推导。
把推理变化成自然数特性 是发现 老罗公理系统 自指的关键。
因为这个发现，才有小歌的＂天才＂发现一说。
有自指后怎么去说明不是关键，发现自指本身才是关键。
至于作者为什么要引用无门关，可能是他看中了禅宗在破除思维障碍方面的彻底性：）
就像作者引用Escher的画和Bach的音乐一样，
他翻来覆去想说人的思维实际上是被很深的限制了的。
破除这个障碍才是理解小歌证明的关键。
只是他这里用无门关 使我觉得我跟禅宗还真有点缘分：）
在youdecide 网友帮助下我大概明白了怎么去正确解读，再次感谢。
我又读了，TNT ProofPair{a,a'}可能是说a是a'的证明，我说了a'是a的证明：
https://bbs.wenxuecity.com/teatime/747119.html
感觉应该是：不存在 a 使得 a 证明a'（不存在a such that a和a'是个 proof pair）: 推出G不是定理（G的Godel number 是a')。
关于G E B的科普证明，有一点我没有讲清楚，只好再啰嗦一下：）
在这个公式中，最关键的是 TNT ProofPair和ArithemoQuine 函数，
它们应该是能在一个在公理系统中能严格推导出来的。
因为是科普，作者就用了 ＂太复杂＂ 一笔带过：）
作为参考，为了推出 a + b = b + a，TNT 用了56个步骤。
小歌的原版应该用的是不同的构造方式并且附有严格推导。
把推理变化成自然数特性 是发现 老罗公理系统 自指的关键。
因为这个发现，才有小歌的＂天才＂发现一说。
有自指后怎么去说明不是关键，发现自指本身才是关键。
至于作者为什么要引用无门关，可能是他看中了禅宗在破除思维障碍方面的彻底性：）
就像作者引用Escher的画和Bach的音乐一样，
他翻来覆去想说人的思维实际上是被很深的限制了的。
破除这个障碍才是理解小歌证明的关键。
只是他这里用无门关 使我觉得我跟禅宗还真有点缘分：）
在youdecide 网友帮助下我大概明白了怎么去正确解读，再次感谢。
我又读了，TNT ProofPair{a,a'}可能是说a是a'的证明，我说了a'是a的证明：
https://bbs.wenxuecity.com/teatime/747119.html
感觉应该是：不存在 a 使得 a 证明a'（不存在a such that a和a'是个 proof pair）: 推出G不是定理（G的Godel number 是a')。