Timeline for Satisfying systems in Gödel's original proof of completeness
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 7, 2020 at 22:15 | comment | added | Mallik | I just figured out that Godel is using "function" to refer not to functions but to predicates. This becomes clear in the final steps of the proof. I haven't worked through the details yet. | |
| Feb 7, 2020 at 21:41 | history | edited | Mallik | CC BY-SA 4.0 |
added 324 characters in body
|
| Feb 7, 2020 at 21:09 | comment | added | Mallik | @NoahSchweber Avigad explicitly considers only formulas $\forall \exists A$ where $A$ does not contain function symbols. The addition of function symbols is the hang-up I have w.r.t. Godel's proof. | |
| Feb 7, 2020 at 20:21 | comment | added | Noah Schweber | @AndreasBlass To be fair there are clearer write-ups of the same argument (e.g. Avigad). | |
| Feb 7, 2020 at 19:55 | history | edited | Mallik | CC BY-SA 4.0 |
added 119 characters in body
|
| Feb 7, 2020 at 5:50 | history | edited | David Roberts♦ | CC BY-SA 4.0 |
Clean up source
|
| Feb 7, 2020 at 2:11 | comment | added | Mallik | @NoahSchweber I've added the original passage from the1930 version (p. 115 of the work cited). | |
| Feb 7, 2020 at 2:08 | history | edited | Mallik | CC BY-SA 4.0 |
added 319 characters in body
|
| Feb 7, 2020 at 1:49 | comment | added | Andreas Blass | @NoahSchweber I conjecture (but don't guarantee) that a lot of what's unclear here comes directly from Gödel's original paper. His argument was considerably more complicated than the Henkin proof that is now standard. | |
| Feb 6, 2020 at 19:29 | comment | added | Noah Schweber | This is a bit unclear to me. First, your "function variables" and "proposition variables" are what we more commonly refer to as "function symbols" and "relation symbols," correct? Second, I don't follow your definition of satisfying system of level $n$, and in particular the definition of $ns$. Do you have a citation to a text where this language is used? That might be helpful ... | |
| Feb 6, 2020 at 18:44 | history | asked | Mallik | CC BY-SA 4.0 |