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.
翻译:本文提出了直觉主义和模态逻辑系统中$Π_{2}$-规则的一般理论。我们引入了$Π_{2}$-规则系统与归纳类的概念,并提供了作为基本工具的模型论和代数完备性定理。作为一般理论的例证,我们从结构理论和逻辑角度分析了哥德尔代数归纳类的结构。研究表明,与其他已充分研究的设定(如逻辑系统或单结论规则系统)不同,存在连续统多个扩展$\mathsf{LC}=\mathsf{IPC}+(p\rightarrow q)\vee (q\rightarrow p)$的$Π_{2}$-规则系统,并展示了我们的方法如何能够轻松证明著名的Takeuti-Titani规则的可容许性。最终结果涉及$\mathsf{LC}$中可容许性的一般问题:(1)我们给出了那些归纳完备——即所有可容许的$Π_{2}$-规则都是可推导的——的归纳类的完整分类;(2)证明了$\mathsf{LC}$上$Π_{2}$-规则的可容许性问题是可判定的。