{"id":"arxiv/2609.00422","url":"https://arxiv.org/abs/2609.00422","tags":["cs.LO","math.LO"],"score":0,"title":"Exponential Gaps Between Intuitionistic Linear Extended Frege Systems","domain":"cs.LO","source":"arxiv","authors":["Amirhossein Akbar Tabatabai"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-08-31","reactions":{}}