[mathjax]Let’s distinguish what I’ll call the Diagonalization Equivalence from the familiar Diagonalization Lemma. The former is a semantic claim: in the right conditions, for any one-place predicate 
of theory T there is a corresponding sentence 
such that is true if and only if 
is true. The latter is a syntactic claim: in the right conditions, for any one-place predicate of theory T there is a corresponding sentence such that 
.
In the previous post, I claimed that in his §35 Carnap proves the semantic Diagonalization Equivalence, which he uses in §36 to prove the semantic version of Gödel’s First Theorem. But I said he doesn’t prove the Lemma there or give the now canonical syntactic version of the Theorem (the one depending on the syntactic assumption of 
-consistency).
Well, no one has protested yet. So, thus emboldened, let me now stick my neck out further!
What happens later in the book? Carnap’s notation and terminology together don’t make for an easy read. But as far as I can see, when he returns to Gödelian matters later, he still is using the semantic Diagonalization Equivalence and not the syntactic Diagonalization Lemma. If the latter was going to appear anywhere, you’d expect to find it in §60 when Carnap returns to the incompleteness of arithmetics: but it isn’t there. (An indication: Carnap here talks of provability being ‘definable’ in arithmetics, and it is indeed expressible — but we know it isn’t capturable/representable by a trivial argument from the Diagonalization Lemma proper. So Carnap hereabouts is still dealing with semantic expressibility, and doesn’t seem to invoke the syntactic notion of capturing/representing needed for the Lemma.)
So, in summary: Yes, Carnap gives a nice tweak to the argument in §1 of Gödel 1931 for the semantic incompleteness theorem, by generalizing the basic idea to give the Diagonalization Equivalence. But this isn’t the modern Diagonalization Lemma. Which isn’t to say that we can’t get the Lemma easily using the wff Carnap constructs: however, as far as I can see, Carnap didn’t explicitly take the step in 1934, even though he is often credited with it.
What am I missing?
I remember looking up Carnap’s book for a similar reason, and coming to the conclusion that Carnap had done something similar to the diagonalization lemma, which was close enough that other people would probably not be willing to take credit for the diagonalization lemma itself, and so Carnap was credited for it even though he did not state it in the modern form. I also suspected that some of the credit to Carnap might stem from personal communications. However, I am not very familiar with the history myself.
Separately, although it just repeats the attribution to Carnap, the paper “On Gödel’s Way in: The Influence of Rudolf Carnap” by Goldfarb (BSL 11, 2005) may have something of interest.
I’ve now had the chance to check this. The Diagonal Lemma/Fixed-Point Theorem isn’t stated as such in Tarski, Mostowski and Robinson but is easily derived from what the three say in section 2, “Definability in arbitrary theories”, in the jointly authored second paper (see pp. 44-47 of the Dover reprint). But since interested there only in decidability, the steps in the derivation aren’t even hinted at. So who did first make that easy derivation? One of Tarski’s students?
[In his ‘Theories incomparable with respect to relative interpretability’ of 1962 Richard Montague refers to the diagonal lemma for Robinson Arithmetic as “well known” and refers to “the familiar proof”.]
Oh! Soemthing happened to the end of my comment. The Gaifman should continue “If we consider the function that maps every sentence χ to α (‘χ’), then σ is mapped to a sentence equivalent to it in T. For this reason the theorem is often known as the fixed point theorem. It is sometimes also called the self-reflection lemma and also diagonalization lemma. Carnap published this observation in [1934] and Gödel stated it in his 1934 paper, referring to Carnap in a footnote. Although the proof generalizes in an obvious way an argument used first by Gödel, anyone who goes through Gödel’s lengthy manuscript will see that it is not at all trivial to extract it from the host of details. Gödel himself did not seem to notice it. Carnap’s role is ignored today, but it is fitting that Carnap’s role be remembered. I shall refer to it as the Gödel-Carnap fixed point theorem. The theorem has numerous applications.
“Nowadays the incompleteness result is usually proved by stating and proving first the Gödel-Carnap fixed point theorem, and then by applying it for the case α(v) = ¬∃ z Proof(z,v). This reverses the historical order. It also endows the fixed point construction with an aura of a magic trick.”
Gödel’s attribution to Carnap occurs on p. 63 of the reprint of Gödel 1934 in Martin Davis’s The Undecidable. Maybe I’m missing somehting but I don’t see in the text on pp. 63-4 where an account of the general diagonalization procedure is given an unambiguous claim to provability of an equivalence inside the theory.
Thanks for all this, Peter.
I don’t know Carnap 1934a either — so I can’t comment on that.
But as it chances, I was reading Rosser 1939 just yesterday. His Lemma 1 seems clearly to be a statement of the semantic Diagonalization Equivalence (as I called it) rather than the syntactic Diagonalization Lemma (and that’s all his proof delivers — it’s all about what can be expressed, not what can be numeralwise represented (or whatever your favourite jargon is).
Gaifman’s ‘ function that maps every sentence χ to α (‘χ’) equivalent to it in T’ is ambiguous between whether it is semantic equivalence or provable equivalence which is in question. His remark about what is trivial to extract doesn’t seem that apt to the semantic Diagonalization Equivalence (once you’ve cracked Gödel’s rather obtuse mode of presentation in 1931). But true, it is perhaps slightly less trivial to extract the Diagonalization Lemma proper, but then I can’t see that Carnap got it clearly either.
And yes, I agree entirely about Gödel’s added footnote.
A small remark: If you know the English translation of Logische Syntax, you essentially also know Carnap1934a. This paper contains material that Carnap could not include in the original German version, as the publisher wanted to keep the book short. It is, however, contained in the English translation (cf. the preface to the latter).
From Andera Cantini’s article on Paradoxes and Contemporary Logic at the Stanford Encyclopedia of Philosophy
“Gödel’s construction was soon given a general form, as a general diagonalization lemma, which refers to arbitrary definable properties. This is to be found in Carnap 1934b, p. 91, Carnap 1934a, p. 270, and in Rosser 1939, p. 57, Lemma 1:
For every formula ψ(v) with only v free, there exists a sentence φ such that
φ ↔ ψ(⌈φ⌉)
is provable.
“As a matter of fact the lemma has become the standard tool for producing self-referential statements and for transforming the semantical paradoxes into indefinability and (formal) undecidability results. The algebra underlying the Gödelian constructions will be grasped only much later during the 1970’s. It is also important to stress that a few years later (1938) an analog of the diagonalization lemma (the so-called second recursion theorem) was discovered by Kleene and was soon to become a basic tool in the foundations of recursion theory and computability theory.
“Carnap, R., 1934a, “Die Antinomien und die Unvollständigkeit der Mathematik”, Monatshefte für Mathematik und Physik, 41:263–284.
–––, 1934b, Die logische Syntax der Sprache, Berlin: Springer.
Rosser, J. B., 1939, “An informal exposition of proofs of Gödel’s and Church’s theorem”, Journal of Symbolic Logic, 4:53–60.”
Looking at Rosser’s Lemma 1, I’m not convinced. I can’t get hold of Carnap’s 1934a.
In ‘Naming and Diagonalization, from Cantor to Gödel to Kleene’, Logic Journal of the IGPL, October 2006, pp. 709 – 728, Haim Gaifman starts with a sketch of a proof of Godel’s Theorem via a fixed-point theorem says, “To complete this brief historical note, Carnap in [1934] observed that Gödel’s construction can be generalized so that it yields, for any given α(v), a fixed point. In [Gödel 34] Carnap is given credit for this and his work is cited. The generalization, which now appears obvious, was not at all obvious in 1934. Anyone who will go through Gödel’s original proof will see that achieving the right perspective is not a trivial matter. I therefore suggest that Carnap’s contribution not be forgotten and that the theorem be referred to as the Gödel-Carnap fixed point theorem.”
In lecture notes Gaifman says, “One of the earliest logicians ─ perhaps the first ─ to read carefully Gödel’s manuscript was Carnap. Analyzing the proof, he noticed that the argument that leads from (12) to (14) is of a general character and does not depend on the wff ¬∃ z Proof(z, v). The same construction can be applied to any wff α(v), resulting in a sentence that “says of itself” that it has the property described by α(v) …”, gives a version of the fixed point construction, then goes on to say, “If we consider the function that maps every sentence χ to α (
Unfortunately I don’t have Carnap’s book either but I recall that one proffesor of mine had a script on Gödel incompleteness theorems. His name is Siegfried Gottwald and his script is available at . Looking at the part of the diagonalization lemma (page 7) it seems he thinks that the diagonalization equivalence leads to the diagonalization lemma. He quotes a remark make by Carnap in §35 as reference.
Script is at http://www.uni-leipzig.de/~logik/gottwald/unvollst.pdf
I thought that the wonderful Mostowski (wonderful for both his bio and his brain) was the most likely. I finally got around to pulling Sentences Undecidable in Formalized Arithmetic off the shelf. It’s billed as an exposition of the Gödel results, but really it’s a dotting of the i’s and crossing of the t’s, as well as a careful characterization of general recursiveness. Moreover, I think the diagonal lemma, not so-called, is on page 89.
Re-reading my comment, I see it isn’t clear that I mean the crossing of i’s comment to be real praise of what Mostowski accomplished.
> So, who did first make the next step?
I can’t check this at the moment, but I’d suggest Tarski, Mostowski and Robinson.
Gosh, I think you’re right. I had rummaged into §60 and following, hoping to see the lemma “pulled down”. I think it’s almost there (isn’t there a passage about the difference between proof of and provable? I’m away from the book right now.)
So, who did first make the next step? I’ve thought Carnap ever since the .5 edition of B&J. Who would know? (If contemporary to Carnap, von Neumann and Bernays had the chops…. Of course, so did Gödel.)
I’ve never read Carnap so I was hesitant to post on the previous topic but if it’s two whole topics of silence ……
What exactly is the semantics Carnap is using? It must not be standard first order logic semantics because there are structures for (say) the language of PA where Godel’s first incompleteness theorem fails. For example: the structure with exactly one element. Of course, this badly fails the axioms of Peano Arithmetic. So is Carnap’s semantics something like “truth across all models which satisfy the axioms of Peano Arithmetic”? If so, then syntax and semantics are the same, in sight of the completeness theorem.
I think the reason these posts haven’t gotten more comments might be because they’re not self-contained, only people who have read Carnap can answer them authoritatively…
Well, yes, I was rather hoping someone who does know their Carnap better than I would help out! The backstory is that the attribute to Carnap is common, and indeed is made by one P*t*r Sm*th in the first edition of his Gödel book! I wanted to check this was right before repeating it in the Second Edn. And more generally, I want to get a better first-hand sense of the history here.
As to Carnap’s semantics: basically, for an arithmetic sentence, ‘true’ for him means true-in-the-intended-interpretation (or in-the-standard-model, if you prefer). Not that he talks quite that way. But in effect he pins down the standard interpretation by requiring that the omega-rule is sound.