Journal of Symbolic Logic 63 (2):709 - 738 (1998)

A Frege proof systemFis any standard system of prepositional calculus, e.g., a Hilbert style system based on finitely many axiom schemes and inference rules. An Extended Frege systemEFis obtained fromFas follows. AnEF-sequence is a sequence of formulas ψ1, …, ψκsuch that eachψiis either an axiom ofF, inferred from previous ψuand ψv by modus ponens or of the formq↔ φ, whereqis an atom occurring neither in φ nor in any of ψ1,…,ψi−1. Suchq↔ φ, is called an extension axiom andqa new extension atom. AnEF-proof is anyEF-sequence whose last formula does not contain any extension atom. In [12], S. A. Cook and R. Reckhow proved that the pigeonhole principlePHPhas a simple polynomial sizeEF-proof and conjectured thatPHPdoes not admit polynomial sizeF-proof. In [5], S. R. Buss refuted this conjecture by furnishing polynomial sizeF-proof forPHP. Since then the important separation problem of polynomial sizeFand polynomial sizeEFhas not shown any progress.In [11], S. A. Cook introduced the systemPV, a free variable equational logic whose provable functional equalities are ‘polynomial time verifiable’ and showed that the metamathematics ofFandEFcan be developed inPVand the soundness ofEFproved inPV. In [3], S. R. Buss introduced the first order systemand showed thatis essentially a conservative extension ofPV. There he also introduced a second order system.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2586859
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 65,784
Through your library

References found in this work BETA

Propositional Consistency Proofs.Samuel R. Buss - 1991 - Annals of Pure and Applied Logic 52 (1-2):3-29.
S 3 I andV 2 I (BD).Gaisi Takeuti - 1990 - Archive for Mathematical Logic 29 (3):149-169.
RSUV Isomorphisms for TAC I , TNC I and TLS.G. Takeuti - 1995 - Archive for Mathematical Logic 33 (6):427-453.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Evidence, Judgment and Truth.Verena Mayer - 2007 - Grazer Philosophische Studien 75 (1):175-197.
Frege on Indirect Proof.Ivan Welty - 2011 - History and Philosophy of Logic 32 (3):283-290.
Frege's Proof of Referentiality.Øystein Linnebo - 2004 - Notre Dame Journal of Formal Logic 45 (2):73-98.
Implicit Proofs.Jan Krajíček - 2004 - Journal of Symbolic Logic 69 (2):387 - 397.
Syntax in Basic Laws §§29–32.Bryan Pickel - 2010 - Notre Dame Journal of Formal Logic 51 (2):253-277.


Added to PP index

Total views
219 ( #48,289 of 2,462,967 )

Recent downloads (6 months)
1 ( #449,363 of 2,462,967 )

How can I increase my downloads?


My notes