# [FOM] The origin of second-order arithmetic

Richard Zach rzach at ucalgary.ca
Tue Dec 5 19:55:26 EST 2017

Hi,
> 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.
>> 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?
Yes. The existence of terms of the form \epsilon f A(f) in K does not
make the system 3rd order, just as the existence of formulas with free
set variables (a formula expressing a third order object, a set of sets)
does not make SOA 3rd order, and the existence of first-order terms with
free variables (a term expressing a function) does not make first-order
PA a second-order theory. I system with variables of order n always
allow the formulation of expressions which express objects of type n+1;
but it's the type of the variables that we quantify over that determines
the "order" of the system.

In other words, if K doesn't count as a formalization of second-order
arithmetic, neither does SOA, for \exists x Y(x) is also a third-order
>> 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.
I was responding to this:
> The system L does not allow one to express basic theorems about the
> reals via formulas,
> but only via formula schemas (See p. 512).
which I read as you saying that Bernays said that L cannot express
theorems about the reals as single formulas. It can. It cannot express
theorems about sets of reals as single formulas.

Hope that helps.

-Richard