Exponential Gaps Between Intuitionistic Linear Extended Frege Systems
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2609.00422
curl -X POST /api/v1/records/arxiv/2609.00422/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2609.00422/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'