2023“钉耙编程”中国大学生算法设计超级联赛（9）- 1003 Reasoning 题解

qzhwlzy / 2023-08-16 / 原文

题目翻译

基本符号

有一推理系统，其中有这些符号：

括号 \((\) 和 \()\)；
逻辑连接词 \(\lnot\) 和 \(\rightarrow\)；
全称量词 \(\forall\)；
变量 \(u\sim z\)；
常量 \(a\sim e\)；
函数 \(f\sim h\)；
谓词 \(P\sim T\)。

这些符号是构成系统的基础，他们之间能够组合出一些其他概念：

项（term）

变量和常量都叫做项；

假设 \(t_1,\ldots,t_n\) 都是项且 \(f\) 是函数，则 \(f\,t_1\ldots t_n\) 也是项。

也就是说，变量、常量和函数的组合就是项。

公式（formula）

假设 \(t_1,\ldots,t_n\) 都是项且 \(P\) 是谓词，则 \(P\, t_1\ldots t_n\) 是公式。这种公式被称为原子公式；

假设 \(\varphi\) 是公式，那么 \((\lnot \varphi)\) 也是公式；

假设 \(\varphi\) 和 \(\psi\) 都是公式，那么 \((\varphi\rightarrow \psi)\) 也是公式；

假设 \(\varphi\) 是公式，\(v\) 是变量，那么 \(\forall v \varphi\) 也是公式。

公式有四种定义，其中第二三种定义只是公式间的组合。下面的定义全部都基于这四种公式的定义。

自由出现（free occurrence）

对于公式 \(\varphi\) 和变量 \(x\)，\(x\) 在 \(\varphi\) 中自由出现的定义为：

假设 \(\varphi\) 是原子公式，当且仅当 \(x\) 在 \(\varphi\) 中出现（字符 \(x\) 在字符串 \(\varphi\) 中）就称 \(x\) 在 \(\varphi\) 中自由出现；

假设 \(\varphi\) 形如 \((\lnot\psi)\)，则 \(x\) 在 \(\varphi\) 中自由出现当且仅当 \(x\) 在 \(\psi\) 中自由出现；

假设 \(\varphi\) 形如 \((\psi\rightarrow \gamma)\)，则 \(x\) 在 \(\varphi\) 中自由出现当且仅当 \(x\) 在 \(\psi\) 或 \(\gamma\) 中自由出现；

假设 \(\varphi\) 形如 \(\forall v \psi\)，则 \(x\) 在 \(\varphi\) 中自由出现当且仅当 \(x\neq v\) 且 \(x\) 在 \(\psi\) 中自由出现。

可知，\(x\) 在 \(\forall v \varphi\) 中自由出现的必要条件是 \(x\neq v\)，即 \(x\) 在 \(\forall x \varphi\) 中不可能自由出现。我们可以把 \(\forall x\) 看作是 \(x\) 被“锁住”了。

替换（replacement）

对于公式 \(\varphi\)、变量 \(x\) 和项 \(t\)，替换 \(\varphi_t^x\) 定义为：

假设 \(\varphi\) 是原子公式，则 \(\varphi_t^x\) 表示将 \(\varphi\) 中的每一个 \(x\) 都替换成 \(t\)；

假设 \(\varphi\) 形如 \((\lnot \psi)\)，则 \(\varphi_t^x=(\lnot\psi)_t^x=(\lnot\psi_t^x)\)；

假设 \(\varphi\) 形如 \((\psi\rightarrow\gamma)\)，则 \(\varphi_t^x=(\psi\rightarrow\gamma)_t^x=(\psi_t^x\rightarrow\gamma_t^x)\)；

假设 \(\varphi\) 形如 \(\forall v\psi\)，则 \(\varphi_t^x = (\forall v\psi)_t^x = \begin{cases}\forall v\psi&x=v\\\forall v(\psi_t^x)&x\neq v\end{cases}\)。

也就是说，假设 \(x\) 在公式 \(\forall x\varphi\) 中被锁住了，那么该公式的替换就是其本身。

零冲突替换（zero-contradiction replacement）

对于公式 \(\varphi\)、变量 \(x\) 和项 \(t\)，零冲突替换定义为：

假设 \(\varphi\) 为原子公式，\(t\) 恒能在 \(\varphi\) 中零冲突替换 \(x\)；

假设 \(\varphi\) 形如 \((\lnot \psi)\)，则 \(t\) 能在 \(\varphi\) 中零冲突替换 \(x\) 当且仅当 \(t\) 能在 \(\psi\) 中零冲突替换 \(x\)；

假设 \(\varphi\) 形如 \((\psi\rightarrow \gamma)\)，则 \(t\) 能在 \(\varphi\) 中零冲突替换 \(x\) 当且仅当 \(t\) 能在 \(\psi\) 和 \(\gamma\) 中同时零冲突替换 \(x\)；

假设 \(\varphi\) 形如 \(\forall v\psi\)，则 \(t\) 能在 \(\varphi\) 中零冲突替换 \(x\) 当且仅当满足下面条件中的任意一个：

\(x\) 在 \(\varphi\) 中没有自由出现；

\(v\) 没有在 \(t\) 中出现，且 \(t\) 能在 \(\psi\) 中零冲突替换 \(x\)。