18
$\begingroup$

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.

Improve this question
$\endgroup$
10
  • 8
    $\begingroup$ 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. $\endgroup$
    – Gerald Edgar
    Commented Apr 23, 2023 at 8:43
  • 2
    $\begingroup$ 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 ? $\endgroup$
    – huurd
    Commented Apr 23, 2023 at 9:19
  • 3
    $\begingroup$ 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. $\endgroup$
    – Gerald Edgar
    Commented Apr 23, 2023 at 9:28
  • 6
    $\begingroup$ If you get From Frege to Godel, then if you like you can ignore everything but the Gödel chapter. $\endgroup$
    – Gerald Edgar
    Commented Apr 23, 2023 at 9:54
  • 3
    $\begingroup$ The recent booklet "Gödel’s Incompleteness Theorems" by Juliette Kennedy seems to also discuss the details of the original proofs. $\endgroup$
    – Michael Greinecker
    Commented Apr 24, 2023 at 13:02

2 Answers 2

Reset to default
21
$\begingroup$

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.

Improve this answer
$\endgroup$
10
  • 1
    $\begingroup$ 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 ? $\endgroup$
    – huurd
    Commented Apr 23, 2023 at 13:45
  • 3
    $\begingroup$ @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. $\endgroup$
    – godelian
    Commented Apr 23, 2023 at 13:52
  • 1
    $\begingroup$ 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" ? $\endgroup$
    – huurd
    Commented Apr 23, 2023 at 14:24
  • 3
    $\begingroup$ @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. $\endgroup$
    – godelian
    Commented Apr 23, 2023 at 15:17
  • 2
    $\begingroup$ @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. $\endgroup$
    – godelian
    Commented Apr 23, 2023 at 15:34
13
$\begingroup$

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

Improve this answer
$\endgroup$
15
  • 3
    $\begingroup$ @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." $\endgroup$
    – Timothy Chow
    Commented Apr 23, 2023 at 13:54
  • 4
    $\begingroup$ Defining the truth of sentences in a model does not in any way require the completeness theorem. $\endgroup$
    – Emil Jeřábek
    Commented Apr 23, 2023 at 15:18
  • 2
    $\begingroup$ @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. $\endgroup$
    – Timothy Chow
    Commented Apr 23, 2023 at 18:47
  • 6
    $\begingroup$ @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. $\endgroup$
    – Timothy Chow
    Commented Apr 23, 2023 at 19:02
  • 5
    $\begingroup$ 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). $\endgroup$
    – Emil Jeřábek
    Commented Apr 24, 2023 at 18:22

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .