Implicit proofs. (English) Zbl 1069.03053

Summary: We describe a general method how to construct from a propositional proof system \(P\) a possibly much stronger proof system \(iP\). The system \(iP\) operates with exponentially long \(P\)-proofs described “implicitly” by polynomial size circuits.
As an example we prove that proof system \(i\text{EF}\), implicit EF, corresponds to bounded arithmetic theory \(V^1_2\) and hence, in particular, polynomially simulates the quantified propositional calculus \(G\) and the \(\Pi^b_1\)-consequences of \(S^1_2\) proved with one use of exponentiation. Furthermore, the soundness of \(i\text{EF}\) is not provable in \(S^1_2\). An iteration of the construction yields a proof system corresponding to \(T_2 + \text{Exp}\) and, in principle, to much stronger theories.


03F20 Complexity of proofs
03D15 Complexity of computation (including implicit computational complexity)
68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)
03F30 First-order arithmetic and fragments
Full Text: DOI


[1] DOI: 10.1016/0168-0072(90)90023-U · Zbl 0711.03025
[2] The relative efficiency of propositional proof systems 44 pp 36– (1979) · Zbl 0408.03044
[3] Seventh Annual ACM Symposium on Theory of Computing pp 83– (1975)
[4] Bounded arithmetic (1986)
[5] Bounded arithmetic, propositional logic, and complexity theory 60 (1995)
[6] DOI: 10.1002/malq.19900360106 · Zbl 0696.03031
[7] Propositional proof systems, the consistency of first order theories and the complexity of computations 54 pp 1063– (1989) · Zbl 0696.03029
[8] Diagonalization in proof complexity (2003)
[9] DOI: 10.1007/978-1-4612-3466-1_15
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.