易字变形：修订间差异

2026年1月9日 (五) 12:09的最新版本

易字变形
术语名称	易字变形
英语名称

易字变形指对一个谓词公式，其中的部分作为子公式的量化公式被替换成其易字式。两个公式互为易字变形意味着两公式间可通过多次易字互相转换，过程中保持语义性质不变。这是一种等价关系。

定义

简单易字变形

对谓词公式 [math]\displaystyle{ \phi }[/math] 和 [math]\displaystyle{ \phi' }[/math] ，若存在公式 [math]\displaystyle{ \psi }[/math] 、原子公式 [math]\displaystyle{ p }[/math] 、互为易字式的两个量化公式 [math]\displaystyle{ \psi,\psi' }[/math] ，使得 [math]\displaystyle{ \phi=\chi[\psi/p],\phi'=\chi'[\psi'/p] }[/math] ，则称 [math]\displaystyle{ \phi,\phi' }[/math] 互为简单易字变形。

易字变形

定义两谓词公式间的易字变形关系为简单易字变形关系的等价闭包：

[math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ \phi }[/math] 本身的易字变形。
[math]\displaystyle{ \phi' }[/math] 是 [math]\displaystyle{ \phi }[/math] 的易字变形， [math]\displaystyle{ \phi'' }[/math] 是 [math]\displaystyle{ \phi' }[/math] 的简单易字变形，则 [math]\displaystyle{ \phi'' }[/math] 是 [math]\displaystyle{ \phi }[/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 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理

@@ 第1行： / 第1行： @@
-[[分类:谓词逻辑]]
+[[分类:谓词逻辑]]{{DEFAULTSORT:yi4zi4bian4xing2}}
+{{#seo:
+|keywords=易字变形
+|description=本文介绍易字变形及易字式的定义、性质与转换方法，包括这种操作的特点及意义。
+|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
+|published_time=2023-07-09
+}}
 {{InfoBox
 |name=易字变形
 |eng_name=
 }}
-'''易字变形'''指一个[[谓词公式]]，其中的部分[[量词|量化公式]]被替换成其[[易字式]]。
+'''易字变形'''指对一个[[谓词公式]]，其中的部分作为子公式的[[量词|量化公式]]被替换成其[[易字式]]。
+两个公式互为易字变形意味着两公式间可通过多次易字互相转换，过程中保持语义性质不变。这是一种[[等价关系]]。
 == 定义 ==
@@ 第10行： / 第17行： @@
 === 简单易字变形 ===
-对谓词公式 <math>\phi</math> 和 <math>\phi'</math> ，若存在公式 <math>\psi</math> 、原子公式 <math>p</math> 、互为易字式的两个量化公式 <math>\psi,\psi'</math> ，使得 <math>\phi=\chi(\psi/p),\phi'=\chi'(\psi'/p)</math> ，则称 <math>\phi,\phi'</math> 互为'''简单易字变形'''。
+对谓词公式 <math>\phi</math> 和 <math>\phi'</math> ，若存在公式 <math>\psi</math> 、原子公式 <math>p</math> 、互为易字式的两个量化公式 <math>\psi,\psi'</math> ，使得 <math>\phi=\chi[\psi/p],\phi'=\chi'[\psi'/p]</math> ，则称 <math>\phi,\phi'</math> 互为'''简单易字变形'''。
+=== 易字变形 ===
+定义两谓词公式间的'''易字变形'''关系为简单易字变形关系的[[等价闭包]]：
+# <math>\phi</math> 是 <math>\phi</math> 本身的易字变形。
+# <math>\phi'</math> 是 <math>\phi</math> 的易字变形， <math>\phi''</math> 是 <math>\phi'</math> 的简单易字变形，则 <math>\phi''</math> 是 <math>\phi</math> 的易字变形。
-=== 易字变形 --=
+== 性质 ==
-递归地定义公式间的 '''易字变形'''：
+互为易字变形的公式[[逻辑等值]]。
-# <math>\phi</math> 是 <math>\phi<math> 本身的易字变形。
-# <math>\phi'</math> 是 <math>\phi</math> 的易字变形， <math>\phi''</math> <math>\phi'</math> 的简单易字变形，则 <math>\phi''</math> 是 <math>\phi</math> 的易字变形。
 {{谓词逻辑}}