置换定理（谓词逻辑）

置换规则
术语名称	置换规则
英语名称	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] 。

谓词逻辑/一阶逻辑
命题结构	项	个体词（个体常项、个体变项）、论域/个体域、函项、项、闭项
	谓词	谓词（谓词常项、谓词变项）
	量词	量词（辖域、出现）、全称量词 [math]\displaystyle{ \forall }[/math] 、存在量词 [math]\displaystyle{ \exists }[/math]
谓词公式	形式定义	谓词语言 [math]\displaystyle{ \mathcal{L}^* }[/math] 、谓词公式、闭式
	逻辑语义	结构、指派/赋值、基本语义定义、解释、满足、模型
	语义分类	普遍有效公式、可满足式、不可满足式
	语义关系	逻辑等值/逻辑等价 [math]\displaystyle{ = }[/math]/[math]\displaystyle{ \Leftrightarrow }[/math] 、逻辑蕴涵 [math]\displaystyle{ \Rightarrow }[/math]
	范式	前束范式、 Skolem 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理