有界算术中一个显式同余谓词的使用
On Use of an Explicit Congruence Predicate in Bounded Arithmetic
摘要：
我们引入系统S^2_0E，它是一个有界算术，对应于Buss的S^2_0，谓词E表示值的存在性。然后证明了S^2_0 E的真性可以由S^2_b_2-定义，从而证明了S^2_0 E在S^2_2中的相容性.最后，我们猜想S^2_0 E + B^b_1-PIND解释S^2_1。
英文摘要：
We introduce system S^2_0E, a bounded arithmetic corresponding to Buss's S^2_0 with the predicate E which signifies the existence of the value. Then, we show that we can Σ^b_2-define truthness of S^2_0 E and therefore we can prove consistency of S^2_0 E in S^2_2. Finally, we conjecture that S^2_0 E + Σ^b_1-PIND interprets S^2_1.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
