公理化、算术与语法

设$\mathcal{T}$$\mathcal{T}$为一个公式集合。 定义$\mathcal{T}$$\mathcal{T}$是蕴含封闭的(Closed under Logical Consequence),当且仅当对于所有公式$A$$A$, 如果$\mathcal{T}\models A$$\mathcal{T} \models A$,那么 $A\in \mathcal{T}$$A \in \mathcal{T}$.

一个蕴含封闭的公式集合称为一个理论(Theory).

$\mathcal{T}$$\mathcal{T}$中的元素称为定理(Theorems).

理论可以这样构造：选择一些公式, 作为公理(Axioms), 然后按照蕴含关系推导出其它公式。

设$\mathcal{T}$$\mathcal{T}$为一个理论。 $\mathcal{T}$$\mathcal{T}$称为可公理化(Axiomatizable)的,当且仅当存在一个公式集合$\mathcal{U}$$\mathcal{U}$, 使得$\mathcal{T}=\{A|\mathcal{U}\models A\}$$\mathcal{T}=\{A|\mathcal{U}{\models}A\}$. 这个公式集合$\mathcal{U}$$\mathcal{U}$就是$\mathcal{T}$$\mathcal{T}$的公理。

如果$\mathcal{U}$$\mathcal{U}$是有限的, 称$\mathcal{T}$$\mathcal{T}$是可有限公理化(Finitely Axiomatizable)的。

皮耶罗公理(Peano Axioms),又称戴德金-皮耶罗公理,定义了自然数的算术属性。

下面定义的算术语言是皮耶罗公理的增强版。

一个算术语言(Language of Arithmetic, ${\mathcal{L}}^{\star }$$\mathcal{L}^\star$)包括:

• 常数0
• 二元关系$<$$<$
• 一元函数$s()$$s()$
• 二元函数$+$$+$
• 二元函数$\times$$\times$.

算术语言的标准解释是${\mathcal{N}}^{\star }$$\mathcal{N}^\star$,个体域是自然数。

• $0^{{\mathcal{N}}^{\star }}$$0^{\mathcal{N}^\star}$是常数0;
• ${<}^{{\mathcal{N}}^{\star }}$$<^{\mathcal{N}^\star}$是普通的小于;
• $s^{{\mathcal{N}}^{\star }}(x)=x+1$$s^{\mathcal{N}^\star}(x)=x+1$是一元函数,如:$s(s(0))=2$$s(s(0))=2$;
• ${+}^{{\mathcal{N}}^{\star }}$$+^{\mathcal{N}^\star}$和${\times }^{{\mathcal{N}}^{\star }}$$\times^{\mathcal{N}^\star}$是普通的加法和乘法。

算术语言也可以有其它解释,如 ${\mathcal{Q}}^{\star }$$\mathcal{Q}^\star$,个体域是非负有理数。

• $0^{{\mathcal{Q}}^{\star }}$$0^{\mathcal{Q}^\star}$是常数0;
• ${<}^{{\mathcal{Q}}^{\star }}$$<^{\mathcal{Q}^\star}$是普通的小于;
• $s^{{\mathcal{Q}}^{\star }}(x)=x+1$$s^{\mathcal{Q}^\star}(x)=x+1$;
• ${+}^{{\mathcal{Q}}^{\star }}$$+^{\mathcal{Q}^\star}$和${\times }^{{\mathcal{Q}}^{\star }}$$\times^{\mathcal{Q}^\star}$是普通的加法和乘法。

或者解释为${\mathcal{P}}^{\star }$$\mathcal{P}^\star$,个体域是非负半整数:$0$$0$, $\frac{1}{2}$$\frac{1}{2}$, $1$$1$, $1\frac{1}{2}$$1\frac{1}{2}$, 2, $2\frac{1}{2}$$2\frac{1}{2}$, $\cdots$$\cdots$

