[Proof Complexity] New preprint

[thapen]

Dear all,

Pavel Pudlak and I have a new preprint on arxiv: 
https://arxiv.org/abs/2606.10535

Quantified propositional calculi and narrow implicit proofs

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.

Comments or questions are welcome,

Neil Thapen