|
|
| （未显示同一用户的5个中间版本） |
| 第1行： |
第1行： |
| [[分类:证明论]][[分类:模型论]] | | [[分类:谓词逻辑]]{{DEFAULTSORT:jie3shi4}} |
| | {{#seo: |
| | |keywords=解释, 谓词逻辑, 赋值, 语义解释 |
| | |description=本文介绍解释的定义、性质与应用，包括解释作为谓词逻辑中语义赋值概念，其在确定谓词公式真值中的核心作用，及其在谓词语义学中的重要性。 |
| | |modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}} |
| | |published_time=2023-07-15 |
| | }} |
| {{InfoBox | | {{InfoBox |
| |name=解释 | | |name=解释 |
| |eng_name=interpretation | | |eng_name=interpretation |
| }} | | }} |
| {{InfoBox
| | '''解释'''('''interpretation''')在[[:分类:谓词逻辑|谓词逻辑]]中指通过[[结构（谓词逻辑）|结构]]或[[赋值（谓词逻辑）|赋值]]为[[谓词公式]]提供语义内容的动作。 |
| |name=模型
| |
| |eng_name=model
| |
| |aliases=解释,interpretation
| |
| }}
| |
| '''解释'''('''interpretation''')是对谓词公式的非逻辑符号取值。 | |
| 即指定论域，并使其中所有[[个体词（谓词逻辑）|个体常项]]、[[函项]]、[[谓词]]替换为论域上的具体对象。
| |
| | |
| 与命题逻辑的解释不同，谓词公式中仅有[[闭式]]被解释后会变成命题。
| |
| | |
| 解释过程中使用的论域及替换用的映射关系，加在一起也叫'''解释'''、'''结构'''('''structure''')或'''模型'''('''model''')。
| |
| | |
| == 定义 ==
| |
| | |
| === 定义1 ===
| |
| | |
| 对谓词公式 <math>G</math> ，其'''解释'''('''explanation''') <math>\mathfrak{I}</math> ，包括：
| |
| | |
| * <math>D</math> 是非空集合，即'''论域'''('''domain of discourse''')或'''个体域'''('''individual domain''')；
| |
| * 将 <math>G</math> 中的每一个个体常项 <math>c</math> 映射到论域 <math>D</math> 中的元素；
| |
| * 将 <math>G</math> 中的每一个 <math>n</math> 元函项 <math>f</math> 映射到论域 <math>D</math> 上的 <math>n</math> 元映射；
| |
| * 将 <math>P</math> -语言中的每一个 <math>n</math> 元谓词 <math>P</math> 映射到论域 <math>D</math> 上的 <math>n</math> 元关系。
| |
| | |
| === 定义2（塔尔斯基语义学） ===
| |
| | |
| 将谓词公式建模为 [[谓词语言|<math>\mathcal{L}_1</math> 语言]]，其中有序对 <math>\mathfrak{I} = \left\langle D, I \right\rangle</math> 被称为一个 '''<math>\mathcal{L}_1</math> -模型'''，也称为 '''<math>\mathcal{L}_1</math> -解释''' ，其中：
| |
| | |
| <math>D</math> 是非空集合，即'''论域'''('''domain of discourse''')或'''个体域'''('''individual domain''')；
| |
| | |
| <math>I</math> 是一个映射，且
| |
| * 将 <math>\mathcal{L}_1</math> -语言中的每一个个体常项 <math>c</math> 映射到论域 <math>D</math> 中的元素 <math>I(c)</math>；
| |
| * 将 <math>\mathcal{L}_1</math> -语言中的每一个 <math>n</math> 元函项 <math>f</math> 映射到论域 <math>D</math> 上的 <math>n</math> 元映射 <math>I(f)</math>；
| |
| * 将 <math>\mathcal{L}_1</math> -语言中的每一个 <math>n</math> 元谓词 <math>P</math> 映射到论域 <math>D</math> 上的 <math>n</math> 元关系 <math>I(P)</math>。
| |
| | |
| 通常简称为'''模型'''('''model''')或'''解释'''('''interpretation''')。
| |
| | |
| == 记号 ==
| |
|
| |
|
| 解释 <math>\mathfrak{I}</math> 下的 <math>c, f, P</math> 的像通常记作 <math>c^\mathfrak{I}, f^\mathfrak{I}, P^\mathfrak{I}</math> 。
| | 结构指定了论域以及公式中每个个体常项、函项、谓词的语义后，[[闭式]]成为了[[命题]]，通过 [[Tarski 真理定义]]获得了一个真值（语义）；而赋值除了结构外还指定了公式中的每个自由的个体变项的取值，此时任意谓词公式都成为了命题。 |
|
| |
|
| == 注意 ==
| | “解释”一词也被用于指代结构本身，即使用的论域及替换用的[[映射]]关系，这一含义见[[结构（谓词逻辑）]]。 |
|
| |
|
| 模型也可以看作某个论域及其上的多元函数及谓词，也就是说[[结构（代数系统）|代数系统的结构]]，因此也被称为一个'''结构'''('''structure''')。
| | 说明：谓词公式及闭式是纯语法形式的概念，符合这样语法的符号串是一个谓词公式或闭式，没有直接绑定语义。 |
| | 结构是从其中每个个体常项、函项、谓词到论域中的个体对象及其关系的映射，赋值是一个结构加上其中个体变项到个体对象的映射。 |
| | 解释是给谓词公式赋予结构或赋值的过程，也就是赋予如下语义的过程：当每个非逻辑符号按照结构中的取值代表论域中的对象及其关系时，这个公式所构成的命题是论域中的一个什么具体命题。 |
|
| |
|
|
| |
|
| {{谓词逻辑}} | | {{谓词逻辑}} |
| {{模型论}}
| |
| 解释
|
| 术语名称
|
解释
|
| 英语名称
|
interpretation
|
解释(interpretation)在谓词逻辑中指通过结构或赋值为谓词公式提供语义内容的动作。
结构指定了论域以及公式中每个个体常项、函项、谓词的语义后，闭式成为了命题，通过 Tarski 真理定义获得了一个真值（语义）；而赋值除了结构外还指定了公式中的每个自由的个体变项的取值，此时任意谓词公式都成为了命题。
“解释”一词也被用于指代结构本身，即使用的论域及替换用的映射关系，这一含义见结构（谓词逻辑）。
说明：谓词公式及闭式是纯语法形式的概念，符合这样语法的符号串是一个谓词公式或闭式，没有直接绑定语义。
结构是从其中每个个体常项、函项、谓词到论域中的个体对象及其关系的映射，赋值是一个结构加上其中个体变项到个体对象的映射。
解释是给谓词公式赋予结构或赋值的过程，也就是赋予如下语义的过程：当每个非逻辑符号按照结构中的取值代表论域中的对象及其关系时，这个公式所构成的命题是论域中的一个什么具体命题。
