Skip to content
DraconiticResearch
Search Sources API
186,123 studies31 sourcesUpdated 32 min ago
PreprintCC BY 4.0arXiv

Exponential Gaps Between Intuitionistic Linear Extended Frege Systems

  • Amirhossein Akbar Tabatabai
Open at sourcePDFDOICite

Abstract

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 ILL with structural rules, and any logic M not contained in L, we construct a family of FLe-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 IMALL and FLe in place of 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.

Related

  1. Extended Frege proofs, circuits and rewriting
    Jan Krajicek
    arXivPreprintCC BY 4.0Full textLogic & foundationsarXiv
  2. From detectability of abstract linear systems to exponential output-to-state stability and back
    Qiaoling Chen, Andrii Mironchenko, Fabian Wirth
    arXivPreprintarXiv licenceFull textOptimisation & controlarXiv
  3. Pseudo-solutions of polynomial systems and the lower bound problem for AC0[p]-Frege systems
    Jan Krajicek
    arXivPreprintCC BY 4.0Full textLogic & foundationsarXiv
  4. Almost sure exponential stabilization of linear stochastic systems driven by a general α-stable process via discrete-time state feedback
    Xuekang Zhang
    arXivPreprintarXiv licenceFull textProbabilityarXiv
  5. A New Extended Exponential Rayleigh Distribution: Estimation and Application
    Dinesh Kumar, Omprakash Prajapati, Sultan Parveen +1
    Reliability: Theory & ApplicationsPeer-reviewedCC BY-NCFull textStatisticsDOAJ

Cite

BibTeXRIS
BibTeX
@misc{tabatabai2026exponential,
  title = {{Exponential Gaps Between Intuitionistic Linear Extended Frege Systems}},
  author = {Amirhossein Akbar Tabatabai},
  howpublished = {arXiv},
  year = {2026},
  month = sep,
  doi = {10.48550/arxiv.2609.00422},
  eprint = {2609.00422},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2609.00422},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - Exponential Gaps Between Intuitionistic Linear Extended Frege Systems
AU  - Amirhossein Akbar Tabatabai
PY  - 2026
DA  - 2026/09/01
PB  - arXiv
DO  - 10.48550/arxiv.2609.00422
UR  - https://arxiv.org/abs/2609.00422
AB  - 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 ILL with structural rules, and any logic M not contained in L, we construct a family of 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 IMALL and FL_e in place of 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.
ER  -