PreprintarXiv licencearXiv
Quantified propositional calculi and narrow implicit proofs
Abstract
In the implicit version of a propositional proof system Q, we work with Q-proofs that are not written down directly, but are succinctly encoded by circuits. Thus implicit Q-proofs are potentially exponentially shorter than usual Q-proofs. We study narrow implicit proofs, a restricted version of this notion, in which lines in the encoded proof can only have polynomial size. We use a cut-elimination construction to show that G_{i+1} is equivalent to narrow implicit G_i, for i >= 1, where G_i is the extension of Frege allowing reasoning with Sigma^q_i quantified propositional formulas. We show that G_1 is equivalent to implicit resolution.
Related
BibTeX
@misc{pudlak2026quantified,
title = {{Quantified propositional calculi and narrow implicit proofs}},
author = {Pavel Pudlák and Neil Thapen},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2606.10535},
eprint = {2606.10535},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2606.10535},
}
RIS
TY - UNPB
TI - Quantified propositional calculi and narrow implicit proofs
AU - Pavel Pudlák
AU - Neil Thapen
PY - 2026
DA - 2026/09/01
PB - arXiv
DO - 10.48550/arxiv.2606.10535
UR - https://arxiv.org/abs/2606.10535
AB - In the implicit version of a propositional proof system Q, we work with Q-proofs that are not written down directly, but are succinctly encoded by circuits. Thus implicit Q-proofs are potentially exponentially shorter than usual Q-proofs. We study narrow implicit proofs, a restricted version of this notion, in which lines in the encoded proof can only have polynomial size. We use a cut-elimination construction to show that G_{i+1} is equivalent to narrow implicit G_i, for i >= 1, where G_i is the extension of Frege allowing reasoning with Sigma^q_i quantified propositional formulas. We show that G_1 is equivalent to implicit resolution.
ER -