有道理。TNT ProofPair和ArithemoQuine可能很复杂。上个帖我字面理解的跟帖可能把a和a’说反了。

我又读了，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')。