Timeline for Is PA interpretable in PRA + TI(<epsilon_0)?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 6 at 23:13 | comment | added | Stephen Mackereth | Thanks! This is very helpful. | |
| Feb 5 at 13:51 | comment | added | Emil Jeřábek | This is the interpretation existence lemma. It goes back to Wang and Feferman; with PA as a base theory, it is essentially a formalization of the Henkin completeness proof in arithmetic. In order to make it work over $Q$, you use cut shortening in place of induction axioms. I’m not sure what is a good reference for the simple version I quoted; a detailed treatment of a generalized version of the Lemma is in link.springer.com/chapter/10.1007/978-3-319-63334-3_5 . ($Q+\{\mathrm{Con}_{T\restriction n}:n\in\mathbb N\}$ is, essentially, $\mho_{*,\infty}(T)$ in §4.3.) | |
| Feb 2 at 16:28 | comment | added | Stephen Mackereth | Do you have a reference for the second part of your answer: "any r.e. theory $T$ is interpretable in $Q + \{\text{Con}_{T \upharpoonright n} : n \in \mathbb{N}\}$"? | |
| Feb 2 at 0:38 | comment | added | Stephen Mackereth | Thank you for the quick reply! And yes, that is what I meant by TI. | |
| Feb 1 at 20:55 | comment | added | Emil Jeřábek | (I assume you mean by TI the transfinite induction schema for primitive recursive predicates; if you take the schema for all formulas, it trivially contains PA.) | |
| Feb 1 at 20:48 | comment | added | Emil Jeřábek | I can't write a proper answer now, but the answer is yes: PRA + TI($<\epsilon_0$) proves the consistency of each finite fragment of PA, and any r.e. theory $T$ is interpretable in $Q+\{\mathrm{Con}_{T\restriction n}:n\in\mathbb N\}$. | |
| S Feb 1 at 20:09 | review | First questions | |||
| Feb 1 at 20:28 | |||||
| S Feb 1 at 20:09 | history | asked | Stephen Mackereth | CC BY-SA 4.0 |