• $0^{{\mathcal{P}}^{\star }}$$0^{\mathcal{P}^\star}$是常数0;
• ${<}^{{\mathcal{P}}^{\star }}$$<^{\mathcal{P}^\star}$是普通的小于;
• $s^{{\mathcal{P}}^{\star }}(x)=x+1$$s^{\mathcal{P}^\star}(x)=x+1$;
• ${+}^{{\mathcal{P}}^{\star }}$$+^{\mathcal{P}^\star}$是普通的加法;
• ${\times }^{{\mathcal{P}}^{\star }}$$\times^{\mathcal{P}^\star}$未定义。

不同的解释、不同的公理化体系会使与算术相关的一阶逻辑公式具有不同的可满足性。

例如:

${\phi }_1$$\varphi_1$: $\mathrm{\forall }x\mathrm{\exists }y\{(x<y)\wedge \mathrm{\neg }\mathrm{\exists }z[(x<z)\wedge (z<y)]\}$$\forall x\exists y\{(x < y)\land \lnot \exists z[(x <z)\land (z< y)]\}$

${\phi }_2$$\varphi_2$: $\mathrm{\forall }x\{[x<s(x)]\wedge \mathrm{\neg }\mathrm{\exists }z[(x<z)\wedge (z<s(x))]\}$$\forall x\{[x < s(x)] \land \lnot \exists z[(x <z) \land (z< s(x))]\}$

接下来是关于语言语法的形式化表达。

1.变量

$v_0,v_1,v_2,\cdots$$v_0,\,\,v_1,\,\,v_2,\,\,\cdots$

例如: $x$$x$是$v_0$$v_0$, $y$$y$是$v_1$$v_1$.

2.谓词(关系)

$A_0^1,A_1^1,A_2^1,\cdots$$A_0^1,\,\,A_1^1,\,\,A_2^1,\,\,\cdots$

$A_0^2,A_1^2,A_2^2,\cdots$$A_0^2,\,\,A_1^2,\,\,A_2^2,\,\,\cdots$

$A_0^3,A_1^3,A_2^3,\cdots$$A_0^3,\,\,A_1^3,\,\,A_2^3,\,\,\cdots$​

$\cdots ,\cdots ,\cdots ,\cdots$$\cdots,\,\,\cdots,\,\,\cdots,\,\,\cdots$

例如: $\{<\}$$\{<\}$ is $\{A_0^2\}$$\{A_0^2\}$

3.常数与函数

$f_0^0,f_1^0,f_2^0,\cdots$$f_0^0,\,\,f_1^0,\,\,f_2^0,\,\,\cdots$

$f_0^1,f_1^1,f_2^1,\cdots$$f_0^1,\,\,f_1^1,\,\,f_2^1,\,\,\cdots$

$f_0^2,f_1^2,f_2^2,\cdots$$f_0^2,\,\,f_1^2,\,\,f_2^2,\,\,\cdots$

$f_0^3,f_1^3,f_2^3,\cdots$$f_0^3,\,\,f_1^3,\,\,f_2^3,\,\,\cdots$

$\cdots ,\cdots ,\cdots ,\cdots$$\cdots,\,\,\cdots,\,\,\cdots,\,\,\cdots$​​

例如: $\{0,s(),+,\times \}$$\{0,s(), +,\times\}$ is $\{f_0^0,f_0^1,f_0^2,f_1^2\}$$\{f_0^0,f_0^1, f_0^2,f_1^2\}$

公式的形式化表达:

$x<1$$x<1$:

$A_0^2(v_0,f_0^1(f_0^0))$$\,\,A_0^2(v_0,f_0^1(f_0^0))$

$2x+1$$2x+1$:

$f_0^2(f_1^2(f_0^1(f_0^1(f_0^0)),v_0),f_0^1(f_0^0))$$\,\,f_0^2(f_1^2(f_0^1(f_0^1(f_0^0)),v_0),f_0^1(f_0^0))$