自由邏輯

自由邏輯是免除存在性假定的邏輯。或者說，它是定理在包括空域的所有論域中都有效的邏輯。

解說

在經典邏輯中，有些定理明確的假定在論域中必須有東西。考慮下列經典的有效定理。

1. $\forall xA(x)\rightarrow \exists xA(x)$;

2. $\forall xA(x)\rightarrow A(r/x)$ (這裡的 r 對於 A(x) 中的 x 不自由出現，而 A(r/x) 是代換 A(x) 中 x 的所有自由出現的結果);

3. $A(r)\rightarrow \exists xA(x/r)$ (這裡的 r 對於 A(x) 中的 x 不自由出現)。

在等價理論中的一個有效的模式展示了同樣的特徵

4. $\forall x(F(x)\rightarrow G(x))\land \exists xF(x)\rightarrow \exists x(F(x)\land G(x))$。

非形式的，如果 F 是『 =y』, G 是『是天馬』，而我們代換 y 為『天馬』，則 (4) 就允許我們從『同一於天馬的所有東西都是天馬』推出某些東西同一於天馬。問題來自把變量代換為無指派(nondesignating)的常量: 事實上，我們在一階邏輯的標準公式中不能這麼做，因為這裡沒有無指派常量。古典上，∃x(x=y) 是通過特殊化(就是前面的(3))而演繹自開放等價公理 y=y。

在自由邏輯中，(1)被替代為

1b. $\forall xA(x)\land E!t\rightarrow \exists xA(x)$, 這裡的 E! 是一個存在謂詞(在自由邏輯的某些但不是所有的公式中，E!t 可以被定義為 ∃y(y=t))。

可以對存在性引入的其他定理做類似的修改(比如，特殊化規則變成為 (A(r) → (E!r → ∃xA(x)))。

自由邏輯的公理化由 Hintikka (1959)、Lambert (1967)、Hailperin (1957) 和 Mendelsohn (1989) 給出。

來源

• K. Lambert, "Existential Import Revisited", Notre Dame Journal of Formal Logic, October 1963, p.288-292