translation

现有一个推理系统，有如下符号组成：

• 圆括号：\((\) 和 \()\)
• 逻辑连词：\(\lnot\) 和 \(\to\)
• 全称量词：\(\forall\)
• 变量：\(u-z\)
• 常量：\(a-e\)
• 函数：\(f-h\)
• 谓词：\(P-T\)

这个推理系统还包括项（term）、公式（formula）、自由出现（free occurrence）和替换（replacement）等概念。基于这些概念，我们可以定义某个项 \(t\) 是否可以毫无冲突地替换某个变量 \(x\)。这是推理的基础之一，你想先解决这个问题。

项（term）的定义如下：

• 所有的变量 \(v\) 是一个项
• 所有的常量 \(c\) 是一个项
• 如果 \(t_1,t_2,\dots,t_n\) 是一些项，\(f\) 是一个函数，则 \(f_{t_1,t_2,\dots,t_n}\) 是一个项

公式（formula）的定义如下：

• 如果 \(t_1,t_2,\dots,t_n\) 是一些项，\(P\) 是一个谓词，则 \(P_{t_1,t_2,\dots,t_n}\) 是一个公式，而且这种公式被称为原子公式（atomic formula）
• 如果 \(\varphi\) 和 \(\psi\) 都是公式，则 \((\lnot\varphi)\) 和 \((\varphi\to\psi)\) 都是公式
• 如果 \(\varphi\) 是公式，\(v\) 是变量，则 \(\forall v\varphi\) 是公式

\(x\) 可以在 \(\varphi\) 中自由出现（free occurrence）的定义如下：

• 如果 \(\varphi\) 是原子公式，\(x\) 可以在 \(\varphi\) 中自由出现当且仅当在 \(\varphi\) 中有 \(x\)（可以理解为字符 \(x\) 在字符串 \(\varphi\) 中出现）
• 如果 \(\varphi\) 是 \((\lnot\psi)\)，\(x\) 可以在 \(\varphi\) 中自由出现当且仅当 \(x\) 可以在 \(\psi\) 中自由出现
• 如果 \(\varphi\) 是 \((\psi\to\gamma)\)，\(x\) 可以在 \(\varphi\) 中自由出现当且仅当 \(x\) 可以在 \(\psi\) 中自由出现或在 \(\gamma\) 中自由出现
• 如果 \(\varphi\) 是 \(\forall v\psi\)，\(x\) 可以在 \(\varphi\) 中自由出现当且仅当 \(x\) 可以在 \(\psi\) 中自由出现且 \(x\neq v\)

对于所有公式 \(\varphi\)，变量 \(x\)，项 \(t\)，替换（replacement）\(\varphi^x_t\) 的定义如下：

• 如果 \(\varphi\) 是原子公式，那么 \(\varphi^x_t\) 是通过简单地将每个字符 \(x\) 替换为字符串 \(t\) 形成的表达式
• 如果 \(\varphi\) 是 \((\lnot\psi)\)，那么 \((\lnot\psi)^x_t=(\lnot\psi^x_t)\)
• 如果 \(\varphi\) 是 \((\psi\to\gamma)\)，那么 \((\psi\to\gamma)^x_t=(\psi^x_t\to\gamma^x_t)\)
• 如果 \(\varphi\) 是 \(\forall y\psi\)，那么 \((\forall y\psi)^x_t=\left\{\begin{array}{ll}\forall y(\psi^x_t) & & \text{if}\ x\neq y\\\forall y\psi & & \text{if}\ x=y\end{array}\right.\)

最后，无冲突替换的定义如下：

• 如果 \(\varphi\) 是原子公式，那么 \(t\) 始终可以在 \(\varphi\) 中无冲突替换 \(x\)
• 如果 \(\varphi\) 是 \((\lnot\psi)\)，那么 \(t\) 在 \(\varphi\) 中可以无冲突替换 \(x\) 当且仅当 \(t\) 在 \(\psi\) 中可以无冲突替换 \(x\)