Is Gödel's incompleteness theorem still valid if one uses a higher-order logic?

Question

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?

Am I correct in thinking that it doesn't, because first-order logic is subsumed in higher-order logic?

Presumably, also, Gödel made use of a Hilbert-style inference system and it doesn't make any difference if natural deduction type inference systems are used instead.

Answer 1

Actually, in higher-order logic, Godel's theorem is extended quite naturally. The long and short of it is that while the Incompleteness theorem holds with regard to a higher-order logic, your intuition that it should not does reflect the following: that a HOL can be regimented into various sublanguages, each of which is capable of formalizing the incompleteness of certain sub-languages of itself.

Let L be our given language, we can then regiment L into an infinite sequence of languages L₀, L₁, ... , L_n. Each L_n is defined as the language which results from augmenting L_n-1 with type n quantifiers, and type 0 is the type of individuals. In each L_n for n > 0, we can formulate a predicate Pr_n(n) which is true of n iff n is the Godel-number of an expression E which is provable in L_n. We can also formulate a function d_n(x) which maps each Godel-number p_n of a predicate P_n (meaning an open sentence with one free variable "x_n-1" of type n-1) to the Godel number of the expression P[p/x]. Taking the godel-number of d_n("~Pr_n(x)"), we have achieved an expression which is true in L_n iff it is not provable in L_n. We can however find a Godel number of a proof in L_n+1 of the expression correxponding to ~Pr_n+1(d_n("~Pr_n(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.

Answer 2

Your assumptions are wrong this time. Gödel used Russell's type theory from Principia Mathematica. Thus Gödel uses a higher-order theory in the original proof (though I'm not sure without taking a deep look how much of the higher-order apparatus is used). In fact, the original paper's (translated) title is "On Formally Undecidable Propositions of Principia Mathematica and Related Systems".

Full second-order logic is also incomplete.

I believe the only requirements on a system to have incompleteness obtain are the following (I might be missing something):

1. Capable of representing primitive recursive functions (at the very least the arithmetical ones).
2. Having a recursively enumerable axiom set.

Once those two hold (modulo my concern that I might be forgetting something), incompleteness applies to that system.

EDIT:

I believe my statement that those are the only two requirements is actually correct (so my concerns were misplaced), Gödel states the conditions as follows:

1. The class of axioms and the rules of inference (i.e., the relation "immediate consequence of") are recursively definable (as soon as the basic signs are replaced in any fashion by natural numbers).
2. Every recursive relation (Note: here Gödel is referring to what are now called primitive recursive functions) is definable in the system.