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.

2 Answers 2


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 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.

  • Actually, more striking is the fact that PA proves the consistency of every finite fragment of itself. Same for ZFC.
    – user21820
    Dec 12, 2018 at 13:36

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.


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.
  • 1
    I'd forgotten the name of the title of Godels original paper - that would have answered my question directly. Jun 14, 2013 at 17:02
  • @Gugg Thanks for the edit! I can always count on you to add the appropriate umlauts (as well as helpful links I was too lazy to dig up) ;)
    – Dennis
    Jun 14, 2013 at 17:39
  • @Gugg: I second that :) Jun 14, 2013 at 18:25

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .