In this paper we present a general theory of $\Pi_{2}$-rules for systems of intuitionistic and modal logic. We introduce the notions of $\Pi_{2}$-rule system and of an Inductive Class, and provide model-theoretic and algebraic completeness theorems, which serve as our basic tools. As an illustration of the general theory, we analyse the structure of inductive classes of G\"{o}del algebras, from a structure theoretic and logical point of view. We show that unlike other well-studied settings (such as logics, or single-conclusion rule systems), there are continuum many $\Pi_{2}$-rule systems extending $\mathsf{LC}=\mathsf{IPC}+(p\rightarrow q)\vee (q\rightarrow p)$, and show how our methods allow easy proofs of the admissibility of the well-known Takeuti-Titani rule. Our final results concern general questions admissibility in $\mathsf{LC}$: (1) we present a full classification of those inductive classes which are inductively complete, i.e., where all $\Pi_{2}$-rules which are admissible are derivable, and (2) show that the problem of admissibility of $\Pi_{2}$-rules over $\mathsf{LC}$ is decidable.
翻译:本文提出了一种关于直觉主义逻辑与模态逻辑系统的Π₂-规则的一般理论。我们引入了Π₂-规则系统与归纳类的概念,并建立了模型论与代数完备性定理,这些构成了我们的基础工具。作为该一般理论的示例,我们从结构理论与逻辑视角分析了哥德尔代数归纳类的结构。我们证明,与其他已深入研究的情形(如逻辑系统或单结论规则系统)不同,存在连续统多个扩展𝖫𝖢 = 𝖨𝖯𝖢 + (p → q) ∨ (q → p)的Π₂-规则系统,并展示了我们的方法如何能够简洁地证明著名的武俊-谷规则的可采纳性。我们的最终结果涉及𝖫𝖢中可采纳性的一般性问题:(1)我们完整分类了那些归纳完备的归纳类,即其中所有可采纳的Π₂-规则均为可推导的;(2)证明了𝖫𝖢上Π₂-规则的可采纳性问题是可判定的。