9
$\begingroup$

I'm quite sure I don't understand very well the links between proof theoretical ordinals of theories, the axioms of transfinite induction and the objects a theory can prove to exist.

For instance I'm considering Peano Axioms ($\mathbf{PA}$), of proof theoretic ordinal $\epsilon_0$, Primitive Recursive Arithmetic ($\mathbf{PRA}$) of proof theoretic ordinal $\omega^\omega$ and Elementary Recursive Arithmetic ($\mathbf{ERA}$), which is a fragment of $\mathbf{PRA}$.

I was wondering if $\mathbf{PRA}+TI\{\alpha\in\epsilon_0\}$ (where $TI$ stands for transfinite induction) was equivalent in some sense to $\mathbf{PA}+TI\{\alpha\in\epsilon_0\}$ or/and to $\mathbf{ERA}+TI\{\alpha\in\epsilon_0\}$ ?

And more generally, if it was true that for any set $A$ of (countable) ordinals such that $\epsilon_0 \subset A$, $\mathbf{ERA}+TI\{\alpha\in A\} = \mathbf{PRA}+TI\{\alpha\in A\} = \mathbf{PA}+TI\{\alpha\in A\}$ ?

Any enlightenment would be most welcome :) Thanks in advance.

Improve this question
$\endgroup$
1
  • $\begingroup$ Sorry for the bad TI notation, it was 1st order transfinite induction up to $epsilon_0$. Thanks for your answer, all is now much clearer to mo. $\endgroup$
    – Primitive Recursive Fab
    Commented Mar 6, 2013 at 13:58

1 Answer 1

Reset to default
9
$\begingroup$

This entirely depends on what exactly you mean by $TI$, as there are several options (I actually do not understand what the $\{\alpha\in\epsilon_0\}$ part of the notation is supposed to mean either, but I will assume it just means transfinite induction up to $\epsilon_0$):

  1. $TI\{\alpha\in\epsilon_0\}$ is the schema $$\forall x\,(\forall y\prec x\,\phi(y)\to\phi(x))\to\forall x\,\phi(x),$$ where $\phi$ is an arbitrary formula, and $\prec$ the standard ordering of type $\epsilon_0$. It is easy to see that transfinite induction implies ordinary induction over a weak base theory (say, $I\Delta_0$), hence in this case, $I\Delta_0+TI\{\alpha\in\epsilon_0\}=\mathrm{PA}+TI\{\alpha\in\epsilon_0\}$ (and the same holds for any base theory in between).

  2. $TI\{\alpha\in\epsilon_0\}$ is the same schema restricted to formulas of bounded complexity $\Gamma$. Typically used choices for $\Gamma$ include $\Pi^0_2$, $\Pi^0_1$, or open formulas in the language of PRA or EA (also called ERA or EFA). In all these cases, $\mathrm{PRA}+TI\{\alpha\in\epsilon_0\}$ is strictly weaker than $\mathrm{PA}+TI\{\alpha\in\epsilon_0\}$, since the former theory can be axiomatized by formulas of bounded complexity, and no consistent set of formulas of bounded complexity can imply full ordinary induction (which is equivalent to the full uniform reflection schema). In the case where $\Gamma$ are open EA-formulas, $\mathrm{EA}+TI\{\alpha\in\epsilon_0\}$ is likewise strictly weaker than $\mathrm{PRA}+TI\{\alpha\in\epsilon_0\}$. On the other hand, if $\Gamma\supseteq\Pi^0_1$, then $TI\{\alpha\in\epsilon_0\}$ implies $I\Sigma_1\supseteq\mathrm{PRA}$ over a weak base theory.

  3. $TI\{\alpha\in\epsilon_0\}$ is the second-order induction axiom $$\forall X\,\forall x\,(\forall y\prec x\,y\in X\to x\in X)\to\forall x\,x\in X.$$ Then one needs to include some comprehension schema in the base theory to make any sense, and its strength determines the strength of the $TI\{\alpha\in\epsilon_0\}$. In particular, if we take at least $\Sigma^0_1$-comprehension, we are in the same situation as in 1. If we take recursive comprehension, it is the same as 2 with $\Gamma=\Delta^0_1$.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Emil: can you recommend some references for the results in #2 in connection with fragments of arithmetic? $\endgroup$
    – Ali Enayat
    Commented Mar 6, 2013 at 19:40
  • 2
    $\begingroup$ @Ali: It seems that I have misremembered the complexities of the restricted transfinite induction schemata used, they seem to be rather lower. As one can find in e.g. Girard’s “Proof theory and logical complexity”, already PRA with the quantifier-free transfinite induction rule up to $\epsilon_0$ proves Con(PA). TI up to $\epsilon_0$ for formulas of restricted complexity proves uniform reflection schemata for PA of restricted complexity. Girard explicitly mentions only the full reflection schema (which needs full TI), but a similar argument gives the restricted versions. ... $\endgroup$
    – Emil Jeřábek
    Commented Mar 11, 2013 at 19:02
  • 2
    $\begingroup$ ... If I get it right this time, $\Sigma^0_1$-reflection (i.e., 1-consistency) is provable over PRA using quantifier-free TI axiom, and more generally $\Sigma^0_{n+1}$-reflection follows from TI up to $\epsilon_0$ for $\Pi^0_n$-formulas. The claim I made above that EA with quantifier-free TI is strictly weaker than the same plus PRA is probably bogus: PRA (or rather the equivalent theory in the language of PA) is a $\Pi^0_2$-axiomatized fragment of PA, hence it is implied by uniform $\Sigma^0_1$-reflection for PA. I’m not sure whether the cut-elimination argument involved in the proof ... $\endgroup$
    – Emil Jeřábek
    Commented Mar 11, 2013 at 19:11
  • 2
    $\begingroup$ ... of $\Sigma^0_1$-reflection by open TI works (or can be worked around) in EA, but it should work over $\mathrm{EA}^+=I\Delta_0+\mathrm{SUPEXP}$. As for other things I mentioned, the fact that PA proves the full uniform reflection for its finite fragments (which implies it is not included in any theory of bounded complexity) can be found in various places, e.g. in Girard again, but a comprehensive source for related results is igitur-archive.library.uu.nl/lg/2008-0326-201008/… . $\endgroup$
    – Emil Jeřábek
    Commented Mar 11, 2013 at 19:17
  • $\begingroup$ Emil: thanks for your detailed explanations (I only now saw them). $\endgroup$
    – Ali Enayat
    Commented Apr 9, 2013 at 3:51

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .