6
$\begingroup$

Consider the theory ${\rm PA}^{\mathbb{T}}$ obtained by adding a truth predicate to Peano arithmetic, applicable to sentences of the unaugmented language and satisfying the compositionality axioms $\mathbb{T}(A \wedge B) \leftrightarrow (\mathbb{T}(A) \wedge \mathbb{T}(B))$, $(\forall n)\mathbb{T}(A(n)) \leftrightarrow \mathbb{T}((\forall n)A(n))$, etc., together with the induction scheme for all formulas of the augmented language.

I've read that this theory proves the same arithmetical formulas as ${\rm ACA}$, which I guess implies that it proves induction up to anything less than $\varepsilon_{\varepsilon_0}$ for all arithmetical formulas. So $\varepsilon_{\varepsilon_0}$ is the proof-theoretic ordinal of ${\rm PA}^{\mathbb{T}}$ in this sense.

Suppose we iterate this construction: let ${\rm PA}^{\mathbb{T}^2}$ be obtained by adding a new truth predicate, applicable to sentences of ${\rm PA}^{\mathbb{T}}$, with compositionality axioms and the induction scheme for all formulas of the newly augmented language.

What is its proof-theoretic ordinal (in the sense of: proving induction up to what for all arithmetical formulas)? What if we iterate the construction finitely many times?

Improve this question
$\endgroup$
7
  • $\begingroup$ Quick answer since I'm heading to a meeting, I'll be back to expand later if I remember. All of these theories are interpretable in $L_{\varepsilon_{\varepsilon_0}}$ so their proof-theoretic ordinal can't be larger than that. $\endgroup$
    – François G. Dorais
    Commented Sep 8, 2021 at 17:27
  • $\begingroup$ @FrançoisG.Dorais What's $L_{\epsilon_{\epsilon_0}}$ here? (My only guess, the $L$-hierarchy, doesn't seem to make sense unless I'm missing something.) $\endgroup$
    – Noah Schweber
    Commented Sep 8, 2021 at 17:33
  • $\begingroup$ Constructible universe. $\endgroup$
    – François G. Dorais
    Commented Sep 8, 2021 at 17:34
  • $\begingroup$ @FrançoisG.Dorais But we already get to $\varepsilon_{\varepsilon_0}$ at the first stage, don't we? So it would have to grow from there. $\endgroup$
    – Nik Weaver
    Commented Sep 8, 2021 at 19:21
  • 1
    $\begingroup$ Of course, the rule of thumb doesn't literally apply here but I will get back to that when I have a chance... (Maybe later today but perhaps only next week... sorry about that!) $\endgroup$
    – François G. Dorais
    Commented Sep 11, 2021 at 20:56

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .