Timeline for Does the original 1931 proof of Gödel’s incompleteness rely on the completeness theorem, or is it purely syntactic?
Current License: CC BY-SA 4.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 24, 2023 at 18:22 | comment | added | Emil Jeřábek | 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). | |
| Apr 24, 2023 at 17:29 | comment | added | huurd | @Timothy Chow : yes indeed, P_0 means Robinson arithmetic in Cori-Lascar book. | |
| Apr 24, 2023 at 17:01 | history | edited | Timothy Chow | CC BY-SA 4.0 |
Added snippets from a relevant reference
|
| Apr 23, 2023 at 19:02 | comment | added | Timothy Chow | @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. | |
| Apr 23, 2023 at 18:59 | comment | added | huurd | @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 ? | |
| Apr 23, 2023 at 18:55 | comment | added | Timothy Chow | @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. | |
| Apr 23, 2023 at 18:49 | comment | added | huurd | @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. | |
| Apr 23, 2023 at 18:47 | comment | added | Timothy Chow | @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. | |
| Apr 23, 2023 at 18:38 | comment | added | Timothy Chow | @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*. | |
| Apr 23, 2023 at 15:22 | comment | added | huurd | @Emil Jeřábek : you're right, but this is not what I said. | |
| Apr 23, 2023 at 15:18 | comment | added | Emil Jeřábek | Defining the truth of sentences in a model does not in any way require the completeness theorem. | |
| Apr 23, 2023 at 14:15 | comment | added | huurd | Can you give me an example of a purely syntactic modern proof of Godel's incompleteness theorem ? | |
| Apr 23, 2023 at 13:54 | comment | added | Timothy Chow | @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." | |
| Apr 23, 2023 at 13:48 | comment | added | huurd | Addendum : what meant "true sentence" in mathematical logic of the 30's ? and more specifically for Godel ? | |
| Apr 23, 2023 at 13:34 | comment | added | huurd | 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. | |
| Apr 23, 2023 at 13:28 | comment | added | huurd | 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. | |
| Apr 23, 2023 at 13:18 | history | answered | Timothy Chow | CC BY-SA 4.0 |