论文标题
通用证据理论：直觉模态逻辑中的可行性
Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal Logics
论文作者
论文摘要
在本文中，我们在模态语言及其片段上介绍了一个序列式的微积分家族，以捕获所有可建设性可接受的系统的本质。称这些计算\ emph {建设性}，我们表明，任何足够强的建设性序列的微积分满足了轻度的技术条件，可行地承认所有Visser的规则，即，有一个多项式时间算法，可以读取Visser规则的前提的证明，并提供了其结论的证据。作为一个积极的应用，我们在几个依次的直觉模态逻辑中显示了维瑟（Visser）规则的可行性，包括$ \ mathsf {ck} $，$ \ mathsf {iksf {ik} $及其通过模式axioms $ t $，$ b $，$ 4 $，$ 4 $，$ 5 $，$ 5 $，$ 5 $，$ 5 $，$ 5 $ $，$ 5 $ $，$ 5 $ $ $，纽约的范围和纽约。在负面的一面，我们表明，如果足够强大的直觉模态逻辑（满足温和的技术条件）不会承认至少一个维瑟的规则，那么它就无法具有建设性的序列序列。因此，除$ \ Mathsf {ipc} $外，没有其他中间逻辑具有建设性的序列计算。
In this paper, we introduce a general family of sequent-style calculi over the modal language and its fragments to capture the essence of all constructively acceptable systems. Calling these calculi \emph{constructive}, we show that any strong enough constructive sequent calculus, satisfying a mild technical condition, feasibly admits all Visser's rules, i.e., there is a polynomial time algorithm that reads a proof of the premise of a Visser's rule and provides a proof for its conclusion. As a positive application, we show the feasible admissibility of Visser's rules in several sequent calculi for intuitionistic modal logics, including $\mathsf{CK}$, $\mathsf{IK}$ and their extensions by the modal axioms $T$, $B$, $4$, $5$, the modal axioms of bounded width and depth and the propositional lax logic. On the negative side, we show that if a strong enough intuitionistic modal logic (satisfying a mild technical condition) does not admit at least one of Visser's rules, then it cannot have a constructive sequent calculus. Consequently, no intermediate logic other than $\mathsf{IPC}$ has a constructive sequent calculus.
