[FOM] Reverse Mathematics question

Paul Blain Levy p.b.levy at cs.bham.ac.uk
Sun Jun 16 15:41:35 EDT 2019


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.]


More information about the FOM mailing list