数理逻辑

数理逻辑是数学的一个分支，其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。

数理逻辑的研究范围是逻辑中可被数学模式化的部分。以前称为符号逻辑（相对于哲学逻辑），又称元数学，后者的使用现已局限于证明论的某些方面。

历史

“数理逻辑”的名称由皮亚诺（Peano）首先给出，他又称其为符号逻辑。数理逻辑在本质上依然是亚里士多德的逻辑学，但从记号学的观点来讲，它是用抽象代数来记述的。

某些哲学倾向浓厚的数学家对用符号或代数方法来处理形式逻辑作过一些尝试，比如说莱布尼兹和兰伯特（Johann Heinrich Lambert）；但他们的工作鲜为人知，后继无人。直到19世纪中叶，乔治·布尔和其后的奥古斯都·德·摩根才提出了一种处理逻辑问题的系统性的数学方法（当然不是定量性的）。

亚里士多德以来的传统逻辑得到改革和完成，由此也得到了研究数学基本概念的合适工具。虽然这并不意味着1900年至1925年间的有关数学基础的争论已有了定论，但这“新”逻辑在很大程度上澄清了有关数学的哲学问题。

传统的逻辑研究（参见逻辑论题列表）较偏重于“论证的形式”，而当代数理逻辑的态度也许可以被总结为对于内容的组合研究。它同时包括“语法”（例如，从一形式语言把一个文字串传送给一编译器程序，从而转写为机器指令）和“语义”（在模型论中构造特定模型或全部模型的集合）。

数理逻辑的里程碑式著作有哥特洛布·弗雷格（Gottlob Frege）的《概念文字》（Begriffsschrift）和伯特兰·罗素的《数学原理》（Principia Mathematica）。

数理逻辑论的体系

数理逻辑的主要分支包括：模型论、证明论、递归论和公理化集合论。数理逻辑和计算机科学有许多重合之处，这是因为许多计算机科学的先驱者既是数学家、又是逻辑学家，如阿兰·图灵,邱奇等。

程序语言学、语义学的研究从模型论衍生而来，而程序验证则从模型论的模型检测衍生而来。

柯里－霍华德同构给出了“证明”和“程序”的等价性，这一结果与证明论有关，直觉逻辑和线性逻辑在此起了很大作用。λ演算和组合子逻辑这样的演算现在属于理想程序语言。

计算机科学在自动验证和自动寻找证明等技巧方面的成果对逻辑研究做出了贡献，比如说自动定理证明和逻辑编程。

一些基本结果

一些重要结果是：

• 一阶公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说，证明集合是原始递归的。实质上，这就是哥德尔完备性定理，虽然那个定理的通常陈述使它与算法之间的关系不明显。

• 有效的一阶公式的集合是不可计算的，也就是说，不存在检测普遍有效性的算法。尽管以下算法存在：对此算法输入一个一阶公式，如果这个一阶公式是普遍有效的，那么算法将在某一时刻停机，如果不是普遍有效的，那么算法将会永远不停地计算下去。然而，即使算法已经运行了亿万年，公式是否有效仍是未知数。换句话说，这一集合是“递归枚举的”，用更通俗的话来讲，是“半可判定的”。

• 普遍有效的二阶公式的集合甚至不是递归可枚举的。这是哥德尔不完备定理的一个结果。

• 勒文海姆-斯科伦定理。

• 相继式演算中的切消定理。

• 保罗·科恩（Paul Cohen）在1963年证明的连续统假设的独立性。

技术参考

一阶语言和结构

定义 一阶语言 ${\mathfrak {L}}\,$ 是一组独特的印刷上的符号，分类如下:

1. 等价符号 $=\,$；连结词 $\lor \,$，$\lnot \,$；全称量词 $\forall \,$ 和圆括号 $(\,$，$)\,$。
2. 变量符号的可数集合 $\{v_{i}\}_{i=0}^{\infty }\,$。
3. 常量符号的集合 $\{c_{\alpha }\}_{\alpha \in \mathrm {A} }\,$。
4. 函数符号的集合 $\{f_{\beta }\}_{\beta \in \mathrm {B} }\,$。
5. 关系符号的集合 $\{R_{\gamma }\}_{\gamma \in \Gamma }\,$。

所以，要指定一个语言，通常只指定一组常量符号、函数符号和关系符号就足够了，因为第一组符号是标准的。圆括号只充当形成符号的群组的目的，在公式中书写函数和关系的时候被非形式的使用。

这些符号就是符号。它们不代表任何东西。他们不意味任何事物。加入语义和语言学要点对数学语言的形式化是没有用的。

