...[I]n view of the elementary nature of the notion of provability, a precise definition of this notion requires only rather simple logical devices. In most cases, those logical devices which are available in the formalized discipline itself (to which the notion of provability is related) are more than sufficient for this purpose. We know, however, that as regards the definition of truth just the opposite holds. Hence, as a rule, the notions of truth and provability cannot coincide; and since every provable sentence is true, there must be true sentences which are not provable.It was not immediately obvious to me what argument Tarski was making here. It seems worth spelling it out in some detail.
The two central premises are of course clear enough. First, we know that in any theory of sufficient strength (e.g., any theory extending Robinson arithmetic Q), the notion of provability can be formally defined. More precisely, the relation "P is a proof of S in T" can be 'represented' in Q in a familiar sense, and provability in T can then be defined as the existential quantification of this relation. Second, we have Tarski's theorem: For any sufficiently expressive language L, such as the language of arithmetic, there can be no formula Tr(x) that defines truth in L.
What's puzzling about this is what's often puzzling about Tarski's remarks on such topics: The remarks about provability are most familiarly applied to theories, such as Q; but Tarski's theorem is most familiarly applied to languages, such as the language of arithmetic. Tarski famously conflates these two notions in many of his writings on truth. And, in fact, it seems to me that Tarski's argument here is only correct if it is primarily one about languages.
Suppose we try to interpret it as one about theories. There is no formula Tr(x) such that, in PA, we can prove all instances of "Tr(S) iff S". But no matter how we interpret the remarks about provability, it will not then follow that "truth and provability cannot coincide". It's perfectly possible that Tr(x) should have the same extension as Pr(x) even though we cannot prove that fact in PA.
So Tarski must mean something like the following. Consider e.g. the language of arithmetic, or any other sufficiently expressive language. In that language, we can define the notion of provability in PA and, indeed, in any formal theory stated in that langauge: That is, there is, for each such theory, a formula PrT(x) that is true of all and only the Gödel numbers of T-provable sentences. But we know from Tarski's theorem that there is no formula Tr(x) that is true of all and only the Gödel numbers of true sentences of L. Hence, those two sets cannot coincide, no matter what formal theory T might be.
As Tarski mentions in note 18, this is no real improvement over Gödel. Most of the machinery that Gödel develops for the purposes of his proof is needed for this one: the definition of provability and the diagonal lemma. It is perhaps worth mentioning, however, that there is no need to suppose that any particular theory proves anything about T-provability, and no hypothesis of the consistency of T is needed here, either.
There's another puzzling remark that Tarski makes in this paper that I am not sure this one can be salvaged. The remark is one Tarski makes during the discussion of 'essential richness':
If the condition of “essential richness” is not satisfied, it can usually be shown that an interpretation of the meta-language in the object-language is possible; that is to say, with any given term of the meta-language a well-determined term of the object-language can be correlated in such a way that the assertible sentences of the one language turn out to be correlated with assertible sentences of the other. As a result of this interpretation, the hypothesis that a satisfactory definition of truth has been formulated in the meta-language turns out to imply the possibility of reconstructing in that language the antinomy of the liar; and this in turn forces us to reject the hypothesis in question. (pp. 351-2)I take there to be here an assertion of the following claim. Suppose that a theory M is (relatively) interpretable in another theory O. Then truth for the language of O cannot be defined in M (since then the liar would be reproducible in M). So understood, the claim is false. Ali Enayat and Albert Visser showed that PA plus a Tarski-style truth-theory for the language of arithmetic is interpretable in PA. (A proof of the same result is given in my paper "Consistency and the Theory of Truth". I should have mentioned all this there.)
Tarski's unclarity about 'language' vs 'theory' makes it unclear, however, exactly what he meant. So, I take his claim to concern theories because I don't know of any coherent notion of interpretation for languages, and of course Tarski is largely responsible for the notion of interpretation to which he is here alluding. (The paper in which Tarski first introduces and studies this notion would not be published until 1953, however: nine years later.) Moreover, his talk of "reconstructing in that language the antinomy of the liar" certainly sounds like talk of provability. But perhaps there is something else he had in mind.
