二阶算术

在二阶逻辑中将皮亚诺公理形式化而得的形式算术理论，记作S。一阶皮亚诺算术PA是不完全的，并且是不可完全的，也就是说，没有一个公理系统在其中能证明PA的所有真的公式而又不证明一个假的公式。寻找一个扩张PA的系统，在其中能证明更多的关于自然数的结果，是一件很自然的事。二阶算术就是一个能证明更多的PA的真公式的系统。二阶算术S建立在二阶逻辑基础上。二阶逻辑是在一阶语言中增加谓词变元，并且量词可以约束谓词变元，在一阶逻辑的公理和推理规则基础上增加关于二阶量词的公理和规则(在形式上与一阶逻辑中关于量词的公理和规则相似)。S的语言的非逻辑符号是个体常元0和后继运算符号′。S的非逻辑公理是下面的三条，它们是皮亚诺公理的形式化：

公理3是归纳公理，其中的X是谓词变元。公理3和PA中的归纳公理模式不同，公理3是单独一个公理，而PA的归纳公理是个模式，代表无穷个公理。

自然数结构N=(N，′，0)是S的模型。S的任一模型都与N同构，即皮亚诺公理是范畴的。关于二阶算术S，简单介绍下面几个结果。①PA的每一定理都是在S中可证的。②在S中可以证明PA的协调性，即表达PA协调性的公式Con(PA)在S是可证的(Con(PA)是不能在PA中证明的)。有在PA中不可证明的PA的真公式，在S中是可证的。③可以在S中定义PA的真公式，即在S中有一个含一个自由个体变元的公式Tr(x)，以表示PA的公式A的哥德尔数，在S中可以证明：(Tr)A。①不是所有PA的真公式都是在S中可证明的。⑤推理规则：从A(0)，A(1)，A(2)，…可推出xA(x)，称为ω-规则。ω－规则有无穷多个前提。把ω-规则加到S中而得的系统记作S。存在S的真公式是在S中不可证明的。