[FOM] On Gödel's Enigmatic Footnote 48a

[Jeffrey Ketland]

Dear Panu,

>There is a rather nice discussion of this issue in:
>Roman Murawski: Undefinability of truth. The problem of the priority:
>Tarski vs. Gödel, History and Philosophy of Logic 19 (1998), 153-160.
>one can find the paper in Murawski's homepage:
>http://www.staff.amu.edu.pl/~rmur/

Many thanks for this.

But I still wish to reiterate my puzzlement about Gödel's footnote 48a:

      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 (c.f., 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 become 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.
      (Gödel 1931, footnote 48a.)

As we know, Part II didn't appear. It's not really this that bothers me.
What bothers me is Gödel's claim:

      Higher-Order Decidability Claim:
      "The undecidable propositions here presented become always
      become decidable by the adjunction of suitable higher types."

How could Gödel have known about this phenomenon in 1931? This is about four
years before Tarski writes about it the Postscript to his long 1935/6 paper.
E.g., we know that Z_{n+1} proves Con(Z_n) and relatedly ACA proves Con(PA)
and MK proves Con(ZF) and so on.

But how could Gödel have known about this sort of phenomenon even in 1931?
He doesn't give the slightest indication how the proof goes. The proof that
I am familiar with is that we can give a formalized truth definition for L_n
sentences inside L_{n+1}, and then we can prove in Z_{n+1} the global
reflection principle "All theorems of Z_n are true". This gives us Con(Z_n).
Similarly for ACA and MK.

So far as I am aware, this phenonenon---the decidability of Gödel-type
propositions by
higher-order semantical methods---is first explicitly discussed by Alfred
Tarski around four years later, in the Postscript which appears in his
1935/6 Der Wahrheitsbegriff paper (which is a German translation of the 1933
Polish book). In the Postscript, Tarski wrote,

         The definition of truth allows the consistency of a deductive
         science to be proved on the basis of a metatheory which is
         of higher order than the theory itself. On the other hand, it
         follows from Gödel’s investigations that it is in general
         impossible to prove the consistency of a theory if the proof
         is sought on the basis of a metatheory of equal or lower order.
         Moreover, Gödel has given a method for constructing
         sentences which---assuming the theory concerned to be
         consistent---cannot be decided in any direction in this theory.
         All sentences constructed according to Gödel’s method possess
         the property that it can be established whether they are true or
         false on the basis of the metatheory of higher order having a
         correct definition of truth. Consequently, it is possible to
         reach a decision regarding these sentences, i.e., they can be
         either proved or disproved. (Tarski 1935/6 (1956), p. 274).

If I understand what Gödel is saying in footnote 48a, where he writes that
"the undecidable propositions here presented become always become decidable
by the adjunction of suitable higher types", it seems to me that Gödel had
already anticipated Tarski's conclusion some four years before Tarski's
discussion appeared!

The only explanation I can think of is that Gödel must have already worked
out at least some of the details of formalized semantics *before* his 1931
paper appeared. That's the only explanation I can provide for his enigmatic
comment in footnote 48a. (I agree that this is meagre evidence.) It's true
that Gödel never wrote this stuff down, and when he discusses the
developments in formalized semantics (e.g., briefly in the 1934 Princeton
lectures), he is always extremely generous in referring to both Tarski and
Carnap. I'm certainly not suggesting that Tarski's profound work on the
basis of scientific semantics was somehow dependent on Gödel's. We have
plenty of evidence that Tarski had worked out a good deal of his theory in
Warsaw quite independently in the late 1920's, before Gödel appears on the
scene.

What I'm suggesting is that Gödel might also have worked out some of these
ideas about the formalized treatment of semantics for himself, but for some
unknown reason didn't publish his findings. This is not necessarily hard to
understand. One possibility, in fact discussed in the Feferman paper that
Charlie Silver has just mentioned, is that Gödel was intimidated by the
dominant prejudice of the formalists and logical positivists against the
notion of objective truth---a central conceptual matter that divided
Russell, Gödel, Popper and Tarski (who all thought the notion of objective
truth made sense, and had a central role to play in the epistemology of
science) from the Vienna Circle positivists, particularly Neurath (who
thought that truth was a metaphysical concept).

Best wishes --- Jeff

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Jeffrey Ketland
School of Philosophy, Psychology and Language Sciences
University of Edinburgh, David Hume Tower
George Square, Edinburgh  EH8 9JX, United Kingdom
jeffrey.ketland at ed.ac.uk
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~