Propositional proof systems and fast consistency provers

DOI10.1305/NDJFL/1187031410MaRDI QIDQ2469433zbMATH OpenOpenAlexWikidataFDO

Authors Joost J. Joosten

Publication date 5 February 2008

Published in Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2004.05431

zbMATH Keywords

fast consistency proveroptimal proof system

Mathematics Subject Classification ID

Complexity of proofs (03F20) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Abstract: A fast consistency prover is a consistent poly-time axiomatized theory that has short proofs of the finite consistency statements of any other poly-time axiomatized theory. Kraj'iv{c}ek and Pudl'ak 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 $sfNP=sfcoNP$ 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 $sfNP=sfcoNP$. 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.

Review text

The paper studies the problem of the length of proofs of finite consistency statements in first-order theories, and its relationship to propositional proof systems and the \(\text{NP}= \text{coNP}\) problem. A \textit{fast consistency prover} (facop) is defined to be a consistent poly-time theory \(S\) containing some arithmetic such that for any consistent poly-time theory \(T\), the finite consistency statements for \(T\) have poly-size proofs in \(S\). By a result of \textit{J. Krajíček} and \textit{P. Pudlák} [J. Symb. Log. 54, No. 3, 1063--1079 (1989; Zbl 0696.03029)], such a facop exists if and only if there exists an optimal propositional proof system. The author further defines an \textit{unlikely fast consistency prover} (ufacop) to be a consistent poly-time theory which proves the finite consistency statements \(\text{Con}_T(x)\) of any consistent poly-time theory \(T\) in size polynomial in \(x^e\), where the axioms of \(T\) are decidable in time \(n^e\). It is shown that the existence of ufacops is equivalent to the existence of polynomially bounded propositional proof systems (and thus to \(\text{NP}= \text{coNP}\), by \textit{S. A. Cook} and \textit{R. A. Reckhow} [J. Symb. Log. 44, 36--50 (1979; Zbl 0408.03044)]). The author also shows that facops do not exist if the requirement of poly-time axiomatization of \(T\) (and \(S\)) is loosened to an r.e.\ axiomatization.

Recommendations

• Consistency and optimality
• Propositional proof systems, the consistency of first order theories and the complexity of computations
• scientific article; zbMATH DE number 910749
• Consistency, optimality, and incompleteness
• On slicewise monotone parameterized problems and optimal proof systems for TAUT
• NEW RELATIONS AND SEPARATIONS OF CONJECTURES ABOUT INCOMPLETENESS IN THE FINITE DOMAIN
• Logical Approaches to Computational Barriers
• Optimal acceptors and optimal proof systems
• scientific article; zbMATH DE number 1179974

Cited in

(4)

• Propositional consistency proofs
• Consistency and optimality
• Propositional proof systems, the consistency of first order theories and the complexity of computations
• Proof Systems for Effectively Propositional Logic

This page was built for publication: Propositional proof systems and fast consistency provers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2469433)