一千萬個為什麽

搜索

如果使用高階邏輯,哥德爾的不完備性定理是否仍然有效?

Gödel's incompleteness theorem is wholly formal (in my understanding), and relies on a proof system that I assume is first-order. Does it make any difference to the theorem if higher-order logic is used?

我是否認為它不正確,因為一階邏輯被包含在高階邏輯中?

據推測,哥德爾也使用了希爾伯特式推理系統,但它並沒有如果使用自然演繹類型推理系統,則會產生差異。

最佳答案

實際上,在高階邏輯中,Godel定理很自然地擴展了。它的長期和短期是,雖然不完備性定理關於高階邏輯,但你的直覺不應該反映以下內容:HOL可以被制定成各種子語言,每個子語言都能夠形式化某些子語言本身的不完整性。

Let L be our given language, we can then regiment L into an infinite sequence of languages L0, L1, ... , Ln. Each Ln is defined as the language which results from augmenting Ln-1 with type n quantifiers, and type 0 is the type of individuals. In each Ln for n > 0, we can formulate a predicate Prn(n) which is true of n iff n is the Godel-number of an expression E which is provable in Ln. We can also formulate a function dn(x) which maps each Godel-number pn of a predicate Pn (meaning an open sentence with one free variable "xn-1" of type n-1) to the Godel number of the expression P[p/x]. Taking the godel-number of dn("~Prn(x)"), we have achieved an expression which is true in Ln iff it is not provable in Ln. We can however find a Godel number of a proof in Ln+1 of the expression correxponding to ~Prn+1(dn("~Prn(x)").
When we arithmetize the the expression Pr(x), which is true iff x is the Godel number of an expression which is provable in L, we find ourselves once again in the familar predicament. d("~Pr(x)") is semantically true but not provable.

轉載註明原文: 如果使用高階邏輯,哥德爾的不完備性定理是否仍然有效?