[FOM] The origin of second-order arithmetic
Richard Zach
rzach at ucalgary.ca
Tue Dec 5 13:33:40 EST 2017
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.
>
More information about the FOM
mailing list