# [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,

> 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: