查看“︁解释（谓词逻辑）”︁的源代码

[[分类:证明论]][[分类:模型论]]
{{InfoBox
|name=解释
|eng_name=interpretation
}}
{{InfoBox
|name=模型
|eng_name=model
|aliases=解释,interpretation
}}
'''解释'''('''interpretation''')是对谓词公式的[[非逻辑符号]]取值。
即对一个抽象的谓词公式，为其指定论域，并使其中所有[[个体词（谓词逻辑）|个体常项]]、[[函项]]、[[谓词]]指向论域上的具体个体对象及其关系、性质。

与命题逻辑的解释不同，谓词公式中仅有[[闭式]]被解释后会变成命题。

解释过程中使用的论域及替换用的[[映射]]关系，加在一起也叫'''解释'''、'''结构'''('''structure''')或'''模型'''('''model''')。

== 定义 ==

=== 定义1 ===

对谓词公式 <math>G</math> ，其'''解释'''('''interpretation''') <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>G</math> 中的每一个 <math>n</math> 元谓词 <math>P</math> 映射到论域 <math>D</math> 上的 <math>n</math> 元[[关系]]。

=== 定义2（塔尔斯基语义学） ===

将谓词公式建模为 [[谓词语言|<math>\mathcal{L}_1</math> 语言]]，其中有序对 <math>\mathfrak{I} = (D, I)</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> 。

== 注意 ==

模型也可以看作某个论域及其上的多元函数及谓词，也就是说[[结构（代数系统）|代数系统的结构]]，因此也被称为一个'''结构'''('''structure''')。


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