Propositional proof systems and fast consistency provers (Q2469433)

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.