[FOM] The origin of second-order arithmetic

[Richard Zach]

Hi,

\xi is an expression with free function variables, not a third order 
order object (that you can quantify over). 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).

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. 
Although, one reason one might not want to count H&B II as "the" source 
for SOA is that they really only vaguely sketch how to do SOA *with set 
& relation variables* in that very last section.

Note that the formalism H (arithmetic with function variables and 
\epsilon) goes back to Ackermann's 1924 dissertation.

-Richard


On 2017-12-03 04:28 AM, sasander at cage.ugent.be wrote:
> I had a historical question regarding second-order arithmetic (SOA for 
> short).
>
>
> First some background: The oft-repeated origin of SOA is as follows:
>
> The formalization of mathematics within second order arithmetic was 
> developed by Hilbert and Bernays
> in Supplement IV of the Grundlagen der Mathematik.
>
> Below, I am referring to the 1970 version of Volume 2 of the 
> Grundlagen, with Maths Reviews number MR0272596.
> This version is said to be freely available as a PDF on the internet 
> (I was told).
>
>
> Secondly, the above widespread claim is plainly false for the 
> following reasons:
>
> The aforementioned Supplement IV contains three formal systems H, K, 
> and L,
> none of which constitutes SOA by any stretch of the imagination, because
>
> The system H makes explicit used of third-order objects (i.e. type two 
> functionals).
> Seeing is believing: the functional \xi on page 495 takes as input a 
> function (type
> one object) and outputs a function (type one object).  Note that 
> function variables
> are denoted by "dotted" variables and that the epsilon operator is used.
>
> The system K is a variation of H in which the definition of \xi can be 
> done via similar
> means, namely the "iota" operator combined with lambda abstraction 
> (See p. 502).
>
> The system L does not allow one to express basic theorems about the 
> reals via formulas,
> but only via formula schemas (See p. 512).
>
> I hope you agree that in light of these facts, H, K, and L do not even 
> come close to being SOA.
>
>
>
> Thirdly, my actual question:  if not Hilbert and Bernays, who was the 
> first to introduce SOA?
>
>
>
> Fourth, more context: it is definitely true that Hilbert's lectures on 
> the foundations of
> math over time evolved into "less and less use of third-order 
> objects", culminating in the
> Grundlagen were there is not so much use of third-objects anymore, 
> compared to earlier works.
>
>
>
> Best,
>
>
> Sam Sanders
>
>
> PS: The following paper about the "prehistory" of SOA does *not* 
> provide an answer to my question,
> nor do the authors make the above observations:
>
> https://arxiv.org/abs/1612.06219
>
>
> ----------------------------------------------------------------
> This message was sent using IMP, the Internet Messaging Program.
>