A bounded arithmetic AID for Frege systems

Annals of Pure and Applied Logic 103 (1-3):155-199 (2000)
  Copy   BIBTEX

Abstract

In this paper we introduce a system AID 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 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 57–106). Hence ALV also proves the soundness of F

Categories

Keywords

Reprint years

DOI

10.1016/s0168-0072(99)00041-x

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

A Note on Conservativity Relations among Bounded Arithmetic Theories.Russell Impagliazzo & Jan Krajíček - 2002 - Mathematical Logic Quarterly 48 (3):375-377.
On the correspondence between arithmetic theories and propositional proof systems – a survey.Olaf Beyersdorff - 2009 - Mathematical Logic Quarterly 55 (2):116-137.
Systems for a foundation of arithmetic.Andrew Boucher - manuscript
Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem.Neil Thapen - 2011 - Archive for Mathematical Logic 50 (7):665-680.
Notes on polynomially bounded arithmetic.Domenico Zambella - 1996 - Journal of Symbolic Logic 61 (3):942-966.
Review: Jan Krajicek, Pavel Pudlak, Gaisi Takeuti, Bounded Arithmetic and the Polynomial Hierarchy; Samuel R. Buss, Relating the Bounded Arithmetic and Polynomial Time Hierarchies; Domenico Zambella, Notes on Polynomially Bounded Arithmetic. [REVIEW]Stephen Cook - 1999 - Journal of Symbolic Logic 64 (4):1821-1823.
Finite reverse mathematics.Harvey Friedman - manuscript
The deduction rule and linear and near-linear proof simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
Tautologies from pseudo-random generators.Jan Krajíček - 2001 - Bulletin of Symbolic Logic 7 (2):197-212.
Separations of first and second order theories in bounded arithmetic.Masahiro Yasumoto - 2005 - Archive for Mathematical Logic 44 (6):685-688.
Approximate counting by hashing in bounded arithmetic.Emil Jeřábek - 2009 - Journal of Symbolic Logic 74 (3):829-860.
On interpretations of bounded arithmetic and bounded set theory.Richard Pettigrew - 2009 - Notre Dame Journal of Formal Logic 50 (2):141-152.
Bounded arithmetic, propositional logic, and complexity theory.Jan Krajíček - 1995 - New York, NY, USA: Cambridge University Press.
Strict $${\Pi^1_1}$$ -reflection in bounded arithmetic.António M. Fernandes - 2010 - Archive for Mathematical Logic 49 (1):17-34.

Analytics

Added to PP
2014-01-16

Downloads
29 (#536,973)

6 months
7 (#411,886)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

On theories of bounded arithmetic for NC 1.Emil Jeřábek - 2011 - Annals of Pure and Applied Logic 162 (4):322-340.
Expander construction in VNC1.Sam Buss, Valentine Kabanets, Antonina Kolokolova & Michal Koucký - 2020 - Annals of Pure and Applied Logic 171 (7):102796.
The equivalence of theories that characterize ALogTime.Phuong Nguyen - 2009 - Archive for Mathematical Logic 48 (6):523-549.

Add more citations

References found in this work

Bounded arithmetic for NC, ALogTIME, L and NL.P. Clote & G. Takeuti - 1992 - Annals of Pure and Applied Logic 56 (1-3):73-117.
Propositional consistency proofs.Samuel R. Buss - 1991 - Annals of Pure and Applied Logic 52 (1-2):3-29.

Add more references