On Use of an Explicit Congruence Predicate in Bounded Arithmetic

2009/04/02 by Yamagata, Yoriyuki
#03F30 #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.0904.0335

Abstract

We introduce system S²₀E, a bounded arithmetic corresponding to Buss's S²₀ with the predicate E which signifies the existence of the value. Then, we show that we can Σ^b₂-define truthness of S²₀ E and therefore we can prove consistency of S²₀ E in S²₂. Finally, we conjecture that S²₀ E + Σ^b₁-PIND interprets S²₁.

Related

• A Note on Induction Schemas in Bounded Arithmetic
• Separation of bounded arithmetic using a consistency statement
• Bounded arithmetic AID for Frege system
• Characterizations of interpretability in bounded arithmetic
• A Formal Proof of the Separation P ≠ NP in Bounded Arithmetic