(資料圖)

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\)
• 如果 \(\varphi\) 是 \((\psi\to\gamma)\)，那么 \(t\) 在 \(\varphi\) 中可以無沖突替換 \(x\) 當且僅當 \(t\) 在 \(\psi\) 和 \(\gamma\) 中都可以無沖突替換 \(x\)
• 如果 \(\varphi\) 是 \(\forall y\psi\)，那么 \(t\) 在 \(\varphi\) 中可以無沖突替換 \(x\) 當且僅當：
  • \(x\) 不能在 \(\varphi\) 中自由出現，或
  • \(y\) 不能在 \(t\) 中自由出現，且 \(t\) 在 \(\psi\) 中可以無沖突替換 \(x\)

標簽：