Source-linked AI summary
Exponential Gaps Between Intuitionistic Linear Extended Frege Systems
Amirhossein Akbar Tabatabai
TL;DR
The paper asks whether proof complexity can distinguish intuitionistic substructural and linear Extended Frege systems on formulas already provable in weaker logics. It proves exponential separations using a feasible disjunction property, showing that stronger logics can yield exponentially shorter proofs. The result also applies in the !-free setting.
Problem
Previous constructions did not distinguish FLe-Extended Frege from intuitionistic Extended Frege, or intermediate systems, on formulas already provable in FLe.
Method
The paper proves a feasible disjunction property for Frege systems of structural logics below intuitionistic logic and uses it to transfer lower bounds into separations.
Results
For structural L below intuitionistic logic and M not contained in L, some FLe-provable formulas have polynomial-size M-Frege proofs but exponential-size L-Extended Frege proofs.
Takeaways & Limitations
Extending a structural logic can yield an exponential reduction in Frege proof lines even for formulas already provable in FLe.
Takeaways & Limitations
The structural-rule framework restricts attention to rules motivated by equivalence to axioms and allowing free context wherever possible.
Abstract
from arXiv · showhide
In this paper, we establish exponential separations between Extended Frege systems for a range of intuitionistic substructural and linear logics. More precisely, for any logic $L$ below the intuitionistic logic obtained by extending $\mathbf{ILL}$ with structural rules, and any logic $M$ not contained in $L$, we construct a family of $\mathsf{FL_e}$-provable formulas that have short proofs in $M$-Frege but require proofs of exponential size in $L$-Extended Frege. The same result holds in the $!$-free settings, using $\mathbf{IMALL}$ and $\mathbf{FL_e}$ in place of $\mathbf{ILL}$. The key ingredient in proving these separations is a variant of the feasible disjunction property for $L$-Frege, which may be of independent interest.
1 Introduction
The paper closes an open gap by proving exponential separations among Extended Frege systems for broad classes of intuitionistic substructural and linear logics. Its central tool is a feasible disjunction property for Frege systems.
- Motivation: Stronger proof systems have resisted super-polynomial lower bounds in classical proof complexity, whereas many strong non-classical systems admit exponential lower bounds.Prior intuitionistic and modal results, including Hrubeš’s and Jeřábek’s work, established a foundation for these separations.
- Motivation: Jalali’s construction transferred intuitionistic lower bounds to substructural settings but did not distinguish FLe-Extended Frege from intuitionistic Extended Frege on FLe-provable formulas.The unresolved issue was whether weaker substructural systems are genuinely less powerful on formulas already provable in FLe.
- Main result: For any structural logic L below intuitionistic logic and any logic M not contained in L, FLe-provable formulas have polynomial-size M-Frege proofs but exponentially many lines in L-Frege proofs.Exponential line lower bounds are equivalent to exponential-size lower bounds for L-Extended Frege proofs.
- Main result: The same exponential separations hold in the !-free setting, replacing ILL and FLe with IMALL and FLe respectively.The result therefore covers both exponential and !-free intuitionistic linear frameworks.
- Technical tool: A feasible disjunction property lets a polynomial-line proof of A ∨ B yield a polynomial-line proof of either A or B.The property strengthens the ordinary disjunction property by imposing polynomial control on proof growth.
- Technical tool: The separation strategy converts a lower bound for a weaker logic into a separation by adjoining an easily provable disjunct, such as B_n := A_n ∨ (⊤→1).B_n has a short IPC-Frege proof, while a short FLe-Frege proof would contradict the feasible disjunction property and the lower bound for A_n.
2 Preliminaries
The preliminaries define the languages, logics, sequents, calculi, Frege systems, proof measures, simulations, and feasible disjunction property used throughout the paper. They also establish equivalence of Frege systems for the same logic and relate sequent calculi to their induced logics.
- Languages and formulas: The unbounded language Lu contains 0, 1, ∧, ∨, ∗, and →; bounded and linear languages add ⊤, ⊥, and !, respectively.The linear language is L! = Lb ∪ {!}.
- Languages and formulas: Formulas are generated from variables, constants, exponentials, and the connectives ∧, ∨, →, and ∗; negation is defined as ¬A := A → 0.Lu- and Lb-formulas restrict this grammar to their available constants and connectives.
- Logics: A logic is a collection of formulas closed under the stipulated logical conditions, including substitution.The preliminaries introduce these closure conditions before defining consequence relations and proof systems.
- Sequent calculi: Sequents have the form Γ ⇒ ∆ with finite multisets of formulas and at most one succedent, and their interpretations convert them into implications from ∗Γ.An empty succedent is interpreted as ∗Γ → 0, while a singleton succedent is interpreted as ∗Γ → ∆.
- Sequent calculi: FLe is the base sequent calculus, and adding structural rules produces the other calculi considered in the paper.Dag-like proofs are finite sequences of sequents derived from assumptions or earlier sequents; tree-like proofs restrict premise reuse.
- Sequent calculi: The induced logic of a calculus G consists of formulas derivable as ⇒ A, and sequent derivability corresponds to derivability of its interpretation in that logic.This establishes the correspondence between sequent calculi and their associated logics.
- Frege systems: Frege proofs are finite sequences of formulas generated by inference rules, with line count l(π) bounded by proof size; Frege systems are sound and strongly complete.Standard Frege systems additionally preserve the logic’s consequence relation, and all Frege systems are assumed standard.
- Proof comparisons: For logics L ⊆ M, Q line-simulates P when P-proofs can be transformed into Q-proofs with polynomially many lines, and all Frege systems for one logic are line- and size-equivalent.Extended Frege proof size is polynomially related to the number of lines in the corresponding Frege system.
3 Structural Calculi
The section defines structural calculi by extending FLe with finite structural rules and relates these calculi to their associated logics and Frege systems. It establishes that structural calculi, tree-like versions, and Frege systems are polynomially equivalent in proof size and line count.
- The framework restricts structural rules so that each is equivalent to an axiom over FLe.
- Structural calculi extend FLe with a finite set of structural rules, and a logic is structural exactly when it has such a calculus.
- Examples include FLe, FLew, FLec, and LJb over Lu, plus systems obtained from IMALL and ILL over Lb and L!.
- Every structural logic has a Frege system, and structural rules of a calculus G are provable in LK! whenever LG is contained in LK!.
- Structural calculi for the same logic, their tree-like versions, and its Frege systems are size-equivalent and line-equivalent.
4 Feasible Disjunction Property
The section proves a feasible disjunction property for structural calculi and Frege systems below LK!, using a translation through angled atoms and polynomial-size auxiliary sequents. The construction yields polynomial-size proofs of one disjunct from proofs of a disjunction.
- Any structural calculus G with LG contained in LK! has the feasible disjunction property.From a G-proof of ⇒A ∨B, one obtains a G-proof of either ⇒A or ⇒B with polynomial line growth.
- 4.2 Feasible Disjunction Property: The resulting feasible disjunction property transfers from structural calculi to L-Frege systems through line-equivalence.
- 4.1 The Translation: The translation t converts formulas into formulas with angled atoms, making disjunctions with atomic disjuncts easier to analyze.It recursively adds angled-atom components to compound formulas and introduces fresh propositional variables corresponding to formulas.
- 4.1 The Translation: Provability preservation constructs auxiliary sequents Sπ and a G-proof σπ from any G-proof π, with auxiliary sequents restricted to Horn forms or specified exponential forms.
- 4.1 The Translation: For tree-like π, the auxiliary set has polynomial size, with |Sπ| bounded by l(π)^O(1).The size bound relies on constructing Sπ recursively over the tree-like proof.
- 4.2 Feasible Disjunction Property: Unit propagation derives either ⇒p or ⇒q from a proof of ⇒p ∨q using polynomially many lines for Horn sequents.
5 Exponential Separations
The section builds exponential lower bounds from clique-coloring formulas and uses feasible disjunction to separate Frege systems for structural and linear logics. The resulting gaps apply broadly when extending a structural logic, including cut-free systems and formulas already provable in FLe.
- 5.1 Substructural Clique-Color Formula: Negation-free variants preserve the 2^Ω(n^1/4)-line lower bound for intuitionistic proofs.Jeřábek replaces negative literals with fresh variables while retaining the lower-bound construction.
- 5.1 Substructural Clique-Color Formula: A minor adjustment makes the formulas FLe-provable, while corresponding LJ!-proofs still require at least 2^Ω(n^1/4) lines.This supplies the hard FLe-provable family used in the later separation argument.
- 5.2 Separation Results: Feasible disjunction introduction lets a proof of A_i produce a proof of A_0 ∨ A_1 with polynomial growth in proof and formula sizes.The property is available for FLeX, IMALLX, ILLX, their cut-free versions, and L-Frege systems extending FLe.
- 5.2 Separation Results: The main theorem separates L-Frege from any M-system with FLe ⊆ M and M not contained in L by adjoining a fixed formula B ∈ M − L.The formulas Θ*_n ∨ B have polynomial-size P-proofs but force short L-Frege proofs only if B were in L, contradicting its choice.
- 5.2 Separation Results: Consequently, extending structural logics can reduce Frege proof-line complexity exponentially, even for formulas already provable in FLe.The result covers FLeX, IMALLX, and ILLX, and also yields exponential gaps between corresponding cut-free systems.