translation

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

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

项（term）的定义如下：

公式（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.\)

1003 Reasoning（大模拟）