跳转到内容

Advertising:

满足(谓词逻辑):修订间差异

来自GSXAB的知识库
Gsxab留言 | 贡献
无编辑摘要
 
Gsxab留言 | 贡献
无编辑摘要
 
(未显示同一用户的1个中间版本)
第1行: 第1行:
[[分类:谓词逻辑]][[分类:模型论]]
[[分类:谓词逻辑]]
[[分类:模型论]]{{DEFAULTSORT:man3zu2}}
{{#seo:
|keywords=满足, 命题逻辑, 逻辑语义学, 可满足性
|description=本文介绍满足关系的定义、性质与应用,包括满足作为结构、赋值与公式间的关系概念,及其在模型定义中的重要性。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-01
}}
{{InfoBox
{{InfoBox
|name=满足
|name=满足
|eng_name=satisfy
|eng_name=satisfy
}}
}}
一个[[赋值(谓词逻辑)|赋值]]'''满足'''('''satisfies''')一个[[谓词公式]],指赋值使得这个公式变成真命题。
一个[[赋值(谓词逻辑)|赋值]]'''满足'''('''satisfies''')一个[[谓词公式]],指这个赋值使得这个公式被[[解释(谓词逻辑)|解释]]为真命题。换句话说,按照这个赋值把这个谓词公式中的[[个体词(谓词逻辑)|个体常项、个体变项]]、[[函项]]、[[谓词]]映射到论域中的个体对象及关系使其成为命题后,得到的命题是真命题。


满足公式集中的每个公式时,也说满足这个公式集。
赋值满足公式集中的每个公式时,也说赋值满足这个公式集。
一个[[模型]]上的任意赋值均满足公式或公式集时,也说一个模型满足这个公式或公式集。
一个[[结构(谓词逻辑)|结构]]上的任意赋值均满足公式或公式集,也就是对个体变项的任意映射,只固定个体常项、函项、谓词的像时,仍然保持得到真命题,称这个结构满足这个公式或公式集,此时称这个公式或公式集为一个理论,这个结构为这个理论的一个[[模型]]


== 定义 ==
== 定义 ==


对谓词公式 <math>\phi</math> 及模型 <math>\mathfrak{I}</math> 上的赋值 <math>\sigma</math> ,若公式在赋值后的命题 <math>\phi^\sigma</math> 为真命题,则称赋值 <math>\sigma</math> '''满足'''('''satisfies''')公式 <math>\phi</math>,记作 <math>\sigma \vDash \phi</math>。
对谓词公式 <math>\phi</math> 及模型 <math>\mathfrak{I}</math> 上的赋值 <math>\sigma</math> ,若公式在赋值后的命题 <math>\phi^\sigma</math> 为真命题,则称赋值 <math>\sigma</math> '''满足'''('''satisfies''')公式 <math>\phi</math> ,记作 <math>\sigma \vDash \phi</math> 。


* 若对公式集 <math>\Gamma</math> 及模型 <math>\mathfrak{I}</math> 上的赋值 <math>\sigma</math> ,对 <math>\Gamma</math> 中任意公式 <math>\phi</math> 都有 <math>\sigma \vDash \phi</math> ,则说赋值 <math>\sigma</math> '''满足'''公式集 <math>\Gamma</math>,记为 <math>\sigma \vDash \Gamma</math>。
* 若对公式集 <math>\Gamma</math> 及模型 <math>\mathfrak{I}</math> 上的赋值 <math>\sigma</math> ,对 <math>\Gamma</math> 中任意公式 <math>\phi</math> 都有 <math>\sigma \vDash \phi</math> ,则说赋值 <math>\sigma</math> '''满足'''公式集 <math>\Gamma</math> ,记为 <math>\sigma \vDash \Gamma</math> 。
* 若对公式 <math>\phi</math> 及模型 <math>\mathfrak{I}</math> ,对 <math>\mathfrak{I}</math> 上任意赋值 <math>\sigma</math> 都有 <math>\sigma \vDash \phi</math> ,则说模型 <math>\mathfrak{I}</math> '''满足'''公式 <math>\phi</math>,记为 <math>\mathfrak{I} \vDash \phi</math>。
* 若对公式 <math>\phi</math> 及模型 <math>\mathfrak{I}</math> ,对 <math>\mathfrak{I}</math> 上任意赋值 <math>\sigma</math> 都有 <math>\sigma \vDash \phi</math> ,则说模型 <math>\mathfrak{I}</math> '''满足'''公式 <math>\phi</math> ,记为 <math>\mathfrak{I} \vDash \phi</math> 。
* 类似地定义 <math>\mathfrak{I} \vDash \Gamma</math> 。
* 类似地定义 <math>\mathfrak{I} \vDash \Gamma</math> 。
{{CharMetaInfo
|char=&#x22A8;
|unicodeCodePoint={{UnicodeCodePoint|U+22A8|True, Is a Tautology, Satisfies, Results in}}
|latex=\vDash
}}




{{命题逻辑}}
{{谓词逻辑}}
{{模型论}}
{{模型论}}

2025年12月25日 (四) 10:08的最新版本

满足
术语名称 满足
英语名称 satisfy

一个赋值满足(satisfies)一个谓词公式,指这个赋值使得这个公式被解释为真命题。换句话说,按照这个赋值把这个谓词公式中的个体常项、个体变项函项谓词映射到论域中的个体对象及关系使其成为命题后,得到的命题是真命题。

赋值满足公式集中的每个公式时,也说赋值满足这个公式集。 一个结构上的任意赋值均满足公式或公式集,也就是对个体变项的任意映射,只固定个体常项、函项、谓词的像时,仍然保持得到真命题,称这个结构满足这个公式或公式集,此时称这个公式或公式集为一个理论,这个结构为这个理论的一个模型

定义

对谓词公式 [math]\displaystyle{ \phi }[/math] 及模型 [math]\displaystyle{ \mathfrak{I} }[/math] 上的赋值 [math]\displaystyle{ \sigma }[/math] ,若公式在赋值后的命题 [math]\displaystyle{ \phi^\sigma }[/math] 为真命题,则称赋值 [math]\displaystyle{ \sigma }[/math] 满足(satisfies)公式 [math]\displaystyle{ \phi }[/math] ,记作 [math]\displaystyle{ \sigma \vDash \phi }[/math]

  • 若对公式集 [math]\displaystyle{ \Gamma }[/math] 及模型 [math]\displaystyle{ \mathfrak{I} }[/math] 上的赋值 [math]\displaystyle{ \sigma }[/math] ,对 [math]\displaystyle{ \Gamma }[/math] 中任意公式 [math]\displaystyle{ \phi }[/math] 都有 [math]\displaystyle{ \sigma \vDash \phi }[/math] ,则说赋值 [math]\displaystyle{ \sigma }[/math] 满足公式集 [math]\displaystyle{ \Gamma }[/math] ,记为 [math]\displaystyle{ \sigma \vDash \Gamma }[/math]
  • 若对公式 [math]\displaystyle{ \phi }[/math] 及模型 [math]\displaystyle{ \mathfrak{I} }[/math] ,对 [math]\displaystyle{ \mathfrak{I} }[/math] 上任意赋值 [math]\displaystyle{ \sigma }[/math] 都有 [math]\displaystyle{ \sigma \vDash \phi }[/math] ,则说模型 [math]\displaystyle{ \mathfrak{I} }[/math] 满足公式 [math]\displaystyle{ \phi }[/math] ,记为 [math]\displaystyle{ \mathfrak{I} \vDash \phi }[/math]
  • 类似地定义 [math]\displaystyle{ \mathfrak{I} \vDash \Gamma }[/math]
字符
Unicode码位 U+22A8 True, Is a Tautology, Satisfies, Results in
Latex命令序列 \vDash


谓词逻辑/一阶逻辑
命题结构 个体词(个体常项、个体变项)、论域/个体域函项项、闭项
谓词 谓词(谓词常项、谓词变项)
量词 量词(辖域、出现)全称量词 [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: