泛函謂詞

在形式邏輯和相關的數學分支中，泛函謂詞或函數符號是應用於一個對象項而生成另一個對象項的邏輯符號。泛函謂詞有時也叫做映射，但是這個術語還有其他意義。在模型中，函數符號被建模為函數。

特別是，在形式語言中的符號 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) 前衛這個量化。最後，使整個陳述是上述泛函謂詞的唯一性條件的實質推論。