形式陈述

皮亚诺算术（PA）是语言 $L_{PA}=\{0,S,+,\times\}$$L_{PA}=\{0,S,+,\times \}$（可扩充 $<$$<$）中的一阶理论。其有限基本公理规定后继单射、$0$$0$ 不是后继，并递归刻画加法与乘法；此外对每个一阶公式 $\varphi(x,\bar y)$$\phi (x,\overline{y})$ 都含一个归纳公理实例

$$ \bigl(\varphi(0,\bar y)\land\forall x(\varphi(x,\bar y)\to\varphi(Sx,\bar y))\bigr) \to\forall x\,\varphi(x,\bar y). $$$$(\phi (0,\overline{y})\wedge \mathrm{\forall }x(\phi (x,\overline{y})\to \phi (Sx,\overline{y})))\to \mathrm{\forall }x\phi (x,\overline{y}).$$

因此归纳是可有效枚举的公理模式，不是一阶语言中的单个量化公理。标准自然数结构 $\mathbb N$$\mathbb{N}$ 是 PA 的模型，但由紧致性和 Löwenheim–Skolem，PA 也有非标准模型。

直觉

PA 把自然数运算的规则写成机器可检查的一阶句子；归纳模式允许每个可由一阶公式表达的性质分别获得一次归纳原则。

例子与边界

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

推论与应用

PA 是可证明性、递归论、不完备性和形式化数学的标准基准理论；其编码能力足以在理论内部表示有限符号串、证明与算法计算。

参考资料

• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001，Ch. 3, formal arithmetic and induction schemata。
• Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas, Mathematical Logic, 2nd ed., Springer, 1994，Chs. 2–3, first-order arithmetic and arithmetization。