[FOM] The origin of second-order arithmetic
sasander at cage.ugent.be
sasander at cage.ugent.be
Sun Dec 3 06:28:57 EST 2017
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