Bounded arithmetic AID for Frege system

Details Bounded arithmetic AID for Frege system Bounded arithmetic AID for Frege system

1998-09-30

arxiv.org/abs/math/9809205v1

Mathematics

Logic

Scientific paper

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 \Sigma^b_0-theorem in AID yields boolean sentences of which F has polysize proofs. Further we define \Sigma^b_1-faithful interpretations between AID + \Sigma b^_0 - CA and a quantified theory QALV of an equational system ALV in P. Clote. Hence ALV also proves the soundness of F.

Affiliated with

Also associated with

No associations

Rating

Bounded arithmetic AID for Frege system does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Bounded arithmetic AID for Frege system, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Bounded arithmetic AID for Frege system will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-693065