[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  
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.


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:


This message was sent using IMP, the Internet Messaging Program.

More information about the FOM mailing list