皮亚诺算术
书籍:逻辑百科辞典
皮亚诺公理在一阶逻辑中形式化而得的理论，也称一阶皮亚诺算术，在文献中通常记作PA。它是自然数算术的形式化理论，因此也称为形式算术、形式数论。皮亚诺公理中包括三个初始概念：0，数，后继。在形式化的系统中，在初始概念中，“数”这一概念是不必要的，但增加了两个二元函数符号+和·，因为在PA的形式公理中包括+和·的递归定义等式。皮亚诺公理有5条，其中的两条：0是数，一数的后继仍是数，在PA中由项形成规则取代了。其它三条公理中，归纳公理不能在一阶逻辑中形式化，在PA中是一个公理模式，同时增加关于+和·的4个定义等式作公理。PA的公理有7条(其中符号′表示后继)：
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(x)是PA语言中的任意公式。(参见皮亚诺公理，形式算术。)