[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
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.
More information about the FOM
mailing list