一階謂詞演算自然推演系統\(N_{\mathcal{L}}\) 中常見公式總結
\[以下是對“自由出現”和“自由"的個人理解：\\ 1. x在\alpha在\beta中若有自由出現，可以認為\alpha和\beta公式的真假與x有關，即原公式成立或否對x有依賴\\ 2.t對x在\alpha在\beta中自由，我們希望變換的時候性質保持不變，如果有約束性即t對x在原公式中不自由，\\ 則相當於縮小了公式成真的范圍\\ \]
關於量詞移位
- \(\forall\) \(\exists\) 和\(\longrightarrow\) 的量詞移位：
\(\forall x(\alpha \longrightarrow \beta)\)：
\[當x不在\alpha自由出現時：\\ \forall x(\alpha \longrightarrow \beta)\ |-|\ \alpha \longrightarrow \forall x\beta \\ \\ 當x不在\beta自由出現時：\\ \forall x(\alpha \longrightarrow \beta)\ |-|\ \exists x \alpha \longrightarrow \beta\\ \\ x在\alpha對\beta是否自由出現未知：\\ \forall x(\alpha \longrightarrow \beta)\ |-|\ \forall x \alpha \longrightarrow \forall x \beta\\ \forall x(\alpha \longrightarrow \beta)\ |-|\ \exists x \alpha \longrightarrow \exists x \beta \]
\(\exists x(\alpha \longrightarrow \beta)\)：
\[x在\alpha中沒有自由出現： \exists x(\alpha \longrightarrow \beta)\ |- \ \alpha \longrightarrow \exists\beta\\ \\ \alpha \longrightarrow \exists \beta \ |- \ \exists x(\alpha \longrightarrow \beta) 恆成立\\ \\ x在\beta中沒有自由出現： \exists x(\alpha \longrightarrow \beta) \ |- \forall x\alpha \longrightarrow \beta\\ \\ \forall x\alpha\longrightarrow\beta \ |- \ \exists x(\alpha \longrightarrow \beta)恆成立 \]
-
$\forall $ \(\exists\) 和 \(\longleftrightarrow\)的量詞移位：
\[\forall x(\alpha \longleftrightarrow \beta)\ |—\ \forall x\alpha \longleftrightarrow \forall x\beta 恆成立\\ \forall x(\alpha \longleftrightarrow \beta)\ |—\ \exists x\alpha \longleftrightarrow \exists x\beta 恆成立 \] -
$\forall $ \(\exists\) 和 \(\and\) \(\or\) 的量詞移位：
\[對於\forall而言：\\ x不在\alpha中自由出現：\alpha \and \forall x\beta\ |- \forall x(\alpha\and\beta)\\ \forall x(\alpha \and \beta)\ |-\ \alpha \and\forall x\beta 恆成立\\ \\ x不在\beta中自由出現:\alpha \or\forall x \beta\ |-| \forall x(\alpha \or\beta)\\ \\ 對於\exists而言：\\ x不在\alpha中自由出現: \alpha \and \exists x\beta |-| \exists x(\alpha \and \beta)\\ x不在\alpha中自由出現:\exists x(\alpha \or \beta) |- \alpha \or \exists x\beta\\ \alpha \or \exists x\beta |- \exists x(\alpha \or \beta)恆成立 \]
211207第一版更新