[FOM] The origin of second-order arithmetic

[sasander at cage.ugent.be]

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.