[FOM] Reverse Mathematics question
Paul Blain Levy
p.b.levy at cs.bham.ac.uk
Sun Jun 16 15:41:35 EDT 2019
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