Visser's rules have an essential role in intermediate logics. They form a basis for the admissible rules of intuitionistic logic and any intermediate logic in which they are admissible. In this paper, we follow the universal proof theory program introduced and developed in [1, 2, 24, 25] to establish a connection between the form of the rules in a sequent calculus for an intuitionistic modal logic and the admissibility of Visser's rules in that logic. More precisely, by investigating the form of the constructively acceptable rules, we first introduce a very general family of rules called the constructive rules. Then, defining a constructive sequent calculus as a calculus consisting of constructive rules and some basic modal rules, we prove that any constructive sequent calculus stronger than $\mathbf{CK}$ 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. This connection has two types of applications. On the positive side, it proves the feasible admissibility of Visser's rules in the sequent system for several intuitionistic modal logics, including $\mathsf{CK}$, $\mathsf{IK}$, their extensions by the usual modal axioms of $T$, $B$, $4$, $5$, the modal axioms of bounded width and depth and the propositional lax logic. On the negative side, though, it shows that if an intuitionistic modal logic satisfying a mild technical condition does not admit Visser's rules, then it cannot have a constructive sequent calculus.
翻译:Visser的规则在中间逻辑中具有不可或缺的作用。 它们构成了可接受直觉逻辑规则和任何中间逻辑的可接受性规则的基础。 在本文中, 我们遵循了[1、2、 24、 25] 中引入和发展的通用证据理论程序, 以建立规则形式在直觉模式逻辑的序列计算法中与Visser的规则在逻辑中可接受性之间的关联。 更确切地说, 通过调查建设性可接受的规则的形式, 我们首先引入了一个非常普遍的规则体系, 称为建设性规则。 然后, 定义一个建设性的序列计算法, 由建设性规则和一些基本模式规则组成的计算法。 我们证明, 任何建设性的序列计算法形式在[1、2、 24、 25] 中都比 美元更强, 满足了一种温和的技术条件, 也就是说, 有一种混合时间算法, 可以证明 Vissers的假设值是价值 。