发表机构
Bernoulli Institute, University of Groningen（格罗宁根大学伯努利研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文建立了直觉主义亚结构和线性逻辑的扩展弗雷格系统间的指数分离，构造了一类公式在不同系统中证明长度的指数差距，关键利用了L-弗雷格的可行析取性质变体。
AI 中文摘要
本文中，我们建立了一系列直觉主义亚结构逻辑和线性逻辑的扩展弗雷格系统之间的指数分离。更准确地说，对于通过扩展 ILL（直觉主义线性逻辑）加入结构规则得到的直觉主义逻辑之下的任意逻辑 L，以及不包含在 L 中的任意逻辑 M，我们构造了一族可由 FLₑ（直觉主义线性逻辑的一个子结构逻辑）证明的公式，这些公式在 M-弗雷格系统中有短证明，但在 L-扩展弗雷格系统中需要指数级大小的证明。在无!（模态算子）的情形下，使用 IMALL（直觉主义乘法加法线性逻辑）和 FLₑ 替代 ILL，该结论同样成立。证明这些分离的关键要素是 L-弗雷格的可行析取性质的一个变体，该变体可能具有独立研究价值。
英文摘要
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.
Comments25 pages
