A 3/4 year ago, I read Gödel's beautiful paper "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme 1". There is one thing, I never understood.

In a footnote, Gödel says the following:

"Der wahre Grund für die Unvollständigkeit, welche allen formalen Systemen der Mathematik anhaftet, liegt, wie im zweiten Tell dieser Abhandlung gezeigt werden wird, darin, dass die Bildung immer höherer Typen sich ins Transfinite fortsetzen lässt, während in jedem formalen System höchstens abzählbar viele vorhanden sind. Man kann nämlich zeigen, dass die hier aufgestellten unentscheidbaren Sätze durch Adjunktion passender höherer Typen (z. B. des Typus $\omega$ zum System $P$) immer entscheidbar werden. Analoges gilt auch für das Axiomensystem der Mengenlehre"

Meltzer's translation renders this in English as:

"The true source of the incompleteness attaching to all formal systems of mathematics, is to be found — as will be shown in Part II of this essay — in the fact that the formation of ever higher types can be continued into the transfinite (cf. D. Hilbert 'Über das Unendliche', Math. Ann. 95, p. 184), whereas in every formal system at most denumerably many types occur. It can be shown, that is, that the undecidable propositions here presented always become decidable by the adjunction of suitable higher types (e.g. of type $\omega$ for the system $P$). A similar result also holds for the axiom system of set theory."

Famously, Gödel never published part 2 of his paper.

Is the theorem which states that the undecidable propositions presented by Gödel become decidable by the adjunction of suitable higher types proved by someone? Has someone formulated Gödel's idea more precisely? Is there any research in this area?

  • $\begingroup$ Thanks for adding the translation. The translation is suitable ;-D $\endgroup$ – asdfusername Jul 9 '15 at 15:53
  • 3
    $\begingroup$ There's some work by Lambek, and Lambek and Scott exploring the relation between Gödel's theorems and the free topos (see references at ncatlab.org/nlab/show/free+topos#references) that might be enlightening. $\endgroup$ – David Roberts Jul 9 '15 at 17:02

I think the main idea here is that, if you have a reasonably strong formal system $T$ (so that the incompleteness theorems apply to it) and you then strengthen it to a "higher type" system $T^+$ in which you can talk about (and quantify over) subsets of the universe that $T$ describes (so that second-order concepts from the point of view of $T$ are first-order from the point of view of $T^+$) and if $T^+$ has suitable comprehension axioms, then $T^+$ will be able to formalize a definition of truth for the language of $T$ and prove that the axioms of $T$ are true and that formal deduction preserves truth. Thus, $T^+$ can prove the consistency of $T$ and, as a consequence, prove the usual Goedel sentence of $T$.

Typical examples are: (1) $T$ is Peano arithmetic and $T^+$ is second-order arithmetic. (2) $T$ is Zermelo-Fraenkel set theory and $T^+$ is Morse-Kelley class theory. (3) (the example Goedel mentioned) $T$ is type theory with an $\omega$-indexed hierarchy of types and $T^+$ is type-theory with an $(\omega+1)$-indexed hierarchy of types.

  • $\begingroup$ And in what sense does the fact that we can strengthen a theory $T$ to a higher type system $T^{+}$ (in which we for example can prove that $T$ is consistent) cause the incompleteness of $T$? I am just curious, since Gödel speaks about this as the "reason of the incompleteness of formal systems". $\endgroup$ – user99916 Nov 16 '16 at 15:20
  • $\begingroup$ @Nullachtfünfzehn I don't think our ability to strengthen $T$ to $T^+$ (or, more accurately, the existence of $T^+$, never mind our abilities) causes incompleteness of $T$. I'd rather interpret Gödel's remark epistemologically: The existence of $T^+$ helps us to understand what's going on with undecidable sentences (specifically with Gödel's "I am unprovable" example). These sentences express, in the language of $T$, some of the additional information that becomes available when we adopt stronger theories like $T^+$. $\endgroup$ – Andreas Blass Nov 16 '16 at 16:28
  • $\begingroup$ I agree, and find it strange that Gödel asserted that this in fact causes incompleteness. Another question: Gödel said: "whereas in every formal system at most denumerably many types occur". How do you interpret this? Did he mean that every formal system has a countable model (in the sense proven by Löwenheim and Skolem)? $\endgroup$ – user99916 Nov 17 '16 at 17:15
  • $\begingroup$ @Nullachtfünfzehn I had always assumed that Gödel intended "occur" to mean "are mentioned explicitly", but This was just an assumption and he might well have meant something more subtle. $\endgroup$ – Andreas Blass Nov 18 '16 at 21:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.