4
$\begingroup$

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)$.
Improve this question
$\endgroup$
3
  • 7
    $\begingroup$ 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. $\endgroup$
    – Ulrik Buchholtz
    Oct 6, 2016 at 16:47
  • 3
    $\begingroup$ 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$. $\endgroup$
    – Noah Schweber
    Oct 6, 2016 at 23:47
  • $\begingroup$ I guess I need some additional requirement on applicable ordinal notations to make question more reasonable. $\endgroup$
    – Dan
    Oct 7, 2016 at 8:47

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.