形式算术

又称形式数论，是初等数论(自然数算术)形式化而得的形式理论。形式算术的语言的初始符号包括个体常元0，一元函数符号′(后继)，二元函数符号+，·以及逻辑符号(包括等词=)。个体常元0和个体变元是项；如果s，t是项，则s′，s+t，s·t是项。形如s=t的表达式，称为原子公式，其中s，t为项。其它的公式由原子公式应用命题联结词和量词构成。系统中的公式称为算术公式。形式算术的公理，除逻辑公理(包括等词公理)外，包括下列非逻辑公理：

1．x′=0。

2．x′=y′→x=y。

3．x+0=x。

4．x+y′=(x+y)′。

5．x·0=0。

6．x·y′=(x·y)+x。

7．归纳公理

A(0)∧x(A(x)→A(x′))→xA(x)。

归纳公理是公理模式，其中的A为算术公式，称为归纳公式。

如果形式算术系统的逻辑公理为一阶逻辑公理，该形式算术系统称为(一阶)皮亚诺算术，记为PA。如果系统的逻辑公理为直觉主义逻辑公理，就称为直觉主义算术。(关于逻辑符号，项和公式的定义，逻辑公理，参看一阶逻辑和直觉主义逻辑。)

初等数论定理(即不用数学分析的工具可证的数论定理)都在PA中可陈述和证明。PA与去掉无穷公理的ZF系统(策尔梅洛－弗兰克尔集合论系统)等价：一个系统可在另一系统中构造模型。形式算术系统的推导力可用序数ε(等式=ε的最小解)来刻划。在形式算术系统中可以推导直到任何序数α＜ε的超穷归纳模式，但不能推导直到ε的超穷归纳。原始递归函数都可在形式算术系统中表示(原始递归函数的定义等式都在形式算术系统中可证)。因此形式算术满足哥德尔不完全性定理：它是不完全的，即存在系统中的公式A，A和它的否定A都不可证；系统的协调性不能在系统自身中证明。1977年，J．帕里斯等人发现加强形式有穷型拉姆齐定理在PA中是不可证的。

形式算术系统的协调性是证明论研究的重要课题。W．阿克曼证明对归纳公理加上限制(归纳公式中无量词)的PA系统是协调的。G．根岑使用直到ε的超穷归纳证明PA是协调的。

带自由变元的形式算术公式定义数论谓词。不含自由变元的公式(闭公式)表达命题。可用一个形式算术的公式定义的数论谓词称为算术的。并不是数论谓词都是算术的。A．塔尔斯基证明，算术“真语句”这一谓词在形式算术中是不可定义的，即不存在一个含一个自由变元的公式T(x)，使得T()成立当且A是真的，其中是A的哥德尔数。令Φ为PA的至多有n个逻辑符号的闭公式的集合，则对Φ是有真定义(truth definition)的，即有一个PA的公式T(x)，使得对Φ的每一语句A，T()A在PA中是可证的。应用公式T(x)可以证明形式算术不是有穷可公理化的，即归纳公理模式是不能用有穷多个公式来表达的。