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

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?

## 最佳答案

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.