A bounded arithmetic AID for Frege systems Original Research Article

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 View the MathML source in Buss (Ann. Pure Appl. Logic 52 (1991) 3–29). We show that AID proves the soundness of View the MathML source, and conversely any View the MathML source-theorem in AID yields boolean sentences of which View the MathML source has polysize proofs. Further we define View the MathML source-faithful interpretations between View the MathML source-CA and a quantified theory QALV of an equational system ALV in Clote (Ann. Math. Art. Intell. 6 (1992) 57–106). Hence ALV also proves the soundness of View the MathML source.