Timeline for Is TA (true arithmetic) interpretable in a recursively axiomatizable theory?
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 6, 2020 at 2:26 | vote | accept | Eric | ||
| Jul 5, 2020 at 15:32 | comment | added | Fedor Pakhomov | @Eric Assume for a contradiction that $\{\varphi\mid \mathsf{TA}\vdash\varphi\}\subsetneq \{\varphi\mid T\vdash \tau(\varphi)\}$. Then there is $\psi$ s.t. $\mathsf{TA}\nvdash \psi$ and $T\vdash \tau(\psi)$. However, since $\mathsf{TA}$ is complete, we would have $\mathsf{TA}\vdash \lnot\psi$. Thus we would have $T\vdash \tau(\lnot \psi)$ and further $T\vdash \lnot \tau(\psi)$ (by preservation of negation). Contradiction, since $T$ was consistent and $T\vdash \tau(\psi)$. | |
| Jul 5, 2020 at 14:23 | comment | added | Eric | @FedorPakhomov I understand coincidence is impossible. But why is inclusion also impossible? Can you explain how "$\tau$ must preserve negation" could imply there's no such $T$? | |
| Jul 5, 2020 at 14:03 | history | edited | Eric | CC BY-SA 4.0 |
edited to address the comments
|
| Jul 5, 2020 at 11:34 | answer | added | Rodrigo Freire | timeline score: 6 | |
| Jul 5, 2020 at 10:09 | comment | added | Fedor Pakhomov | @მამუკაჯიბლაძე Right, I missed it. So we would need to require a bit more from $\tau$. For example, we could only consider $\tau$ that preserve negation, i.e. $T\vdash \lnot \tau(\varphi)\leftrightarrow\tau(\lnot\varphi)$. Then we should have $\{\varphi\mid \mathsf{TA}\vdash\varphi\}=\{\varphi\mid T\vdash \tau(\varphi)\}$. Otherwise due to completeness of $\mathsf{TA}$ there would be $\psi$ such that $T\vdash\tau(\psi)$ and $T\vdash\tau(\lnot\psi)$, which would imply inconsistency of $T$. | |
| Jul 5, 2020 at 9:56 | comment | added | მამუკა ჯიბლაძე | @FedorPakhomov Does not the question ask about inclusion rather than coincidence? Maybe it is trivial to encompass this in your comment, but... | |
| Jul 5, 2020 at 9:39 | comment | added | Fedor Pakhomov | As long as the translation $\tau$ is computable (or even arithmetical) this isn't possible. For any arithmetical $\tau$ and recursively axiomatizable $T$ the set $\{\varphi\mid T\vdash \tau(\varphi)\}$ will be arithmetical and hence couldn't coincide with the set of theorems of $\mathsf{TA}$. | |
| Jul 5, 2020 at 9:00 | review | Close votes | |||
| Jul 11, 2020 at 3:04 | |||||
| Jul 5, 2020 at 8:48 | comment | added | Monroe Eskew | What’s “suitable”? | |
| Jul 5, 2020 at 8:39 | history | asked | Eric | CC BY-SA 4.0 |