论文标题
\ mathbb {n}上的归纳模型
Induction Models on \mathbb{N}
论文作者
论文摘要
数学诱导是计算机科学和数学的基本工具。当基本情况B设置为包含0的单例集和一单位生成函数S时，Henkin启动了数学诱导的形式化的数学诱导限制。尽管随后的研究表明几种诱导模型是等效的，但在不同诱导模型之间并不存在还原和等效性的精确逻辑表征。在本文中，我们概括了归纳模型的定义，并证明了给定B的存在和构建，反之亦然。然后，我们对不同诱导模型之间的降低进行形式表征，这些模型可以在另一个感应模型中以证明为证明。还原的概念使我们能够捕获归纳模型之间的等效性。
Mathematical induction is a fundamental tool in computer science and mathematics. Henkin initiated the study of formalization of mathematical induction restricted to the setting when the base case B is set to singleton set containing 0 and a unary generating function S. The usage of mathematical induction often involves wider set of base cases and k-ary generating functions with different structural restrictions. While subsequent studies have shown several Induction Models to be equivalent, there does not exist precise logical characterization of reduction and equivalence among different Induction Models. In this paper, we generalize the definition of Induction Model and demonstrate existence and construction of S for given B and vice versa. We then provide a formal characterization of the reduction among different Induction Models that can allow proofs in one Induction Models to be expressed as proofs in another Induction Models. The notion of reduction allows us to capture equivalence among Induction Models.
