查看“︁置换定理（谓词逻辑）”︁的源代码

[[分类:谓词逻辑]]{{DEFAULTSORT:zhi4huan4ding4li3}}
{{#seo:
|keywords=置换, 置换定理
|description=本文介绍谓词逻辑中的置换，以及与置换相关的置换定理及其性质。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2026-01-09
}}
{{InfoBox
|name=置换规则
|eng_name=substitution rule
|aliases=置换定理
}}
[[置换（逻辑）|置换]]指[[原子公式]]替换为其他公式的操作，谓词逻辑中的相关定理称为置换定理。其有几个不同形式的推论。

== 定理 ==

对谓词公式 <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>\Gamma\vDash\forall x_0 \cdots \forall x_k (\phi\leftrightarrow\psi)</math> 则 <math>\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>\Gamma\vDash\forall x_0 \cdots \forall x_k (\phi\leftrightarrow\psi)</math> 且 <math>\Delta\vDash\chi[\phi[t_0/x_0,\cdots,t_k/x_k]/p]</math> 则 <math>\Gamma,\Delta\vDash\chi[\psi[t_0/x_0,\cdots,t_k/x_k]/p]</math> 。
* <math>\vDash\forall x_0 \cdots \forall x_k (\phi\leftrightarrow\psi)</math> 则 <math>\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>\vDash \phi\leftrightarrow\psi</math> 则 <math>\vDash\chi[\phi/p]\leftrightarrow\chi[\psi/p]</math> 。


{{谓词逻辑}}