置换定理（谓词逻辑）
| 置换规则 | |
|---|---|
| 术语名称 | 置换规则 |
| 英语名称 | substitution rule |
| 别名 | 置换定理 |
置换指原子公式替换为其他公式的操作，谓词逻辑中的相关定理称为置换定理。其有几个不同形式的推论。
定理
对谓词公式 [math]\displaystyle{ \phi,\psi,\chi }[/math] ，原子公式 [math]\displaystyle{ p }[/math] ，且 [math]\displaystyle{ \phi,\psi }[/math] 中自由变项只有 [math]\displaystyle{ x_0, \cdots, x_k }[/math] ，设项 [math]\displaystyle{ t_0,\cdots,t_k }[/math] 分别对这些自由变项在两个公式中可自由代入，则有： [math]\displaystyle{ \forall x_0\cdots \forall x_n (\phi\leftrightarrow\psi) \vDash \chi[\phi[t_0/x_0,\cdots,t_k/x_k]/p]\leftrightarrow \chi[\psi[t_0/x_0,\cdots,t_k/x_k]/p] }[/math] 。
推论
- [math]\displaystyle{ \Gamma\vDash\forall x_0 \cdots \forall x_k (\phi\leftrightarrow\psi) }[/math] 则 [math]\displaystyle{ \Gamma\vDash\chi[\phi[t_0/x_0,\cdots,t_k/x_k]/p]\leftrightarrow\chi[\psi[t_0/x_0,\cdots,t_k/x_k]/p] }[/math] 。
- [math]\displaystyle{ \Gamma\vDash\forall x_0 \cdots \forall x_k (\phi\leftrightarrow\psi) }[/math] 且 [math]\displaystyle{ \Delta\vDash\chi[\phi[t_0/x_0,\cdots,t_k/x_k]/p] }[/math] 则 [math]\displaystyle{ \Gamma,\Delta\vDash\chi[\psi[t_0/x_0,\cdots,t_k/x_k]/p] }[/math] 。
- [math]\displaystyle{ \vDash\forall x_0 \cdots \forall x_k (\phi\leftrightarrow\psi) }[/math] 则 [math]\displaystyle{ \vDash\chi[\phi[t_0/x_0,\cdots,t_k/x_k]/p]\leftrightarrow\chi[\psi[t_0/x_0,\cdots,t_k/x_k]/p] }[/math] 。
- [math]\displaystyle{ \vDash \phi\leftrightarrow\psi }[/math] 则 [math]\displaystyle{ \vDash\chi[\phi/p]\leftrightarrow\chi[\psi/p] }[/math] 。