跳转到内容

Advertising:

易字变形:修订间差异

来自GSXAB的知识库
Gsxab留言 | 贡献
无编辑摘要
Gsxab留言 | 贡献
无编辑摘要
 
(未显示同一用户的1个中间版本)
第1行: 第1行:
[[分类:谓词逻辑]]
[[分类:谓词逻辑]]{{DEFAULTSORT:yi4zi4bian4xing2}}
{{#seo:
|keywords=易字变形
|description=本文介绍易字变形及易字式的定义、性质与转换方法,包括这种操作的特点及意义。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-09
}}
{{InfoBox
{{InfoBox
|name=易字变形
|name=易字变形
|eng_name=
|eng_name=
}}
}}
'''易字变形'''指一个[[谓词公式]],其中的部分[[量词|量化公式]]被替换成其[[易字式]]。
'''易字变形'''指对一个[[谓词公式]],其中的部分作为子公式的[[量词|量化公式]]被替换成其[[易字式]]。
两个公式互为易字变形意味着两公式间可通过多次易字互相转换,过程中保持语义性质不变。这是一种[[等价关系]]。


== 定义 ==
== 定义 ==
第14行: 第21行:
=== 易字变形 ===
=== 易字变形 ===


递归地定义公式间的 '''易字变形''':
定义两谓词公式间的'''易字变形'''关系为简单易字变形关系的[[等价闭包]]
# <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> 的易字变形。
== 性质 ==
互为易字变形的公式[[逻辑等值]]。




{{谓词逻辑}}
{{谓词逻辑}}

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] 互为简单易字变形

易字变形

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

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

Advertising: