ECCC-Report TR03-055https://eccc.weizmann.ac.il/report/2003/055Comments and Revisions published for TR03-055en-usThu, 24 Jul 2003 16:10:25 +0300
Paper TR03-055
| Implicit proofs |
Jan Krajicek
https://eccc.weizmann.ac.il/report/2003/055
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 iEF, 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 iEF is not provable in S^1_2.
An iteration of the construction yields
a proof system corresponding to T_2 + Exp and, in principle,
to much stronger theories.
Thu, 24 Jul 2003 16:10:25 +0300https://eccc.weizmann.ac.il/report/2003/055