论文标题
跨结构逻辑的证据复杂性
Proof Complexity of Substructural Logics
论文作者
论文摘要
在本文中，我们研究了广泛的各种子结构系统的证明复杂性。对于任何证明系统，$ \ mathbf {p} $至少与全兰贝克微积分一样强，$ \ mathbf {fl} $，以及通过扩展的弗雷格系统对某些无限分支的超级启动性逻辑进行多项拟合模拟，我们对证明长度的指数较低。更确切地说，我们将提供$ \ MathBf {p} $ - 可证明的公式$ \ {a_n \} _ {n = 1}^{\ infty} $，使得最短的$ \ $ \ m athbf {p} $ - for $ a_n $ a_n $ in $ a_n $ a_n $ a_n $ a_n $ a_n的最短长度。下边界还扩展到$ \ Mathsf {fl} $和任何无限分支超级元素逻辑之间的逻辑中的任何Frege系统（扩展Frege System）中的证明线（证明长度）的数量。我们还将证明证明系统和逻辑的结果相似，扩展了Visser的基本命题演算$ \ MATHBF {BPC} $及其逻辑$ \ Mathsf {BPC} $。最后，在经典的子结构设置中，我们将在任何证明系统中通过$ \ mathbf {cfl_ {ew}} $多项式模拟的任何证明系统中的指数下限建立指数下限。
In this paper, we investigate the proof complexity of a wide range of substructural systems. For any proof system $\mathbf{P}$ at least as strong as Full Lambek calculus, $\mathbf{FL}$, and polynomially simulated by the extended Frege system for some infinite branching super-intuitionistic logic, we present an exponential lower bound on the proof lengths. More precisely, we will provide a sequence of $\mathbf{P}$-provable formulas $\{A_n\}_{n=1}^{\infty}$ such that the length of the shortest $\mathbf{P}$-proof for $A_n$ is exponential in the length of $A_n$. The lower bound also extends to the number of proof-lines (proof-lengths) in any Frege system (extended Frege system) for a logic between $\mathsf{FL}$ and any infinite branching super-intuitionistic logic. We will also prove a similar result for the proof systems and logics extending Visser's basic propositional calculus $\mathbf{BPC}$ and its logic $\mathsf{BPC}$, respectively. Finally, in the classical substructural setting, we will establish an exponential lower bound on the number of proof-lines in any proof system polynomially simulated by the cut-free version of $\mathbf{CFL_{ew}}$.
