Timeline for Connection between second-order arithmetic and Hilbert-Bernays' Grundlagen
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 2, 2020 at 12:42 | comment | added | Sam Sanders | 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. | |
| Oct 2, 2020 at 12:35 | comment | added | Sam Sanders | @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.. | |
| Oct 1, 2020 at 10:10 | comment | added | none | @Carl Mummert any idea? | |
| Sep 28, 2020 at 18:22 | comment | added | Ali Enayat | 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 | |
| Sep 27, 2020 at 20:57 | history | asked | Sam Sanders | CC BY-SA 4.0 |