逻辑引擎

自然数的Peano公理系统

下面是不引入集合概念的Peano公理系统。由于不引入集合概念，所以归纳公理必须使用二阶逻辑，对任意属性谓词进行量化。

先引入相等关系（同一关系）的定义：
eq0. $\forall a$ . $a=a$ 自反性（reflexive）
eq1. $\forall a,b$ . $a=b \Rightarrow b=a$ 对称性（symmetric）
eq2. $\forall a,b,c$ . $a=b \wedge b=c \Rightarrow a=c$ 传递性（transitive）
eq3. $\forall P,a,b$ . $a=b \Rightarrow (P(a)\Rightarrow P(b))$ 相等则具有相同属性。

利用上述相等关系定义，这里给出不依赖于集合论只基于二阶逻辑的自然数Peano公理：
n0. $N(0)$ 0是自然数
n1. $\forall a$ . $N(a) \Rightarrow N(S(a))$ 自然数的后继也是自然数
n2. $\forall a,b$ . $N(a) \wedge N(b) \Rightarrow (S(a)=S(b) \Rightarrow a=b)$ 仅当两自然数相等后继才可能相等
n3. $\forall a$ . $N(a) \Rightarrow \sim 0=S(a)$ 0不是任何自然数的后继
n4. $\forall P,a$ . $P(0) \wedge (N(a) \Rightarrow (P(a) \Rightarrow P(S(a))) \Rightarrow (\forall b. N(b) \Rightarrow P(b))$ 归纳公理的二阶逻辑版本。对于任意属性P和任意自然数a，如果【a)0具有属性P，b)只要a具有属性P则a的后继也具有属性P】，那么任意自然数都具有属性P。如果引入集合概念就可以只用一阶逻辑。