因为确实需要在这些形式化之外获得某些意义。在语言之上的模型的概念就提供着这种语义。

定义 在语言 ${\mathfrak {L}}\,$ 上的 ${\mathfrak {L}}\,$-结构是由非空集合 $A\,$ 构成的包(bundle)，它是结构的全集，包括了:

1. 对于来自 ${\mathfrak {L}}\,$ 的每个常量符号 $c\,$，有一个元素 $c^{\mathfrak {A}}\in A\,$。
2. 对于来自 ${\mathfrak {L}}\,$ 的每个 $n\,$-元函数符号 $f\,$，有一个 $n\,$-元函数 $f^{\mathfrak {A}}:A^{n}\longrightarrow A\,$。
3. 对于来自 ${\mathfrak {L}}\,$ 的每个 $n\,$-元关系符号 $R\,$，有一个在 $A\,$ 上的 $n\,$-元关系，就是说一个子集 $R^{\mathfrak {A}}\subseteq A^{n}\,$。

在这个上下文中对这种结构使用模型这个词。但是理解它的动机或许是重要的，见下。

项、公式和句子

定义 ${\mathfrak {L}}\,$-项是来自 ${\mathfrak {L}}\,$ 的符号的非空有限字符串 $t\,$，如

• $t\,$ 是一个变量符号。
• $t\,$ 是一个常量符号。
• $t\,$ 是形如 $ft_{1}...t_{n}\,$ 的字符串，这里的 $f\,$ 是 $n\,$-元函数符号而 $t_{1}\,$, ..., $t_{n}\,$ 是 ${\mathfrak {L}}\,$ 的项。

定义 ${\mathfrak {L}}\,$-公式是来自 ${\mathfrak {L}}\,$ 的符号的非空有限字符串 $\phi \,$，如

• $\phi \,$ 是形如 $t_{1}=t_{2}\,$ 的字符串，这里的 $t_{1}\,$ 和 $t_{2}\,$ 是 ${\mathfrak {L}}\,$ 的项。
• $\phi \,$ 是形如 $Rt_{1}...t_{n}\,$ 的字符串，这里的 $R\,$ 是 $n\,$-元关系符号而 $t_{1}\,$, ..., $t_{n}\,$ 是 ${\mathfrak {L}}\,$ 的项。
• $\phi \,$ 形如 $\lnot (\alpha )\,$，这里的 $\alpha \,$ 是 ${\mathfrak {L}}\,$-公式。
• $\phi \,$ 形如 $(\alpha \lor \beta )\,$，这里的 $\alpha \,$ 和 $\beta \,$ 二者是 ${\mathfrak {L}}\,$-公式。
• $\phi \,$ 形如 $(\forall y)(\alpha )\,$，这里的 $y\,$ 是来自 ${\mathfrak {L}}\,$ 的变量符号而 $\alpha \,$ 是 ${\mathfrak {L}}\,$-公式。

定义 由要么第一个要么第二个子句来特征描述的 ${\mathfrak {L}}\,$-公式被称为原子。

定义 设 $\phi \,$ 是一个 ${\mathfrak {L}}\,$-公式。来自 ${\mathfrak {L}}\,$ 的变量符号 $x\,$ 被称为在 $\phi \,$ 中是自由的，如果

• $\phi \,$ 是原子，而 $x\,$ 出现在 $\phi \,$ 中。
• $\phi \,$ 形如 $\lnot (\alpha )\,$，而 $x\,$ 在 $\alpha \,$ 中是自由的。
• $\phi \,$ 形如 $(\alpha \lor \beta )\,$，而 $x\,$ 在 $\alpha \,$ 或 $\beta \,$ 中是自由的。
• $\phi \,$ 形如 $(\forall y)(\alpha )\,$，这里的 $x\,$ 和 $y\,$ 不是同一个变量符号而 $x\,$ 在 $\alpha \,$ 中是自由的。

定义 句子是没有自由变量的公式。

指派函数

此后，${\mathfrak {L}}\,$ 将指称一阶语言，${\mathfrak {A}}\,$ 是 ${\mathfrak {L}}\,$-结构，它下层的全集用 $A\,$ 指称。每个公式都将被理解为 ${\mathfrak {L}}\,$-公式。

定义 到 ${\mathfrak {A}}\,$ 的变量指派函数(v.a.f.)是自 ${\mathfrak {L}}\,$ 的变量集合到 $A\,$ 的函数。

定义 设 $s\,$ 是到 ${\mathfrak {A}}\,$ 的 v.a.f.。我们定义项指派函数(t.a.f.) ${\overline {s}}\,$，自 ${\mathfrak {L}}\,$-项的集合到 $A\,$，如:

• 如果 $t\,$ 是变量符号 $x\,$，则 ${\overline {s}}(t)=s(x)\,$。
• 如果 $t\,$ 是常量符号 $c\,$，则 ${\overline {s}}(t)=c^{\mathfrak {A}}\,$。
• 如果 $t\,$ 形如 $ft_{1}...t_{n}\,$，则 ${\overline {s}}(t)=f^{\mathfrak {A}}({\overline {s}}(t_{1}),...,{\overline {s}}(t_{n}))\,$。

定义 设 $s\,$ 是到 ${\mathfrak {A}}\,$ 的 v.a.f.，假定 $x\,$ 是一个变量而 $a\in A\,$。我们定义 v.a.f. $s[x|a]\,$，指称为 $x\,$-指派函数的修改 $s\,$，为

$s[x|a](v)={\begin{cases}s(v)&{\mbox{if }}v\neq x\\a&{\mbox{if }}v=x\end{cases}}\,$

逻辑满足

定义 设 $\phi \,$ 是公式，并假定 $s\,$ 是到 ${\mathfrak {A}}\,$ 的 v.a.f.。我们称 ${\mathfrak {A}}\,$ 通过指派 $s\,$ 满足 $\phi \,$ ，并写为 ${\mathfrak {A}}\models \phi [s]\,$，如果:

• $\phi \,$ 形如 $t_{1}=t_{2}\,$，而 ${\overline {s}}(t_{1})={\overline {s}}(t_{2})\,$。
• $\phi \,$ 形如 $Rt_{1}...t_{n}\,$，而 $({\overline {s}}(t_{1}),...,{\overline {s}}(t_{n}))\in R^{\mathfrak {A}}\,$。
• $\phi \,$ 形如 $\lnot (\alpha )\,$，而 ${\mathfrak {A}}{\mbox{ }}\not \models {\mbox{ }}\alpha [s]\,$。
• $\phi \,$ 形如 $(\alpha \lor \beta )\,$，而 ${\mathfrak {A}}\models \alpha [s]\,$ 或者 ${\mathfrak {A}}\models \beta [s]\,$。
• $\phi \,$ 形如 $(\forall y)(\alpha )\,$，而对于每个元素 $a\in A\,$，${\mathfrak {A}}\models \alpha [s[y|a]]\,$。

定义 设 $\phi \,$ 是公式，并对到 ${\mathfrak {A}}\,$ 的每个 v.a.f. $s\,$ 假定 ${\mathfrak {A}}\models \phi [s]\,$。则我们称 ${\mathfrak {A}}\,$ 建模 $\phi \,$，并写为 ${\mathfrak {A}}\models \phi \,$。

定义 设 $\Phi \,$ 是公式的集合，并对每个公式 $\phi \in \Phi \,$ 假定 ${\mathfrak {A}}\models \phi \,$，则我们称 ${\mathfrak {A}}\,$ 建模 $\Phi \,$，并写为 ${\mathfrak {A}}\models \Phi \,$。

在 $\phi \,$ 是句子的情况下，就是没有自由变量的公式，存在一个单一的 v.a.f.，对于它 ${\mathfrak {A}}\models \phi [s]\,$，直接的蕴涵了 ${\mathfrak {A}}\models \phi \,$。

定义 设 $\phi \,$ 是一个句子，并假定 ${\mathfrak {A}}\models \phi \,$。则我们称 $\phi \,$ 为在 ${\mathfrak {A}}\,$ 中是真实的。

逻辑蕴含和真实

定义 设 $\Psi \,$ 和 $\Phi \,$ 是公式的集合。我们称 $\Psi \,$ 为逻辑蕴涵 $\Phi \,$，并写为 $\Psi \models \Phi \,$，如果对于所有结构 ${\mathfrak {A}}\,$， ${\mathfrak {A}}\models \Psi \,$ 蕴涵 ${\mathfrak {A}}\models \Phi \,$。

作为简写，在处理单元素集合(singleton)的时候，我们经常写 $\Psi \models \phi \,$ 替代 $\Psi \models \{\phi \}\,$。

定义 设$\phi \,$ 是公式，并假定 $\varnothing \models \phi \,$。则我们称 $\phi \,$ 是全集有效，或者简单有效，在这种情况下我们简单的写为 $\models \phi \,$。

假如公式 $\phi \,$ 是有效的，实际上意味着所有 ${\mathfrak {L}}\,$-结构 ${\mathfrak {A}}\,$ 建模 $\phi \,$。

