皮亚诺算术

Peano 算术把 $0$、后继、加法、乘法和归纳规则写成机器可检查的一阶句子。归纳不是量化所有子集的单个二阶公理，而是让每个可由一阶公式表达的性质分别获得一个公理实例；因此 PA 有非标准模型。它又足够强，能够编码有限语法和计算，也因此进入 Gödel 不完备定理的适用范围。

公式 $x+0=x$、$x+S(y)=S(x+y)$ 递归约束加法；归纳实例可证明 $\mathrm{\forall }x(x+0=x)$ 等算术命题。二阶 Peano 公理在完整二阶语义下可范畴地刻画 $\mathbb{N}$，一阶 PA 则不能排除非标准元素；不能把二者混为一谈。PA 的公理集无限但递归可枚举。一个结构满足 PA 不意味着其外部元素都由有限次后继从 $0$ 得到；这正是非标准模型出现的空间。PA 也不包含所有在标准自然数中为真的一阶句子。

PA 可证明加法交换、每个非零数有前驱等基本算术事实。紧致性则可构造含有“比每个标准自然数都大”之元素的非标准模型，具体展示标准模型 $\mathbb{N}$ 并不唯一。相比之下，去掉乘法的 Presburger 算术可判定且完备，说明乘法显著提高了表达与证明复杂度。

自然数模型公理库自然数模型Natural numbers · Peano system由零元、后继和二阶归纳原则范畴性刻画的离散数系模型。提供标准语义，数学归纳法公理库数学归纳法Mathematical induction · Weak induction由基例和从 n 到 n+1 的归纳步推出性质对全部自然数成立。在 PA 中以公理模式出现。PA 对有限符号串、证明和算法计算的编码能力，使它成为可证明性、递归论、不完备性和形式化数学的标准基准理论；Gödel 第一不完备定理公理库哥德尔第一不完备定理Gödel's first incompleteness theorem足够强、有效公理化且一致的算术理论存在既不可证也不可否证的句子。与第二不完备定理揭示其内部限制，递归论与证明论则研究其可证明函数和一致性强度。