[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).



This message was sent using IMP, the Internet Messaging Program.

More information about the FOM mailing list