Incompleteness theorems via Turing category
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866912160816300032 |
|---|---|
| author | Savelyev, Yasha |
| author_facet | Savelyev, Yasha |
| contents | We give a reframing of Godel's first and second incompleteness theorems that applies even to some undefinable theories of arithmetic. The usual Hilbert-Bernays provability conditions and the diagonal lemma are replaced by a more direct diagonalization argument, from first principles, based in category theory and in a sense analogous to Cantor's original argument. To this end, we categorify the theory Gödel encodings, which might be of independent interest. In our setup, the Gödel sentence is computable explicitly by construction even for $Σ^{0} _{2}$ theories (likely extending to $Σ^{0} _{n}$). In an appendix, we study the relationship of our reframed second incompleteness theorem with arguments of Penrose. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_14084 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Incompleteness theorems via Turing category Savelyev, Yasha Logic Logic in Computer Science We give a reframing of Godel's first and second incompleteness theorems that applies even to some undefinable theories of arithmetic. The usual Hilbert-Bernays provability conditions and the diagonal lemma are replaced by a more direct diagonalization argument, from first principles, based in category theory and in a sense analogous to Cantor's original argument. To this end, we categorify the theory Gödel encodings, which might be of independent interest. In our setup, the Gödel sentence is computable explicitly by construction even for $Σ^{0} _{2}$ theories (likely extending to $Σ^{0} _{n}$). In an appendix, we study the relationship of our reframed second incompleteness theorem with arguments of Penrose. |
| title | Incompleteness theorems via Turing category |
| topic | Logic Logic in Computer Science |
| url | https://arxiv.org/abs/2412.14084 |