On the correspondence between arithmetic theories and propositional proof systems - a survey

Mathematical Logic Quarterly 55 (2):116-137 (2009)

The purpose of this paper is to survey the correspondence between bounded arithmetic and propositional proof systems. In addition, it also contains some new results which have appeared as an extended abstract in the proceedings of the conference TAMC 2008 [11].Bounded arithmetic is closely related to propositional proof systems; this relation has found many fruitful applications. The aim of this paper is to explain and develop the general correspondence between propositional proof systems and arithmetic theories, as introduced by Krajíček and Pudlák [46]. Instead of focusing on the relation between particular proof systems and theories, we favour a general axiomatic approach to this correspondence. In the course of the development we particularly highlight the role played by logical closure properties of propositional proof systems, thereby obtaining a characterization of extensions of EF in terms of a simple combination of these closure properties
Keywords logical closure properties  propositional translations  extended Frege systems  propositional proof systems  Bounded arithmetic
Categories (categorize this paper)
DOI 10.1002/malq.200710069
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 47,350
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Notes on Polynomially Bounded Arithmetic.Domenico Zambella - 1996 - Journal of Symbolic Logic 61 (3):942-966.
Bounded Arithmetic and the Polynomial Hierarchy.Jan Krajíček, Pavel Pudlák & Gaisi Takeuti - 1991 - Annals of Pure and Applied Logic 52 (1-2):143-153.
The Complexity of Propositional Proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
Forcing in Proof Theory.Jeremy Avigad - 2004 - Bulletin of Symbolic Logic 10 (3):305-333.

View all 25 references / Add more references

Citations of this work BETA

Partially Definable Forcing and Bounded Arithmetic.Albert Atserias & Moritz Müller - 2015 - Archive for Mathematical Logic 54 (1-2):1-33.

Add more citations

Similar books and articles

Some Remarks on Lengths of Propositional Proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.
The Complexity of Propositional Proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
Quantum Deduction Rules.Pavel Pudlák - 2009 - Annals of Pure and Applied Logic 157 (1):16-29.
Implicit Proofs.Jan Krajíček - 2004 - Journal of Symbolic Logic 69 (2):387 - 397.
Herbrand Style Proof Procedures for Modal Logic.Marta Cialdea - 1993 - Journal of Applied Non-Classical Logics 3 (2):205-223.


Added to PP index

Total views
15 ( #597,491 of 2,291,079 )

Recent downloads (6 months)
2 ( #580,277 of 2,291,079 )

How can I increase my downloads?


My notes

Sign in to use this feature