查看“︁泛函谓词”︁的源代码

{{Unreferenced |time=2008-06-20T09:00:01+00:00 }}
在[[形式逻辑]]和相关的[[数学]]分支中，'''泛函谓词'''或'''函数符号'''是应用于一个对象项而生成另一个对象项的[[逻辑符号]]。泛函谓词有时也叫做'''映射'''，但是这个术语还有其他意义。在[[模型论|模型]]中，函数符号被建模为[[函数]]。

特别是，在[[形式语言]]中的符号 ''F'' 是函数符号，如果给定任何表示在语言中的一个对象的符号 ''x''，''F''(''x'') 也是表示这个语言中一个对象的符号。在[[类型论|有类型逻辑]]中，''F'' 是带有域类型 '''T''' 和陪域类型 '''U''' 的函数符号，如果给定表示类型 '''T''' 的一个对象的任何符号 ''x''，''F''(''x'') 也是表示类型 '''U''' 的对象的符号。你可以类似的定义多于一个变量的函数符号，类比于多于一个变量的函数；[[零]] 个变量的函数符号简单的是一个[[常量]]符号。

现在考虑这个形式语言的模型，它带有类型 '''T''' 和 '''U''' 被建模为[[集合 (数学)|集合]] ['''T'''] 和 ['''U''']，而类型 '''T''' 的每个符号 ''X'' 被建模为 ['''T'''] 中的元素 [''x'']。则 ''F'' 可以被建模为集合
:<math>[F]:=\big\{([x],[F(x)]):[x]\in[\mathbf{T}]\big\},</math>
它简单的是带有域 ['''T'''] 和陪域 ['''U'''] 的一个[[函数]]。[''F''(''x'')] = [''F''(''y'')] 只要 [''x''] = [''y''] 是一致性模型的要求。

== 介入新的函数符号 ==

在允许介入新的谓词符号的谓词逻辑系统中，你可能也想介入新的函数符号。从旧的函数符号介入新的函数符号是容易的；给定函数符号 ''F'' 和 ''G''，有一个新函数符号 ''F'' <small>o</small> ''G''，它是 ''F'' 和 ''G'' 的'''复合'''，[[全称量化|对于所有]] ''x''，满足 (''F'' <small>o</small> ''G'')(''x'') = ''F''(''G''(''x''))。当然，等式的右边在有类型的逻辑中没有意义，除非 ''F'' 的域类型匹配 ''G'' 的陪域类型，这是定义复合的要求。

你还自动的获得特定的函数符号。在无类型逻辑中，有一个'''恒等谓词''' id，对于所有 ''X'' 满足 id(''x'') = ''x''。在有类型逻辑中，给定任何类型 '''T'''，有一个恒等谓词 id<sub>'''T'''</sub>，带有域和陪域类型 '''T'''；对于类型 '''T''' 的所有 ''x''，它满足 id<sub>'''T'''</sub>(''x'') = ''x''。类似的，如果 '''T''' 是 '''U''' 的一个[[子类型]]，则有一个域类型 '''T''' 和陪域类型  '''U''' 的包含谓词，它满足相同的等式；有与从旧类型构造新类型的其他方式相关联的额外的函数符号。

此外，你可以在证明了适当的[[定理]]之后定义泛函谓词。(如果你在证明了定理之后不允许介入新符号的形式系统下工作，那么你必须使用关系符号来处理，详见下一个章节)。特别是，如果你能够证明对于所有 ''x'' (或特定类型的所有 ''x'')，[[存在量化|存在]]一个[[唯一量化|唯一]]的 ''y'' 满足某个条件 ''P''，则你可以介入一个新的函数符号 ''F'' 来指示它。注意 ''P'' 自身是涉及 ''x'' 和 ''y'' 二者的关系[[谓词]]。所以如果有这样的一个谓词 ''P'' 和定理:
: 对于类型 '''T''' 的所有 ''x''，对于类型 '''U''' 的某个唯一的 ''y''，有 ''P''(''x'',''y'')，
则可以介入一个新的域类型 '''T''' 和陪域类型 '''U''' 的函数符号 ''F'' 满足:
: 对于类型 '''T''' 的所有 ''x''，对于类型 '''U'''的所有 ''y''，有 ''P''(''x'',''y'') [[当且仅当]] ''y'' = ''F''(''x'')。

== 不使用泛函谓词 ==

很多谓词逻辑系统不允许泛函谓词，只允许关系[[谓词]]。这是有用的，例如在证明[[元逻辑]]定理(比如[[哥德尔不完备定理]])的上下文中，这里你不希望允许介入新的函数符号(或任何其他新符号)。但是有一个方法只要前者可以存在就把函数符号替代为关系符号；进一步的，这是算法性的因此适合于应用多数元定理于这个结果。

特别是，如 ''F'' 有域类型 '''T''' 和陪域类型 '''U'''，则它可以被替代为类型 ('''T''','''U''') 的谓词 ''P''。直觉上，''P''(''x'',''y'') 意味着 ''F''(''x'') = ''y''。接着在 ''F''(''x'') 在陈述中出现的任何时候，你都可以把它替代为类型 '''U''' 的新符号 ''y''，并包括另一个陈述 ''P''(''x'',''y'')。为了能够做同样的演绎，你要一个额外的命题:
: 对于类型 '''T''' 的[[全称量化|对于所有]] ''x''，对于类型 '''U''' 的某个[[唯一量化|唯一]]的 ''y''，有  ''P''(''x'',''y'')。
(当然，这是前面章节中在介入新的函数符号之前必须证明为定理的同样的命题)。

因为函数符号的消除对于某些目的是方便的和可能的，很多形式逻辑系统不明确的处理函数符号而只使用关系符号；另一种考虑方式是泛函谓词是特殊种类的谓词，是满足上述命题的特殊谓词。如果你希望指定只适用于泛函谓词 ''F'' 的一个命题[[模式]]就有问题了；如何提前知道它是否满足这个条件? 要得到这个模式的等价公式，首先把形如 ''F''(''x'') 的任何东西都替代为新变量 ''y''。接着在介入对应的 ''x'' 之后(就是说，在 ''x'' 被加以量词之后，或在陈述开始处如果 ''x'' 是自由的)立即就对 ''y'' [[全称量化|加全称量词]], 并用 ''P''(''x'',''y'') 前卫这个量化。最后，使整个陈述是上述泛函谓词的唯一性条件的[[实质蕴涵|实质推论]]。

让我们采用在 [[Zermelo-Fraenkel 集合论]]中[[替代公理]]的例子。这个模式声称，对于任何有一个变量的函数谓词 ''F'':
:<math>\forall A, \exists B, \forall x, x \in A \rightarrow F(x)\in B.</math> 
首先，我们必须把 ''F''(''x'') 替代为其他变量 ''y'': 
:<math>\forall A, \exists B, \forall x, x \in A\rightarrow y \in B.</math> 
当然，这个陈述不正确；''y'' 必须在 ''x'' 之后立即加量词: 
:<math>\forall A, \exists B, \forall x, \forall y, x \in A \rightarrow y\in B.</math> 
我们仍必须介入 ''P'' 来前卫这个量化: 
:<math>\forall A, \exists B, \forall x, \forall y, P(x,y) \rightarrow (x \in A \rightarrow y \in B).</math> 
这是几乎正确的，但是它适用于太多谓词；我们实际需要的是: 
:<math>(\forall x, \exists ! y, P(x,y))\rightarrow (\forall A, \exists B, \forall x, \forall y, P(x,y)\rightarrow (x \in A \rightarrow y \in B)).</math> 
这个版本的替代公理模式现在适合用于不允许介入新的函数符号的形式语言中。可作为选择的，你可把最初的陈述解释为在这种形式语言中的陈述；它只是在结束处生成的陈述的简写。

==参见==
*[[真值函数]]
*[[布尔值函数]]
*[[替代公理]]

[[Category:數理邏輯|F]]
[[Category:模型论]]