$Π^0_1$ Proof Ordinals

Question

Natural theories extending EFA (exponential/elementary function arithmetic) are well-ordered by $Π^0_1$ provability, and we would like a formal definition of the well-ordering that is robust yet as fine as possible. Here is the definition I came up with.

Fix an elementary ordinal notation system such that the predecessor partial function (given $α+1$ return $α$) is elementarily definable. Formally, the definition (and the ordinals it gives) depends on the ordinal notation system. However, at least if the ordinal is not too large, natural ordinal notation systems (such as Veblen normal form) are elementarily equivalent, and provably so in EFA, which should suffice.

Set $f_0(n)=2^2_n$, $f_{α+1}(n) = f_α(2^2_n)$ ($2^2_n$ is iterated exponentiation), and for limit α, $f_α(n)=\max(f_β(n): β<α ∧ \mathrm{code}(β)<n)$ ($\mathrm{code}(β)$ is the integer coding $β$).
(Alternatively, if we are given reasonable fundamental sequences, set $f_α(n) = f_{α[n]}(n)$.)

Con$_α$ = ∀n Con$_f$(EFA + $f_α(n)$ exists) where Con$_f$ is cut-free consistency.
Th($α$) = EFA + {Con$_β$: $β<α$}
For a theory $T$ extending EFA,
$|T|_{Π^0_1} = \sup(α+1: T⊢\mathrm{Con}_α)$
$T$ is $Π^0_1$-regular iff $T$ and $\mathrm{Th}(|T|_{Π^0_1})$ prove the same $Π^0_1$ statements.

The intended meaning of Con$_α$ is to iterate the cut-free consistency of EFA $1+α$ times. If I understand correctly, in EFA cut-free consistency is robust but more fine grained than ordinary consistency, and EFA ⊢ Con(EFA) ⇔ Con$_f$(EFA+Con$_f$(EFA)) (and also Con$_f$(EFA)⇔Con(Q)).

Is this definition equivalent to the standard definition of $Π^0_1$ ordinals?

If I understand correctly, the standard definition is
$|T|_{Π^0_1} = \sup(α+1:T ⊢ \mathrm{Con}_f(A(α)))$
where $A$ is an elementary formula with two free variables such that $\mathrm{EFA} ⊢ ∀α \, A(α) = \mathrm{EFA}∪\{\mathrm{Con}_f(A(β)):β<α\}$
$A(α)$ means $\{n:A(α,n)\}$, and statements are coded by their Gödel numbers.

Informally, the standard definition is based on direct iteration of consistency (using fixed-point theorem to get the desired predicate) while the definition I gave is based on consistency of existence of large numbers.

Also, do the following intuitively true identities hold:
|EFA|$_{Π^0_1}$ = 0
|EFA+Con$_f$(EFA)|$_{Π^0_1}$ = 1
|EFA+Con(EFA)|$_{Π^0_1}$ = 2
|PA|$_{Π^0_1}$ = $ε_0$
|EFA+Con(PA)|$_{Π^0_1}$ = $ε_0+1$
|EFA+Con(ACA$_0$)|$_{Π^0_1}$ = $ε_0+2$
|PRA+Con(PA)|$_{Π^0_1}$ = $ε_0+ω^ω$
|PA+Con(PA)|$_{Π^0_1}$ = $ε_0·2$
with each of these theories $Π^0_1$-regular.

Answer 1

Modulo the fact that Beklemishev [1] considers consistency with cuts as the basic consistency notion, his $\mathsf{Con}(\mathsf{EA}_\alpha)$ are equivalent to your's $\mathsf{Con}_{\alpha}$. It is quite easy to account for the effects of the switch between cut-free and full consistency using the result of Visser [2] that for finite extensions $T$ of $\mathsf{EA}$, we have $\mathsf{EA}\vdash \mathsf{Con}(T)\mathrel{\leftrightarrow} \mathsf{Con}_f(\mathsf{EA}+\mathsf{Con}_f(T))$.

Beklemishev fixes an ordinal notation system and using Diagonal Lemma defines $\mathsf{EA}_\alpha$ as a uniformly $\Sigma_1$-axiomatizable family of theories for $\alpha$ from the ordinal notation system such that provably in $\mathsf{EA}$: $$\mathsf{EA}_\alpha=\mathsf{EA}+\{\mathsf{Con}(\mathsf{EA}_\beta)\mid \beta<\alpha\}.$$ Using Löb's theorem it is easy to prove that in fact there is $\mathsf{EA}$-provably unique family of theories $\mathsf{EA}_\alpha$ satisfying the condition above (unique in extensional sense as a family of sets of theorems). To make this definition matching with your's let $$\mathsf{EA}_\alpha'=\mathsf{EA}+\{\mathsf{Con}_f(\mathsf{EA}_\beta')\mid \beta<\alpha\}.$$

