6
$\begingroup$

By Gentzen's consistency proof, we know that PA has the same consistency strength as PRA + TI(<epsilon_0). Question: is PA interpretable in PRA + TI(<epsilon_0)?

For simplicity, let us assume that PRA + TI(<epsilon_0) is formulated as a first-order theory in the language of arithmetic. Then my question is: does there exist a syntactic translation that carries theorems of PA to theorems of PRA + TI(<epsilon_0) by giving definitions of the universe, functions, and relations?

Improve this question
$\endgroup$
6
  • 4
    $\begingroup$ 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\}$. $\endgroup$
    – Emil Jeřábek
    Commented Feb 1 at 20:48
  • $\begingroup$ (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.) $\endgroup$
    – Emil Jeřábek
    Commented Feb 1 at 20:55
  • $\begingroup$ Thank you for the quick reply! And yes, that is what I meant by TI. $\endgroup$
    – Stephen Mackereth
    Commented Feb 2 at 0:38
  • 1
    $\begingroup$ 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}\}$"? $\endgroup$
    – Stephen Mackereth
    Commented Feb 2 at 16:28
  • 1
    $\begingroup$ 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.) $\endgroup$
    – Emil Jeřábek
    Commented Feb 5 at 13:51

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .