置换定理（谓词逻辑）：修订间差异

2026年1月9日 (五) 14:47的版本

置换规则
术语名称	置换规则
英语名称	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{ \forall }[/math] 、存在量词 [math]\displaystyle{ \exists }[/math]
谓词公式	形式定义	谓词语言 [math]\displaystyle{ \mathcal{L}^* }[/math] 、谓词公式、闭式
	逻辑语义	结构、指派/赋值、基本语义定义、解释、满足、模型
	语义分类	普遍有效公式、可满足式、不可满足式
	语义关系	逻辑等值/逻辑等价 [math]\displaystyle{ = }[/math]/[math]\displaystyle{ \Leftrightarrow }[/math] 、逻辑蕴涵 [math]\displaystyle{ \Rightarrow }[/math]
	范式	前束范式、 Skolem 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理

@@ 第15行： / 第15行： @@
 == 定理 ==
-对谓词公式 <math>\phi,\psi,\chi</math> ，原子公式 <math>p</math> ，且 <math>\phi,\psi</math> 中自由变项只有 <math>x_0, \cdots, x_k</math> ，设项 <math>t_0,\cdots,t_k</math> 分别对这些自由变项在两个公式中可自由代入，则有： <math>\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>\phi,\psi,\chi</math> ，原子公式 <math>p</math> ，且 <math>\phi,\psi</math> 中自由变项只有 <math>x_0, \cdots, x_k</math> ，设项 <math>t_0,\cdots,t_k</math> 分别对这些自由变项在两个公式中可自由代入，则有： <math>\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> 。
 {{谓词逻辑}}