Using Löb's theorem (for cut-free $\mathsf{EA}$-provability) it is rather routine to prove that $\mathsf{EA}$-provably for all notation systems $\alpha$ we have $\mathsf{Con}_f(\mathsf{EA}_\alpha')\mathrel{\leftrightarrow}\mathsf{Con}_\alpha$. Reasoning in $\mathsf{EA}$ and using additional assumption that there is a cut-free proof of $\forall \alpha(\mathsf{Con}_f(\mathsf{EA}_\alpha')\mathrel{\leftrightarrow}\mathsf{Con}_\alpha)$ we need to prove the eqivalence between $\mathsf{Con}_f(\mathsf{EA}_\alpha')$ and $\mathsf{Con}_\alpha$. We use the aforementioned cut-free proof to show equivalence between $\mathsf{Con}(\mathsf{EA}_\alpha')$ and $\mathsf{Con}_f(\mathsf{EA}+\{\mathsf{Con}_\beta\mid \beta<\alpha\})$. Now we just need to establish the equivalence $$\mathsf{Con}_f(\mathsf{EA}+\{\mathsf{Con}_\beta\mid \beta<\alpha\})\mathrel{\leftrightarrow}\mathsf{Con}_\alpha.$$ From left to right it is rather straightforward by proving that for $\alpha\ne 0$ the formula to the left implies that for any $n$ we have $\mathsf{Con}_f(\mathsf{EA}+\mathsf{Con}_f(\mathsf{EA}+\text{$f_\alpha(n)$ exists}))$. The idea of a proof of the implication from right to left, is to use purely universal axiomatization of $\mathsf{EA}$ in the language with all Kalmar elementary functions and next to employ Herbrand's theorem to reformulate the consistency assertion to the left.

Now analogously to what Beklemishev have done in his paper, we have $$|\mathsf{EA}'_\alpha|_{\Pi^0_1}=\alpha.$$ and again analogously to what he have done (see Section 7 from [1]), we immediately get most of the ordinals that you mentioned. For the other ordinals we would need a bit of additional work:

1. $|\mathsf{EA}+\mathsf{Con}(\mathsf{EA})|_{\Pi^0_1}=2$: follows immediatelly from the mentioned theorem of [2];
2. $|\mathsf{EA}+\mathsf{Con}(\mathsf{ACA}_0)|_{\Pi^0_1}=\varepsilon_0+2$, since $$\mathsf{EA}+\mathsf{Con}(\mathsf{ACA}_0)=\mathsf{EA}+\mathsf{Con}_f(\mathsf{EA}+\mathsf{Con}_f(\mathsf{ACA}_0))=\mathsf{EA}+\mathsf{Con}_f(\mathsf{EA}+\mathsf{Con}(\mathsf{PA})),$$ where in the last equality we are using $\mathsf{EA}$-formalized conservativity proof of $\mathsf{ACA}_0$ over $\mathsf{PA}$ via the transformation of cut-free $\mathsf{ACA}_0$-proofs to $\mathsf{PA}$-proofs with cuts;
3. $|\mathsf{PRA}+\mathsf{Con}(PA)|_{\Pi^0_1}=\varepsilon_0+\omega^\omega$: it wasn't mentioned by Beklemishev, but easily could be established by the same technique.

P.S. I very much like your equivalent definition of $\Pi^0_1$-ordinal, I didn't knew this precise formulation. Curiously, almost at the same time you asked the question, in the fall of 2017, I was exploring in a somewhat similar direction. Namely, my idea was to measure how much consistency a model of arithmetic could prove in terms of how much longer than the original model could its end-extensions obtained by the formalized completeness theorem be. However, I haven't managed to make a nice formulation out of this.

[1] Beklemishev, Lev D. "Proof-theoretic analysis by iterated reflection." Archive for Mathematical Logic 42.6 (2003).

[2] A. Visser. Interpretability logic. In Mathematical Logic, Proceedings of the 1988 Heyting Conference. Plenum Press, 1990