[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