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.