一阶逻辑篇--一门数学编程语言

从数学编程语言的角度解读一阶逻辑

从整体上看，一阶逻辑=命题逻辑+谓词+量词+函数。

我们可以将一阶逻辑看作是一种特殊的数学编程语言，其目标是精确地表达关于“对象”及其“属性”和“关系”的陈述，并进行逻辑推理。

原子量

在一门编程语言中，我们首先需要定义基本的数据类型。 在一阶逻辑中，我们也有类似的“原子量”作为构建更复杂表达式的基础：

• 数 (Numbers): 正如示例 $\forall x\in \mathbb{R}.x^2\ge 0$ 中的 $x\in \mathbb{R}$，一阶逻辑可以处理各种数，例如实数 ($\mathbb{R}$)、整数 ($\mathbb{Z}$)、自然数 ($\mathbb{N}$) 等。 这些数可以作为我们程序操作的基本数据。 在编程语言中，这对应于 int, float, double 等数值类型。
• 常量 (Constants): 常量代表着程序中固定的、不可变的值。 虽然您的列表中没有显式列出，但在实际一阶逻辑的应用中，常量也扮演重要角色。 例如，我们可以用常量符号 0, 1, e, pi 等来指代特定的数学常数，或者用 Alice, Bob 等指代特定的人。 在编程中，常量类似于字面量，例如 10, 3.14, "hello" 或者用 const 定义的常量。
• 布尔值 (Boolean Values): 真 (True, $\top$ 或 $T$) 和 假 (False, $\perp$ 或 $F$) 是逻辑运算和谓词判断的基础。 一阶逻辑的语句最终会被判断为真或假，这类似于编程语言中布尔类型 bool 或 boolean，以及条件判断的结果。

操作

编程语言离不开各种运算符来操作数据。 在一阶逻辑中，我们有逻辑运算符来构建复杂的逻辑表达式：

• 非 (NOT, $\neg$, $\overline{}$): 对应编程语言中的逻辑非运算符 ! 或 not。 例如，$\neg P$ 就如同编程中的 !P，表示逻辑取反。 在第 3.6.5 节的量词否定定律中，我们看到了 NOT 操作的应用。
• 与 (AND, $\wedge$): 对应编程语言中的逻辑与运算符 && 或 and。 例如，$P\wedge Q$ 如同 P && Q，表示逻辑“与”运算，两者都为真时结果才为真。 在 Problem 3.46 的解答中，我们大量使用 AND 来连接多个条件。
• 或 (OR, $\vee$): 对应编程语言中的逻辑或运算符 || 或 or。 例如，$P\vee Q$ 如同 P || Q，表示逻辑“或”运算，两者至少有一个为真时结果为真。 在 Problem 3.46(a) 部分的答案中，我们使用了 OR 来表示 “在左边或在右边” 的关系。
• 蕴含 (IMPLIES, $⟹$, $\to$): 虽然在一些编程语言中没有直接的蕴含运算符，但其逻辑意义可以用条件语句 if (P) then Q 来模拟，或者在逻辑表达式中进行表达。 例如，$P⟹Q$ 可以理解为 “如果 P 成立，那么 Q 也应该成立”。 第 3.6.6 节讨论谓词公式的有效性时，就使用了蕴含符号来表达逻辑推导关系。
• 等价 (EQUIVALENT, $\leftrightarrow$, $\equiv$, $\iff$): 逻辑等价表示两个公式的真值相同。 虽然编程语言中没有直接的等价运算符，但可以用相等性判断 == 来比较逻辑表达式的结果是否一致。 例如，$P\leftrightarrow Q$ 可以理解为 “P 和 Q 的逻辑结果总是相同的”。 在第 3.6.5 节的量词德摩根定律和 3.6.6 节的有效性示例中，都使用了等价符号。
• 永真式 (Tautology): 永真式就像一个永远返回 true 的程序片段。 在逻辑中，我们用永真式来表示总是成立的逻辑规律，例如第 3.4 节中的排中律 $A\vee \overline{A}\leftrightarrow T$。
• 永假式 (Contradiction): 永假式则像一个永远返回 false 的程序片段。 逻辑中的矛盾式表示永远不可能成立的逻辑状态，例如第 3.4 节中的矛盾律 $A\wedge \overline{A}\leftrightarrow F$。

函数

在编程语言中，函数接受输入并返回输出，实现从一种类型数据到另一种类型数据的转换。 在一阶逻辑中，“函数：对象->对象” 对应于 函数符号 (Function Symbols)。

• 函数符号 在一阶逻辑中代表着定义在论域上的函数关系，它接受一个或多个论域中的对象作为输入 (参数)，并返回论域中的另一个对象作为输出。 例如，数学中的加法 +，乘法 *，平方根 sqrt 等都可以视为函数符号。 虽然在第 3.6 节的例子中函数符号使用不多，但在更广泛的一阶逻辑应用中，特别是在数理逻辑和形式化数学中，函数符号是不可或缺的。
• 类型签名 “对象->对象” 强调了函数是从论域中的对象映射到论域中的对象的，这与编程语言中函数的类型定义概念一致。 例如，一个函数可能被定义为 int add(int a, int b)，其类型签名就是 (int, int) -> int。

量词

量词是区分一阶逻辑和命题逻辑的关键特征，从编程角度看，可以将量词理解为强大的循环控制结构，用于处理论域中的多个对象：

• 存在量词 ($\exists x$): “存在 $x$ 使得…” 可以类比于编程中的 搜索算法或条件判断。 $\exists x.P(x)$ 就像在某个数据集合中搜索是否存在满足条件 $P(x)$ 的元素。 例如，在编程中，我们可能会遍历一个列表，检查是否有任何元素满足某个条件，一旦找到一个就返回 true。 第 3.6.1 节的 $\exists x\in \mathbb{R}.5x^2-7=0$ 就像在实数集中寻找方程的解。 Problem 3.46 中的 $\exists y.(F(x,y)\vee F(y,x))$ 则是在学生集合中寻找与学生 $x$ 有位置关系的其他学生。
• 全称量词 ($\forall x$): “对于所有 $x$ 都满足…” 可以类比于编程中的 循环遍历和普遍性验证。 $\forall x.P(x)$ 就像遍历某个数据集合中的 所有 元素，并检查 每个元素 是否都满足条件 $P(x)$。 例如，检查一个数组中的所有元素是否都是正数。 第 3.6.1 节的 $\forall x\in \mathbb{R}.x^2\ge 0$ 就像验证所有实数的平方是否都非负。 哥德巴赫猜想的公式 $\forall n\in Evens\exists p\in Primes\exists q\in Primes.n=p+q$ 则体现了更复杂的嵌套循环和条件检查结构。

谓词

“谓词：对象->布尔值” 精准地描述了谓词在一阶逻辑中的作用。

谓词 (Predicates) 可以看作是 返回布尔值的函数，它描述了论域中对象的 属性 或对象之间的 关系。 例如：

• $x^{2}\geq 0$ 可以视为一个谓词，判断实数 $x$ 是否具有 “平方非负” 的属性。
• $F(x,y)$ 是谓词，判断学生 $x$ 和 $y$ 是否满足 “$x$ 在 $y$ 左侧” 的关系。
• $n \in Evens$ 和 $p \in Primes$ 是谓词，判断数字是否属于偶数集合或素数集合。
• $Solves(x)$ 是谓词，判断 “你” 是否具有 “解决问题 $x$” 的能力。
• $H(a, d)$ 是谓词，判断 “美国人 $a$” 和 “梦想 $d$” 是否满足 “拥有” 的关系。

“对象->布尔值” 的类型签名 强调了谓词的本质： 它接受对象 (一个或多个) 作为输入，并输出一个布尔值 (真或假)，表明该属性或关系是否成立。 这与编程语言中常见的布尔函数（例如 isEmpty(list), isAdult(age), isEqualTo(value1, value2)）的概念完全一致。

语句形式

“语句形式”：

• $\exists x$. some-formula;
• $\forall x$. some-formula;

体现了一阶逻辑中量词作为语句前缀，构成基本语句结构的方式。 这类似于编程语言中，某些关键词（如 if, for, while）引导控制流语句的结构。

• 量词前缀： 量词 ($\exists x$ 或 $\forall x$) 就像语句的 “控制头”，它声明了要量化的变量 $x$ 及其作用域， 这类似于编程语言中循环语句的 for (int i = 0; i < n; i++) 或 foreach (item in list) 中的循环变量声明和范围限定。
• some-formula: 可以是一个简单的谓词，也可以是由逻辑运算符组合成的复杂谓词公式，这类似于编程语言中，循环体或条件语句体可以是简单的表达式，也可以是复杂的代码块。
• 分号 ; (可选): 分号虽然在一阶逻辑语法中不是必须的，但在 “数学编程语言” 的视角下，可以将其视为语句的结束符，增强代码（公式）的可读性，就像编程语言中使用分号分隔语句一样。

总结： 一阶逻辑

通过以上类比，我们可以将一阶逻辑理解为一种 “数学编程语言”，它的 “程序” 就是 谓词公式。 编写一阶逻辑公式，就像编写一段程序来：

1. 操作定义在 “论域” 上的 “对象” (数据)。
2. 使用 “谓词” 函数来描述对象的属性和关系。
3. 使用 “逻辑运算符” 组合谓词，构建复杂的逻辑条件。
4. 使用 “量词” 这种强大的循环控制结构，对论域中的对象进行量化断言 (存在性或普遍性)。

一阶逻辑程序的“运行结果”，就是判断该公式在给定解释下是 “真” (True) 还是 “假” (False)。 而一阶逻辑的 “推理系统”，则类似于程序的 “编译” 和 “调试” 工具，帮助我们分析和验证逻辑程序的正确性，并从已有的逻辑程序推导出新的逻辑程序 (定理)。