定义 设 $\phi \,$ 是一个句子，并假定 $\models \phi \,$。则我们称 $\phi \,$ 为真实的。

变量代换

定义 设 $u\,$ 是项，并假定 $x\,$ 是变量，而 $t\,$ 是另一个项。我们定义这个项 $u_{t}^{x}\,$，读做把 $x\,$ 替换为 $t\,$ 的 $u\,$，如下:

• 如果 $u\,$ 是变量符号 $x\,$，则 $u_{t}^{x}\,$ 被定义为是项 $t\,$。
• 如果 $u\,$ 是不是 $x\,$ 的变量符号，则 $u_{t}^{x}\,$ 被定义为项 $u\,$。
• 如果 $u\,$ 是常量符号，则 $u_{t}^{x}\,$ 被定义为项 $u\,$。
• 如果 $u\,$ 形如 $ft_{1}...t_{n}\,$，则 $u_{t}^{x}\,$ 被定义为项 $f{t_{1}}_{t}^{x}...{t_{n}}_{t}^{x}\,$。

定义 设 $\phi \,$ 是公式，并假定 $x\,$ 是变量，而 $t\,$ 是项。我们定义公式 $\phi _{t}^{x}\,$，读做把 $x\,$ 替换为 $t\,$ 的 $\phi \,$，如下:

• 如果 $\phi \,$ 形如 $t_{1}=t_{2}\,$，则 $\phi _{t}^{x}\,$ 被定义为公式 ${t_{1}}_{t}^{x}={t_{2}}_{t}^{x}\,$。
• 如果 $\phi \,$ 形如 $Rt_{1}...t_{n}\,$，则 $\phi _{t}^{x}\,$ 被定义为公式 $R{t_{1}}_{t}^{x},...,{t_{n}}_{t}^{x}\,$。
• 如果 $\phi \,$ 形如 $\lnot (\alpha )\,$，则 $\phi _{t}^{x}\,$ 被定义为公式 $\lnot (\alpha _{t}^{x})\,$。
• 如果 $\phi \,$ 形如 $(\alpha \lor \beta )\,$，则 $\phi _{t}^{x}\,$ 被定义为公式 $(\alpha _{t}^{x}\lor \beta _{t}^{x})\,$。
• 如果 $\phi \,$ 形如 $(\forall y)(\alpha )\,$，则
  • 如果 $x\,$ 和 $y\,$ 是同一个变量符号，则 $\phi _{t}^{x}\,$ 被定义为公式 $\phi \,$。
  • 否则 $\phi _{t}^{x}\,$ 被定义为公式 $(\forall y)(\alpha _{t}^{x})\,$。

可代换性

定义 设 $\phi \,$ 是公式，并假定 $x\,$ 是变量，而 $t\,$ 是项。我们称 $t\,$ 对 $x\,$ 在 $\phi \,$ 中是可代换的，如果:

• $\phi \,$ 是原子。
• $\phi \,$ 形如 $\lnot (\alpha )\,$，而 $t\,$ 对 $x\,$ 在 $\alpha \,$ 中是可代换的。
• $\phi \,$ 形如 $(\alpha \lor \beta )\,$，而 $t\,$ 对 $x\,$ 在 $\alpha \,$ 和 $\beta \,$ 二者中是可代换的。
• $\phi \,$ 形如 $(\forall y)(\alpha )\,$，而
  • 要么 $x\,$ 在 $\phi \,$ 中不是自由变量。
  • 要么 $y\,$ 在 $t\,$ 中不出现，而 $t\,$ 对 $x\,$ 在 $\alpha \,$ 中是可代换的。

项于变量的可代换性的概念相应于在代换在项或公式中完成之后保持真实性的概念。严格的说，代换总是允许的，但可代换性将是强制的，以此生成意义不被代换所破坏的公式。

引用

• A. S. Troelstra & H. Schwichtenberg (2000). Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science) (2nd ed.). Cambridge University Press. ISBN 0521779111.
• George Boolos & Richard Jeffrey (1989). Computability and Logic (3rd ed.). Cambridge University Press. ISBN 0521007585.
• Elliott Mendelson (1997). Introduction to Mathematical Logic (4th ed.) Chapman & Hall.
• A. G. Hamilton (1988). Logic for Mathematicians Cambridge University Press.

外部链接

• Mathematical Logic around the world
• Polyvalued logic
• Computability logic 数理逻辑的新方向 - 从真理的理论到可计算性的理论。

参见条目

• 逻辑
• 可计算性逻辑
• 博弈语义
• 可证明性逻辑
• 可解释性逻辑
• 相继式演算
• 直觉逻辑
• 谓词逻辑