一阶谓词演算自然推演系统\(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第一版更新