| Popis: |
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 in Buss (Ann. Pure Appl. Logic 52 (1991) 3–29). We show that AID proves the soundness of F , and conversely any Σ 0 b -theorem in AID yields boolean sentences of which F has polysize proofs. Further we define Σ 1 b -faithful interpretations between AID+Σ 0 b -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 F . |
Full Text from ScienceDirect