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.
翻译:本文提出了一种关于直觉主义逻辑与模态逻辑系统的Π₂规则的一般理论。我们引入了Π₂规则系统与归纳类的概念,并建立了模型论与代数完备性定理,这些构成了我们的基本工具。作为一般理论的例证,我们从结构理论与逻辑的视角分析了哥德尔代数归纳类的结构。研究表明,与其他已深入研究的体系(如逻辑系统或单结论规则系统)不同,扩展𝖫𝖢=𝖨𝖯𝖢+(𝑝→𝑞)∨(𝑞→𝑝)的Π₂规则系统具有连续统基数,并展示了我们的方法如何简化著名Takeuti-Titani规则可采纳性的证明。最终结果涉及𝖫𝖢中可采纳性的一般性问题:(1)我们完整分类了那些归纳完备的归纳类,即所有可采纳的Π₂规则皆可推导的类;(2)证明了𝖫𝖢上Π₂规则的可采纳性问题是可判定的。