Bounded arithmetic AID for Frege system

1998/09/30 by Arai, Toshiyasu
#FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.math/9809205

Abstract

In this paper we introduce a system AID (Alogtime Inductive Definitions) of bounded arithmetic. The main feature of AID is to allow a form of inductive definitions, which was extracted from Buss' propositional consistency proof of Frege systems F. We show that AID proves the soundness of F, and conversely any Σ^b₀-theorem in AID yields boolean sentences of which F has polysize proofs. Further we define Σ^b₁-faithful interpretations between AID + Σb^₀ - CA and a quantified theory QALV of an equational system ALV in P. Clote. Hence ALV also proves the soundness of F.

Related

• Comments on Beckmann's Uniform Reducts
• Constant-Depth Frege Systems with Counting Axioms Polynomially Simulate Nullstellensatz Refutations
• On interpretations of bounded arithmetic and bounded set theory
• On Use of an Explicit Congruence Predicate in Bounded Arithmetic
• Characterizations of interpretability in bounded arithmetic