Does extended Frege p-simulate circuit Frege with substitutions?

Question

Consider propositional logic.

Frege systems are textbook-style proof systems, with a finite set of logically sound axioms and rules. However you can generalise each axiom/rule with substitutions, replacing each variable simultaneously everywhere with a term. This is fine because if we take any propositional tautology and replace the variables, which can have value 0 or 1, with terms that can have value 0 or 1, the tautology is still guaranteed to evaluate to true under all assignments. Frege systems are all p-equivalent.

Frege systems normally only allow this for axioms and rules, but you can also soundly allow substitutions on derived formulas, as long as they are guaranteed to be tautological as well. This can be guaranteed by not allowing non-tautological assumptions anywhere in the proofs. The resulting system is known sometimes as Substitution Frege.

While Substitution Frege allows you to replace variables with terms. Extended Frege allows the opposite, to replace complicated formulas to be replaced with fresh variables (extension variables). This allows Extended Frege to avoid large complicated formulas. Extended Frege even allows extension variables that use previous extension variables in their definitions.

However extension and substitution don't seem very compatible to me. It would be wrong to substitute extension variables with terms that don't represent the formulas they actually represent and the assumptions now include non-tautological information: the definitions of extension variables.

A third variation is Circuit Frege, which is Frege but using circuits (which allow subformulae/subcircuits to be reused without rewriting them) instead of formulas.

Substitution Frege, Extended Frege and Circuit Frege are all p-equivalent. In other words, there is an efficient (polynomial time) algorithm that can take a proof in one format and transform it into a proof in the other. The proofs that these algorithms (p-simulations) exists, some of them seem obvious, others appear to involved non-trivial relationships between propositional proof complexity and theories of Bounded Arithmetic. Which I admit I don't fully understand yet.

Whether the tautology is a formula or a circuit should not fundamentally change the soundness of the substitution rule, you are just replacing the input variables (that can be 0 or 1) with terms (either formulas or circuits) than can be 0 or 1. So while extension and substitution seem incompatible circuitry and substitution do seem compatible. I'll call this system Circuit Frege with Substitutions.

The question I have is asking if you have a proof of a tautology f in Circuit Frege with Substitution, does there exist an efficient way to turn that into an Extended Frege proof of f (possibly using extension variables to represent the circuitry in f)? Does it make a difference if the substituted terms are formulas or circuits? Whom can I cite for these results?

Answer 1

The answer is yes. I’d say this is essentially folklore, but if you want a published reference, see Lemma 2.6 in my paper [1]. The lemma is stated more generally for proof systems for transitive modal logics; plain classical logic is just the special case for the modal logic axiomatized by $A\leftrightarrow\Box A$ (or you can just read the proof and ignore all boxes).

The statement of Lemma 2.6 says, in your terminology, that given a proof of a circuit $\phi$ in Circuit Frege with Substitution (called SCF in the paper), we can construct in polynomial time a Substitution Frege proof of a formula $E_\phi\to q_\phi$ “using extension variables to represent the circuitry in $\phi$”. For classical logic, you can then transform the SF-proof into a CF-proof in polynomial time (this is not true for modal logics in general), and this gives you a CF-proof of $\phi$ itself by Lemma 2.5, hence an EF-proof of $\phi$ if $\phi$ is just a formula.

(Alternatively, if $\phi$ is just a formula, you can apply the substitution rule once more to substitute the extension variables in $E_\phi\to q_\phi$ with the subformulas they represent, obtaining an SF-proof of $\phi$, which you can transform to an EF-proof.)

Reference:

[1] E. Jeřábek: On the proof complexity of logics of bounded branching, Annals of Pure and Applied Logic 174 (2023), no. 1, article no. 103181, 54 pp., doi 10.1016/j.apal.2022.103181. Preprint arXiv:2004.11282.