18

Has anybody read each and every line of the English translation of the 1931 Gödel paper (from page 40 to the end)?

I tried once, but the notation is so far from the modern notation, and the setup is so strange (use of arbitrary-order formulas) that I found it quite difficult to follow.

If somebody managed to get to the end, I have the following question for him (her).

  1. Is this proof purely syntactic?
  2. Does it avoid the completeness theorem?

The proofs I read all use the completeness theorem at some point, so I wonder what a purely syntactic proof would be like, if it happens to exist.

user3840170
  • 190
huurd
  • 995
  • 8
    There is this little book...
    Frege and Gödel by Jean van Heijenoort (Editor)
    The second half is on Gödel's paper: The complete text, and discussion for the modern reader.     – Gerald Edgar Apr 23 '23 at 08:43
  • 2
    I found "from Frege to Godel" by Jean van Heijenoort, are you refering to that book, or is there another one called "Frege and Godel" by the same author ? – huurd Apr 23 '23 at 09:19
  • 3
    Frege and Gödel contains only the first and last chapters of From Frege to Gödel. The other chapters cover the development of mathematical logic between those two. – Gerald Edgar Apr 23 '23 at 09:28
  • Ok, so I didn't find "Frege and Godel" unfortunately. – huurd Apr 23 '23 at 09:51
  • 6
    If you get From Frege to Godel, then if you like you can ignore everything but the Gödel chapter. – Gerald Edgar Apr 23 '23 at 09:54
  • Thank you for your suggestion, I read the comments of Jean van Heijenoort about Godel's paper, but it does't help in answering my question. If anyone knows the answer, please let me know. – huurd Apr 23 '23 at 10:20
  • I have just come across this book recently. I hope it's relevant... – Akira Apr 23 '23 at 15:41
  • Thank you, I will have a look ! – huurd Apr 23 '23 at 15:46
  • 3
    The recent booklet "Gödel’s Incompleteness Theorems" by Juliette Kennedy seems to also discuss the details of the original proofs. – Michael Greinecker Apr 24 '23 at 13:02
  • @Michael Greinecker : great, thank you ! – huurd Apr 24 '23 at 14:57

2 Answers2

21

I have read it and I strongly recommend its reading in detail, the payoff is immense given that many details about the Gödel sentence (e.g., that it is equivalent to a certain arithmetical sentence) gives a lot more information than just the diagonal argument with which it is usually presented in later accounts. I put it first in the top 3 papers in mathematics I have ever read.

As far as I remember, the only mention of Gödel completeness theorem is in footnote 55 appended to his Proposition IX (page 69 of the file in your link). But this is just a remark about a particular consequence of this proposition, and no use of this completeness theorem is made in his proof.

Another thing that is very clear from his paper is the difference between theory and metatheory which in this translation is pointed out by the use of italics; thus a provable formula is the arithmetized version of the meta-theoretical concept (other editions use upper case letters instead of italics, which is even clearer).

Connections to Hilbert's tenth problem are also indicated due to the careful arithmetization procedure which he carries out throughout his 46 definitions (pp. 52 to 58). These were later exploited by Martin Davis to provide a normal form for recursively enumerable sets, crucial for the solution (in the negative) of Hilbert's problem.

godelian
  • 5,682
  • 1
    What is the meaning of the use of variables of arbitrary order by Godel in this paper ? why doesn't he stick to first order formulas ? – huurd Apr 23 '23 at 13:45
  • 3
    @huurd His paper focuses specifically on the system of Principia Mathematica which was built with a rudimentary type theory in response to Russell's paradox. Gödel treats in detail this foundation but it is clear from his proof (and he claims it) that the same argument can be carried out in other foundational systems like e.g. ZFC. – godelian Apr 23 '23 at 13:52
  • 1
    In the book "from Frege to Gödel" p 592, the author says "The logical axioms are equivalent to the logic of Principia mathematica without the ramified theory of types. The arithmetic axioms are Peano's, properly transcribed." What does mean "logical axioms" ? – huurd Apr 23 '23 at 14:24
  • @huurd The logical axioms are the tautologies, i.e., validities (in every structure) of the system. Arithmetical axioms only hold in certain structures (e.g., the standard model) – godelian Apr 23 '23 at 14:29
  • I see, but the signature used by Godel includes the membership symbol of ZFC, why didn't he just used the nowadays standard signature of Peano arithmetic ? well, I guess that in order to understand that I have to read about Principia Matematica.. can you recommand a modern review of that to avoid getting into the original Russel's book ? – huurd Apr 23 '23 at 14:36
  • 3
    @huurd There is no such membership symbol. The epsilon letter is used in this translation to denote bounded minimization operation, and is defined at the beginning of page 48. I don't think there is much need to study the system of Principia much more than what is described in the paper. – godelian Apr 23 '23 at 15:17
  • Ok so I will try again to dive into the paper. – huurd Apr 23 '23 at 15:20
  • But do you agree this paper is not easy to read for a modern reader because of old fashion notations ? another striking fact is the relative shortness of this proof compared to modern proofs : does it mean that Godel's proof contains shortcuts ? – huurd Apr 23 '23 at 15:27
  • 2
    @huurd It's certainly not an easy read and one has to invest some time and energy to situate in the historical context. Also, the proof of Gödel's second theorem is only sketched, which explains the short length. He intended to give a full proof in a subsequent paper that never came out, since his paper got immediate acceptance. He's known for the dense prose and that's his style. Maybe you can first complement with other expositions and return later to this one. – godelian Apr 23 '23 at 15:34
  • I have read modern proofs all the way through, but when I came to read that one I got lost at many points and couldn't connect the dots. But I'll give it another try ! – huurd Apr 23 '23 at 15:39
13

Certainly the incompleteness theorem can be proved purely syntactically and without reference to the completeness theorem. There is another MO question with more details.

I haven't worked through the original proof in detail, but I'm sure that Gödel took pains to limit himself to syntactic arguments since Hilbert's program was one of the major motivations for his investigations. As for the completeness theorem, I'm surprised that you say that all the proofs you have read use the completeness theorem, because I don't think I've seen any proof that uses the completeness theorem. Can you cite an example where the completeness theorem is used to prove the incompleteness theorem?

EDIT: I was able to find Google Books snippets of the Cori–Lascar reference mentioned by the OP in the comments below. (I think that ${\cal P}_0$ denotes something like Robinson's arithmetic and $\cal P$ denotes something like first-order Peano arithmetic, but this notation was not defined in the snippets that I was able to view.) As you can see, the completeness theorem is indeed invoked in the proof of the second incompleteness theorem. But once again, as discussed in the other MO question, the completeness theorem is not really needed for the proof.

enter image description here enter image description here

[stuff skipped]

enter image description here

[stuff skipped]

enter image description here

Timothy Chow
  • 78,129
  • 1
    For example, in the book "Mathematical Logic: A Course with Exercises Part II: Recursion Theory, Gödel’s Theorems, Set Theory, Model Theory" by Cori-Lascar, the proof makes use at some point of the completeness theorem. – huurd Apr 23 '23 at 13:28
  • It is usually said of the famous Godel sentence that it is "true, but not provable in Peano". What could mean "true" from a purely syntactic point of view ? This sentence is true (i.e. satisfiable) in the standard model N, but I can't imagine any definition of this notion just using syntactic means. – huurd Apr 23 '23 at 13:34
  • Addendum : what meant "true sentence" in mathematical logic of the 30's ? and more specifically for Godel ? – huurd Apr 23 '23 at 13:48
  • 3
    @huurd I agree that "true" is defined in terms of the satisfaction relation, but the statement of Gödel's incompleteness theorem does not require the word "truth." – Timothy Chow Apr 23 '23 at 13:54
  • Can you give me an example of a purely syntactic modern proof of Godel's incompleteness theorem ? – huurd Apr 23 '23 at 14:15
  • 4
    Defining the truth of sentences in a model does not in any way require the completeness theorem. – Emil Jeřábek Apr 23 '23 at 15:18
  • @Emil Jeřábek : you're right, but this is not what I said. – huurd Apr 23 '23 at 15:22
  • @huurd I'm not exactly sure what you mean by "purely syntactic"; some people I've talked to mean that they want to avoid not just semantics but also avoid arithmetic. If arithmetic bothers you, then you could try taking a look at Quine's Mathematical Logic, paying special attention to his discussion of "protosyntax*. – Timothy Chow Apr 23 '23 at 18:38
  • 2
    @huurd Alternatively, you might take a look at Lawrence Paulson, A Machine-Assisted Proof of Gödel's Incompleteness Theorems for the Theory of Hereditarily Finite Sets, which goes into explicit detail about many points which tend to be glossed over in other accounts. – Timothy Chow Apr 23 '23 at 18:47
  • @Timothy Chow : by purely syntactic I mean using only the syntactic definition of a formal proof, and not refering at all to the completeness theorem (provable = true in every model). Arithmetic does not bother me. – huurd Apr 23 '23 at 18:49
  • @huurd Okay, well, that's a much easier request to satisfy. You might try Gödel Without (Too Many) Tears by Peter Smith. Notice for example that in Chapters 12 and 13, he explicitly distinguishes between the "semantic" version and the "syntactic" version. – Timothy Chow Apr 23 '23 at 18:55
  • @Timothy Chow : ok thank you, I will have a look. So now, do you agree that most of the modern proofs of Godel's theorem rely at some stage on the equivalence provable iff true in every model ? – huurd Apr 23 '23 at 18:59
  • 6
    @huurd No, I do not. I have no easy access to the book you cited, but as I said, I don't think I've ever encountered a proof of Gödel's incompleteness theorem that relies on Gödel's completeness theorem. I'm just giving one specific reference that is freely available online which tries to be explicit on this point. Even "semantic" proofs don't rely on Gödel's completeness theorem, as Emil Jeřábek has pointed out. – Timothy Chow Apr 23 '23 at 19:02
  • @Timothy Chow : yes indeed, P_0 means Robinson arithmetic in Cori-Lascar book. – huurd Apr 24 '23 at 17:29
  • 5
    So they somehow invoke the completeness theorem to prove $\Sigma_1$-completeness of Robinson's arithmetic? That's certainly not necessary (and not usual). You can easily prove it by (meta-)induction on the complexity of the sentence in a syntactic way (except that you need the truth predicate for $\Sigma_1$-sentences, of course, otherwise you cannot even state the theorem). – Emil Jeřábek Apr 24 '23 at 18:22