泛函谓词

在形式逻辑和相关的数学分支中，泛函谓词或函数符号是应用于一个对象项而生成另一个对象项的逻辑符号。泛函谓词有时也叫做映射，但是这个术语还有其他意义。在模型中，函数符号被建模为函数。

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

现在考虑这个形式语言的模型，它带有类型 T 和 U 被建模为集合 [T] 和 [U]，而类型 T 的每个符号 X 被建模为 [T] 中的元素 [x]。则 F 可以被建模为集合

[F]:={\big \{}([x],[F(x)]):[x]\in [\mathbf {T} ]{\big \}},

它简单的是带有域 [T] 和陪域 [U] 的一个函数。[F(x)] = [F(y)] 只要 [x] = [y] 是一致性模型的要求。

介入新的函数符号编辑

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

你还自动的获得特定的函数符号。在无类型逻辑中，有一个恒等谓词 id，对于所有 X 满足 id(x) = x。在有类型逻辑中，给定任何类型 T，有一个恒等谓词 id_T，带有域和陪域类型 T；对于类型 T 的所有 x，它满足 id_T(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) 前卫这个量化。最后，使整个陈述是上述泛函谓词的唯一性条件的实质推论。