皮亚诺算术

Peano 算术把 $0$、后继、加法、乘法和归纳规则写成机器可检查的一阶句子。归纳不是量化所有子集的单个二阶公理，而是让每个可由一阶公式表达的性质分别获得一个公理实例。非标准模型的存在可这样证明：在语言中加入常元 $c$ 及所有要求 $c>\overline{n}$（$n=0,1,2,\dots$），其中 $\overline{n}=S^{n}0$ 是标准数码。任意有限子集只涉及有限多个下界，在 $\mathbb{N}$ 中把 $c$ 解释成更大的自然数便可满足。紧致性给出满足全部要求的模型，其中 $c$ 大于每个标准数码，故不是标准自然数模型。它又足够强，能够编码有限语法和计算，也因此进入 Gödel 不完备定理的适用范围。

公式 $x+0=x$、$x+S(y)=S(x+y)$ 递归约束加法；取 $\phi (x)$ 为 $0+x=x$，可用归纳证明 $\mathrm{\forall }x(0+x=x)$：基步 $0+0=0$ 来自第一条公理；若 $0+x=x$，则第二条给出 $0+Sx=S(0+x)=Sx$，完成后继步。

二阶 Peano 公理在完整二阶语义下可范畴地刻画 $\mathbb{N}$，一阶 PA 则允许非标准元素：从外部看，模型中的某些元素不是从 $0$ 经有限次后继得到的。PA 的公理集无限但递归可枚举；标准自然数中全部一阶真句组成的理论则无法有效公理化。

PA 可证明加法交换、每个非零数有前驱等基本算术事实。紧致性则可构造含有“比每个标准自然数都大”之元素的非标准模型，具体展示标准模型 $\mathbb{N}$ 并不唯一。相比之下，Presburger 算术理路Presburger 算术Presburger arithmetic · 加法算术 · 线性整数算术在加法与序的整数约束中，通过系数统一和有限余数检验消去量词，并判定自然数加法算术。只保留加法语言，并把归纳模式也限制到这个语言；其有效公理系统完备且可判定。加入固定模数的同余谓词后，线性约束可通过有限余数检验消去量词，例如把 $\mathrm{\exists }x(y\le 2x\le y+3\wedge x\equiv 1(\mathrm{mod}3))$ 化为 $y$ 模六属于 $0,1,2,5$ 四类。

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

编码计算与内部证明之间的接口是算术可表示性理路算术可表示性Arithmetical representability以β余数编码有限计算序列，完整证明原始递归函数的PA逐输入唯一表示，并区分外部编码与内部统一总性。：该页从余数唯一性与β编码出发，给出零函数、后继、投影、复合和原始递归的全部构造；对每个标准输入，理论能证明具体输出及该输入下的唯一性。1394与6编码1、3、7的轨迹，把外部计算记录与内部任意见证的唯一性分别核对。这里的一族逐输入证明须与一个统一的全称总性定理区分；非标准模型使这种区别具有实际意义。