[FOM] The origin of second-order arithmetic

sasander at cage.ugent.be sasander at cage.ugent.be
Tue Dec 5 15:57:19 EST 2017

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  
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  
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  
formula schemas are needed.  I would call that a basic theorem, but perhaps
not a good example.



PS: Ackermann?s dissertation has been digitised and is freely available here:


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

More information about the FOM mailing list