[FOM] The origin of second-order arithmetic
sasander at cage.ugent.be
sasander at cage.ugent.be
Wed Dec 6 03:54:50 EST 2017
Dear Richard,
> it's the type of the variables that we quantify over that determines
> the >"order" of the system.
In light of the previous, I would say this definition is/becomes/has
become meaningless:
System H allows one to introduce all sorts of functionals like
Feferman?s mu and the Suslin functional.
The latter are the counterparts of ACA_0 and Pi11-CA_0 in Kohlenbach
higher-order reverse mathematics. Now, many equivalences in the
latter can be formulated in H, esp. because one can often
effectively convert one functional to the other (via a term from
Goedel?s T). Also, one rarely needs
type 3 (fourth-order) objects anyway.
Hence, one can directly simulate large parts of higher-order reverse
math in H and its subsystems, but because
one happens to not quantify over functionals, the system H is ?second-order?.
So can we at least agree
that ?morally? system H should be considered as ?beyond second-order
arithmetic? (and we will leave it
to our own imagination if it is third-order or not), due to its
ability to directly simulate higher-order reverse math?
Note that Feferman?s mu etc cannot be directly represented in SOA
(like many discontinuous objects).
Best,
Sam
----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.
More information about the FOM
mailing list