[FOM] The origin of second-order arithmetic

[Joe Shipman]

What I’d like to know is what systems were proposed that we would recognize as “Second Order Arithmetic”, which both preceded and were weaker than the full Z2. If so, there would be historical motivation for Reverse Mathematics’ emphasis on subsystems of Z2. 

The Predicative/Impredicative boundary and the controversy over AC are the two examples I can think of where people cared about this, but was either of these issues ever connected to a fully formalized system that we would recognize as a subsystem of Second Order Arithmetic, before the Mostowski 1952 paper?

Here I mean “proposed as reliable foundations for analysis” rather than simply “proposed as an object of study”, where it was noted that particular theorems not known to be provable in the proposed system were actually mathematically doubtful because of reservations about impredicativity, arbitrary choices, etc.

— JS

Sent from my iPhone

> On Dec 5, 2017, at 3:57 PM, sasander at cage.ugent.be wrote:
> 
> Dear Richard,
> 
> Thanks for your answer!
> 
>> Note that the formalism H (arithmetic with function variables and \epsilon) ?>goes back to Ackermann's 1924 dissertation.
> 
> Indeed, that?s what the first sentence of Supplement IV says (p 467 in my reference).  That sentence *also* says the following: that the formalism presented
> in Supplement IV is *up to insignificant differences* the one from Hilbert?s lectures about proof theory and Ackermann?s disseration.  However, both Hilbert?s
> lectures (See the excellent book by Sieg) and Ackermann?s dissertation (See below link) explicitly introduce third-order objects, which they refer to as ?Funktionfunktionen?.
> 
> In light of the above, it is not a stretch of the imagination to think that \xi on p 495 is to be interpreted as a third-order object.
> Moreover, on the second page of Supplement IV, we find the following sentence:
> 
> entsprechend sind als Funktionale die Ausdruecke (\epsilon f )A(f) zugelassen, worin A(f) aus einer Formel A(g), welche die freie Funktionsvariable g,
> dagegen nicht die gebundene Variable f enthaelt, mittels der Ersetzung von g durch f hervorgeht.
> 
> I changed the variables because FOM probably does not like Fraktur (or Umlauts).  This sentence essentially says that functionals may be obtained
> from the epsilon operator as (\epsilon f )A(f), assuming there are no variable clashes for the function variable f.
> 
>> \xi is an expression with free function variables, not a third order order ?>object
> 
> By ?expression", do you mean ?formula?? Note that \xi is not a formula: the dotted equality is equality between functions (See e.g. p 477).
> The ?~? symbol would be used otherwise (See e.g. p. 483).
> 
> I just noted that a functional similar to \xi is introduced at the bottom of p. 479 (without getting a name like \xi).
> 
>> (that you can quantify over).
> 
> Curiously, Hilbert-Bernays indeed do avoid quantifying over third-order objects.
> As I said, there is definitely a tendency towards less third-order stuff over the years, culminating in
> the Grundlagen.  However the latter are not free of third-order stuff, it seems.
> 
>> This doesn't make H third-order for the same reason that the term (x + y) in >first order number theory doesn't make first-order PA a second-order theory, >even though x + y expresses a function from numbers to numbers (a second-order >?object).
> 
> Do you still stand by that analogy?
> 
>> L does allow the expression of theorems about the reals; it's statements about >*sets of* reals that can only be expressed by formula schemas.
> 
> Well, I did say ?basic theorems about the reals?; Hilbert-Bernays name "Satz von der oberen Grenze? (supremum principle) among the thms for which
> formula schemas are needed.  I would call that a basic theorem, but perhaps
> not a good example.
> 
> Best,
> 
> Sam
> 
> 
> PS: Ackermann?s dissertation has been digitised and is freely available here:
> 
> http://gdz.sub.uni-goettingen.de/dms/load/img/?PID=GDZPPN002270129
> 
> ----------------------------------------------------------------
> This message was sent using IMP, the Internet Messaging Program.
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom