Rosser-type undecidable sentences based on Yablo's paradox
Rosser-type undecidable sentences based on Yablo's paradox
复制标题
基于Yablo悖论的Rosser型不可判定句子
DOI：
10.1007/s10992-013-9309-z
复制
发表时间：
2014
影响因子：
1.5
通讯作者：
Taishi Kurahashi
中科院分区：
文献类型：
--
作者：
Norihiro Nakashima;Hajime Matsui;Taishi Kurahashi
人们普遍认为哥德尔和罗瑟对不完备性定理的证明与说谎者悖论有关。雅布洛悖论，一个没有自我参照的类说谎者悖论，也可以用来证明哥德尔的第一和第二不完全性定理。我们表明，使用Rosser的可证明性谓词的Yablo悖论的形式化的情况是不同的Rosser的证明。也就是说，通过使用技术的Guelei和Solovay，我们证明了每个实例的Rosser型形式化的Yablo悖论的每个一致的，但不是101-声音理论的不可判定性是依赖于一个标准的证明谓词的选择。
It is widely considered that Gödel’s and Rosser’s proofs of the incompleteness theorems are related to the Liar Paradox. Yablo’s paradox, a Liar-like paradox without self-reference, can also be used to prove Gödel’s first and second incompleteness theorems. We show that the situation with the formalization of Yablo’s paradox using Rosser’s provability predicate is different from that of Rosser’s proof. Namely, by using the technique of Guaspari and Solovay, we prove that the undecidability of each instance of Rosser-type formalizations of Yablo’s paradox for each consistent but not Σ1-sound theory is dependent on the choice of a standard proof predicate.