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_0-theorem in AID yields boolean sentences of which F has polysize proofs. Further we define Σ^b_1-faithful interpretations between AID + Σb^_0 - CA and a quantified theory QALV of an equational system ALV in P. Clote. Hence ALV also proves the soundness of F.
Connections
Explore this paper’s authors, topics and related work.
Building this map preview
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Reviews 0
Write a review
No reviews yet.
Discussion 0
Add a comment
No comments yet.