Timeline for Proof of second incompleteness theorem for Set theory without Arithmetization of Syntax
Current License: CC BY-SA 4.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 16, 2022 at 20:06 | answer | added | Andrej Bauer | timeline score: 4 | |
| Aug 16, 2022 at 19:45 | comment | added | Joel David Hamkins | It makes sense to me to discuss the first incompleteness theorem without coding syntax, but I don't see how it makes sense to discuss the second incompleteness without an internal account of syntax, since the second incompleteness theorem asserts that the theory T does not prove its own consistency. But to even express the statement of the second incompletness theorem, one must already have an internal account of the theory and an internal account of the notion of proof. | |
| Aug 16, 2022 at 19:06 | answer | added | Charles Loyola | timeline score: 1 | |
| Jul 23, 2020 at 23:59 | comment | added | Andrés E. Caicedo | More interesting is whether you can avoid self-referenciality (no appeals to Gödel's diagonal lemma, for instance). See for instance MR4009518. Visser, Albert, From Tarski to Gödel—or how to derive the second incompleteness theorem from the undefinability of truth without self-reference. J. Logic Comput. 29 (2019), no. 5, 595–604. | |
| S Jul 23, 2020 at 23:35 | history | suggested | CommunityBot | CC BY-SA 4.0 |
Correct subject/verb agreements
|
| Jul 23, 2020 at 22:18 | review | Suggested edits | |||
| S Jul 23, 2020 at 23:35 | |||||
| Jul 23, 2020 at 20:18 | history | edited | Ali | CC BY-SA 4.0 |
edited body
|
| Jul 13, 2020 at 12:55 | comment | added | Mohammad Golshani | See also: fuchino.ddo.jp/notes/woodin-incompl-e.pdf and also andrescaicedo.files.wordpress.com/2010/11/… | |
| Jul 13, 2020 at 9:32 | comment | added | Fedor Pakhomov | For strong enough finite fragment $T$ of $\mathsf{ZFC}$ it would be possible to define a model $M$ of $T$ to be a binary relation $(D^M,\in^M)$ such that we have relativizations of all axioms of $T$ to $(D^M,\in^M)$. So for this kind of theories it would be possible to formulate model-theoretic version of Gödel's 2nd incompleteness theorem without reference to enconding of syntax. However, as far as I know, there are no proofs of G2 that avoid encoding of syntax. But, it is still possible to show this way that $T$ doesn't prove that there is a transitive model of $T$ (using regularity). | |
| Jul 12, 2020 at 20:44 | comment | added | Monroe Eskew | I think the first chapter of Kunen’s Set Theory has a good sketch of the argument. | |
| Jul 12, 2020 at 19:25 | comment | added | Ali | @MonroeEskew : I see... Are there any books or articles covering these arguments or related concerns? | |
| Jul 12, 2020 at 19:06 | comment | added | Monroe Eskew | You can do the argument referring directly to finite sequences of symbols, meaning some natural coding in hereditarily finite sets. So you can avoid prime factorization etc. | |
| Jul 12, 2020 at 18:36 | comment | added | Ali | @MonroeEskew : I don't mean we shouldn't use any coding and prove the incompleteness theorem from scratch, obviously we need at least definition of the numbers in ZF! In my question i ask for a proof with those basic coding needing for defining some notions like model and satisfaction from ZF axioms.By some coding of formula i mean, some extra coding for helping us in the proof like Godel numbering. | |
| Jul 12, 2020 at 18:20 | comment | added | Monroe Eskew | You don’t have to code with natural numbers, but you have to use something. | |
| Jul 12, 2020 at 18:14 | comment | added | Ali | @MonroeEskew : Do we need some coding like Godel numbering to define the notions of model and satisfaction? Aren't those definable via axioms of ZF? | |
| Jul 12, 2020 at 18:00 | comment | added | Monroe Eskew | Won’t some coding of formulas be inevitable? Even if you want it to be model-theoretic, you have to define what is a theory and what it means for a model to satisfy it. | |
| Jul 12, 2020 at 17:48 | history | asked | Ali | CC BY-SA 4.0 |