AI 中文总结
该研究提出了直觉模态逻辑IK4的Kruskal判定程序，通过无切嵌套证明结合Kruskal定理等证明其可判定性，给出了统一的证明高度界。
AI 中文摘要
我们通过直接使用无切嵌套证明来证明Simpson提出的直觉模态逻辑IK4的可判定性。一旦固定了结束公式，节点处仅会出现有限多的输入和输出公式组合，尽管模态树本身仍然是无界的。我们通过根同胚嵌入对这些嵌套矢列进行排序：弱化可添加输入公式，而传递性允许将模态边拉伸为非空路径。Kruskal定理使根同胚嵌入成为一个良拟序，但这本身并不能使规则的反向应用有效：推理仍可能发生在任意大的上下文中。有限支撑引理表明，最小前驱仅需保留推理所用的位置、所选基元的像以及连接它们的分支点。结合有界规则实例的有效枚举，该界使得最小前驱可计算。从初始矢列进行反向闭包运算会得到一个由有限基向上闭包集组成的递增序列。该序列最终会稳定下来，其稳定值即为可证明的嵌套矢列集合。此时，仅需有限多的无切证明：每个其他可证明的嵌套矢列都可通过沿嵌入进行弱化从其中一个得到。它们的最大高度给出了统一的证明高度界。
英文摘要
We prove decidability of Simpson's intuitionistic modal logic IK$ by working directly with cut-free nested proofs. Once the end formula is fixed, only finitely many combinations of input and output formulae can occur at a node, although the modal tree itself remains unbounded. We order these nested sequents by rooted homeomorphic embedding: weakening may add input formulae, while transitivity allows a modal edge to be stretched into a non-empty path. Kruskal's theorem makes rooted homeomorphic embedding a well-quasi-order, but does not by itself make backward application of the rules effective: an inference may still occur inside an arbitrarily large context. The finite-support lemma shows that a minimal predecessor need retain only the positions used by the inference, the images of the chosen basis elements, and the branch points joining them. Together with an effective enumeration of bounded rule instances, this bound makes the minimal predecessors computable. Backward closure from the initial sequents gives an increasing sequence of finitely based upward-closed sets. The sequence eventually stabilises, and its stable value is the set of provable nested sequents. At that point, finitely many cut-free proofs suffice: every other provable nested sequent is obtained from one of them by weakening along an embedding. Their maximum height gives a uniform proof-height bound.
Comments24
