10
$\begingroup$

What is the exact (historical) connection between second-order arithmetic and Hilbert-Bernays' Grundlagen der Mathematik?

Some background: the literature on Reverse Mathematics contains a number of claims regarding the connection between second-order arithmetic and Hilbert-Bernays' Grundlagen der Mathematik. Most of these are vague (some might say inaccurate), probably in part due to the fact that the Grundlagen have not been translated to English (in full).

Here is the gap I wish to see filled:

On one hand, Hilbert-Bernays define a logical system H (for Hilbert) in Grundlagen der Mathematik (Supplement IV) and formalise mathematics therein. Other systems are sketched, as well as the associated development, but no real details are given. System H uses the language of second-order arithmetic enriched with third-order parameters, like symbols for Feferman's $\mu^2$ and a version of Kleene's $\exists^3$.

On the other hand, second-order arithmetic $Z_2$ only has first and second-order variables. Someone must have thrown out the third-order parameters for some reason.

This leads to more specific questions:

Who first introduced $Z_2$ and where (and why)? Who first claimed $Z_2$ can be found in the Grundlagen?

Improve this question
$\endgroup$
4
  • 3
    $\begingroup$ The paper "Prehistory of the subsystems of second-order arithmetic" by Dean and Walsh presumably sheds light on your question. The paper was published in the Review of Symbolic Logic (2017), and a draft of it is also available via arxiv.org/abs/1612.06219 $\endgroup$
    – Ali Enayat
    Commented Sep 28, 2020 at 18:22
  • $\begingroup$ @Carl Mummert any idea? $\endgroup$
    – none
    Commented Oct 1, 2020 at 10:10
  • $\begingroup$ @AliEnayat Thanks for the suggestion. One of the shortcomings of that paper (in my personal opinion) is that the authors are trying to be too neutral: they are unwilling to just explicitly say that the Hilbert-Bernays system H involves third-order parameters defined via the epsilon operator. The weaker system K, meant to avoid the latter, still involves Feferman's mu. There is even a discussion about a version of countable choice in H and K, not provable in ZF given the third-order parameters. Finally, the system L can only be used to formalise math indirectly, according to H-B.. $\endgroup$
    – Sam Sanders
    Commented Oct 2, 2020 at 12:35
  • $\begingroup$ My point is that the Hilbert-Bernays approach is definitely third-order. Previous systems (Hilbert-Ackermann) even involved higher types (than type 2/third-order). For whatever reason, even this is not a neutral statement to some, which is why I have asked the above question. $\endgroup$
    – Sam Sanders
    Commented Oct 2, 2020 at 12:42

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .