[FOM] The origin of second-order arithmetic

[Richard Zach]

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 
object in your sense.
>> 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