One very common informal statement of Gödel’s theorem is that it shows that for any (sufficiently strong consistent blah blah) formal system, there are truths that it can’t prove. And if you don’t formulate Gödel’s incompleteness theorem that way, at least you state this as a corollary: Gödel’s theorem shows that truth and provability (in any one formal system) come apart. But if you read Gödel”s original paper(s) on incompleteness, you are probably struck by the fact that Gödel doesn’t say this. In fact, the word “wahr” doesn’t even appear in Gödel’s 1931 paper. I think Gödel doesn’t note this consequence until the 1934 Princeton lectures (p. 363 of Collected Works I). A number of reasons have been offered for this: a) he was reacting against Hilbert, so he wanted to keep everything purely finitary, b) he was working in the context of the Vienna Circle, and they considered “truth” to be a suspect, metaphysical notion. This is an aspect that people interested in Gödel’s platonism have written extensively about, since Gödel claimed that even at the time of writing the 1931 paper he was a platonist.

So who was the first to note this consequence in print? My money is on the guy who made truth respectable among the logical empiricists. Here’s the end of Tarski’s “Einige Betrachtungen über die Begriffe der ω-Widerspruchsfreiheit und der ω-Vollständigkeit“, Monatshefte für Mathematik und Physik 40 (1933) 97-112 (the paper was received in July 1932), translated as “Some observations on the concepts of ω-completeness and ω-consistency”, Logic, Semantics, Metamathematics, 2nd ed., pp. 279-295:

[T]he following is worthy of emphasis: the profound analysis of Gödel’s investigations shows that whenever we have undertaken a sharpening of the rules of inference, the facts, for the sake of which this sharpening was felt to be necessary, still persist, although in a more complicated logical structure. The formalized concept of consequence will, in extension, never coincide with the ordinary one, the consistency of that system will not prevent the possibility of ‘structural falsehood’. However liberally we interpret the concept of the deductive method, its essential feature has always been (at least hitherto) that in the construction of the system and in particular in the formulation of its rules of inference, use is made exclusively of general logical and structurally descriptive concepts. If now we wish to regard as the ideal of deductive science the construction of a system in which all the true statements (of the given language) and only such are contained, then this ideal unfortunately cannot be combined with the above view of the deductive method.

Now here’s something puzzling. The translation has a footnote to this passage which is not in the original:

The validity of the remarks stated in the last paragraph essentially depends on the decision not to use in metamathematical discussion any devices which cannot be formalized within the framework of the theory of types of Principia Mathematica. But as soon as we abandon this decision and allow ourselves to use stronger devices in metamathematical discussion, most of the remarks as originally formulated lose their validity and the whole paragraph requires a thorough revision.

What in the passage quoted depends for its validity on metamathematics being formalizable in PM? Maybe that if the metatheory is stronger than PM, you can define a “formalized notion of consequence” which characterizes the true statements of PM, e.g., using an ω rule. But Tarski just did that immediately before the quoted passage and says that the resulting formalized notion of consequence is not “in harmony with the current view of the deductive method”. So what can he have in mind here?

Church-Turing thesis + the system is recursively enumerable (or if you prefer is primitive recursive)

Tarski’s original comments are to the effect that as long as we consider a system that adheres to the “deductive method” — even when this is interpreted “liberally” — we can’t have a complete system. And this is just as true if we take the deductive method to mean “any system that produces an r.e. set of theorems” as the previous comment suggests. But the footnote indicates that this no longer holds when the metatheory is stronger than PM. No amount of strengthening the metatheory will make it the case that Gödel’s theorem no longer apply to any r.e. theory.

Hi, I hope I will be able to explain what I meant in my previous comment, which I wrote in hurry.If CT fails, there can be finitist theories of mathematics which are not r.e. Hence Godel’s theorem can not be applied to them (one can argue about this possibility but I don’t think we can rule it out completely.) As far as I understand (please correct me if I am wrong, I am no expert on Tarski) what Tarski means by deductive method can include such a system, although it is not algorithmic in the sense of CT. (A deductive method that might require intelligent decisions which includes all of the mathematics (at that point of history) was important, although probably we have got used to deductive systems in much narrower sense) One reason that Godel had not pointed out the point Tarski made was probably that he was not convinced of CT at the time of writing his paper (but one has to check it in his collected works which I don’t have access to currently. If I remember currectly, there was some discussion about it in the discussion before the paper in the collected works.) I hope I am clarifying my comment more than making it more incoherent.By the way, I enjoy reading your blog.

I see what you mean. But I’m doubtful as to whther this is what Tarski had in mind here. For one, I guess the footnote is from a late date, perhaps the publication of the first edition of the collection Logic, Semantics, metamathematics (1956). By that time I think Tarski and Gödel had accepted CT.