[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!


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