Propositional Proof Systems and Fast Consistency Provers

Notre Dame Journal of Formal Logic 48 (3):381-398 (2007)
  Copy   BIBTEX

Abstract

A fast consistency prover is a consistent polytime axiomatized theory that has short proofs of the finite consistency statements of any other polytime axiomatized theory. Krajíček and Pudlák have proved that the existence of an optimal propositional proof system is equivalent to the existence of a fast consistency prover. It is an easy observation that NP = coNP implies the existence of a fast consistency prover. The reverse implication is an open question. In this paper we define the notion of an unlikely fast consistency prover and prove that its existence is equivalent to NP = coNP. Next it is proved that fast consistency provers do not exist if one considers RE axiomatized theories rather than theories with an axiom set that is recognizable in polynomial time

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 74,310

External links

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

Through your library

Similar books and articles

The Complexity of Propositional Proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
A Simple Proof That Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
The Unprovability of Consistency: An Essay in Modal Logic.George Boolos - 1979 - Cambridge, England: Cambridge University Press.
Indexed Systems of Sequents and Cut-Elimination.Grigori Mints - 1997 - Journal of Philosophical Logic 26 (6):671-696.
Socratic Proofs.Andrzej Wiśniewski - 2004 - Journal of Philosophical Logic 33 (3):299-326.

Analytics

Added to PP
2010-08-24

Downloads
27 (#427,599)

6 months
1 (#415,900)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Joost Joosten
Universitat de Barcelona

Citations of this work

No citations found.

Add more citations

References found in this work

First-Order Proof Theory of Arithmetic.Samuel R. Buss - 2000 - Bulletin of Symbolic Logic 6 (4):465-466.
The Lengths of Proofs.Toshiyasu Arai - 2000 - Bulletin of Symbolic Logic 6 (4):473-475.

Add more references