[FOM] Reverse Mathematics question
Paul Blain Levy
p.b.levy at cs.bham.ac.uk
Sun Jun 16 16:00:34 EDT 2019
On second thoughts I expect the answer to (ii) to be No, i.e. that
recursion is more powerful than induction. But I'm still interested to
hear the answer!
Paul
On 16/06/2019 20:41, Paul Blain Levy wrote:
> Hi,
>
> For a relation R on a set A, write W^R(x) to say that x is an
> R-well-founded element of A. The "Generation" principle says that if
> all y in A such that R(y,x) are R-well-founded then so is x. The
> "Induction" principle says that, for any predicate psi on A that is
> R-inductive (i.e. for every x in A, if all y in A such that R(y,x)
> satisfy psi then x does too) is true of every R-well-founded element.
>
> Let "W-arithmetic" be Peano arithmetic extended with the syntax
> W^{x,y.phi}(a), where phi can itself use W, together with axiom
> schemes for Generation and Induction.
>
> My questions:
>
> (i) Has this system (or something trivially equivalent to it) been
> studied?
>
> (ii) Is the ATR_0 subsystem of second-order arithmetic a conservative
> extension of W-arithmetic, just as the ACA_0 subsystem is a
> conservative extension of Peano arithmetic?
>
> [I expect that the answer to both questions is yes.]
>
> Paul
>
>
>
More information about the FOM
mailing list