Premium
On the correspondence between arithmetic theories and propositional proof systems – a survey
Author(s) -
Beyersdorff Olaf
Publication year - 2009
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200710069
Subject(s) - propositional variable , propositional formula , closure (psychology) , mathematics , well formed formula , proof complexity , axiom , bounded function , relation (database) , propositional calculus , axiomatic system , structural proof theory , simple (philosophy) , algebra over a field , proof theory , calculus (dental) , discrete mathematics , arithmetic , pure mathematics , computer science , mathematical proof , epistemology , theoretical computer science , intermediate logic , philosophy , dentistry , database , mathematical analysis , geometry , medicine , economics , description logic , market economy
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 (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)