介入新的函数符号

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

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

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

则可以介入一个新的域类型 T 和陪域类型 U 的函数符号 F 满足:

不使用泛函谓词

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

特别是，如 F 有域类型 T 和陪域类型 U，则它可以被替代为类型 (T,U) 的谓词 P。直觉上，P(x,y) 意味着 F(x) = y。接着在 F(x) 在陈述现的任何时候，你都可以把它替代为类型 U 的新符号 y，并包括另一个陈述 P(x,y)。为了能够做同样的演绎，你要一个额外的命题:

(当然，这是前面章节中在介入新的函数符号之前必须证明为定理的同样的命题)。

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

让我们采用在 Zermelo-Fraenkel 集合论中替代公理的例子。这个模式声称，对于任何有一个变量的函数谓词 F:

首先，我们必须把 F(x) 替代为其他变量 y:

当然，这个陈述不正确；y 必须在 x 之后立即加量词:

我们仍必须介入 P 来前卫这个量化:

这是几乎正确的，但是它适用于太多谓词；我们实际需要的是:

这个版本的替代公理模式现在适合用于不允许介入新的函数符号的形式语言中。可作为选择的，你可把最初的陈述解释为在这种形式语言中的陈述；它只是在结束处生成的陈述的简写。

参见

真值函数

布尔值函数

替代公理

免责声明：以上内容版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。感谢每一位辛勤著写的作者，感谢每一位的分享。