有道理。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')。