# Canonical formal theory corresponding to a given ordinal

There is a notion of "proof theoretic ordinal" for a formal theory https://en.wikipedia.org/wiki/Ordinal_analysis

Can we go backwards?

That is, we are given some recursive ordinal notation (we don't know if it's indeed ordinal notation). Is there some canonical way to construct formal theory corresponding to this ordinal?

I realize that probably not every ordinal is a strength of some theory (like $w$+1). So, strictly speaking, I am asking about computable function $F$ from ordinals to formal theories such that

1. If $O$ is indeed ordinal notation then $F(O)$ is consistent theory.
2. Strength of $F(O)$ is at least $O$.
3. If $O_1$ < $O_2$ then $F(O_2)$ is extension of $F(O_1)$, i.e. set of provable formulas in $F(O_1)$ is contained in the set of provable formulas in $F(O_2)$.
• Sure: take something like F(O) = PRA + PR-TI(O), where PR-TI(O) expresses transfinite induction along O for primitive recursive predicates. There are of course many variations, according to which predicates you assert transfinite induction for, and which base theory you use. Oct 6, 2016 at 16:47
• Note that this construction is highly notation-dependent: e.g. any true $\Pi^0_1$ sentence will follow from $F(O)$ for some notation $O$ for (I believe) $\omega+1$. Oct 6, 2016 at 23:47
• I guess I need some additional requirement on applicable ordinal notations to make question more reasonable.
– Dan
Oct 7, 2016 at 8:47