皮亚诺算术

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的轨迹，把外部计算记录与内部任意见证的唯一性分别核对。这里的一族逐输入证明须与一个统一的全称总性定理区分；非标准模型使这种区别具有实际意义。