BusyBeaver(6) Is Quite Large

It boggles my mind that a number (an uncomputable number, granted) like BB(748) can be "independent of ZFC". It feels like a category error or something.

It boggles my mind that we ever thought a small amount of text that fits comfortably on a napkin (the axioms of ZFC) would ever be “good enough” to capture the arithmetic truths or approximate those aspects of physical reality that are primarily relevant to the endeavors of humanity. That the behavior of a six state Turing machine might be unpredictable via a few lines of text does not surprise me in the slightest.

As soon as Gödel published his first incompleteness theorem, I would have thought the entire field of mathematics would have gone full throttle on trying to find more axioms. Instead, over the almost century since then, Gödel’s work has been treated more as an odd fact largely confined to niche foundational studies rather than any sort of mainstream program (I’m aware of Feferman, Friedman, etc., but my point is there is significantly less research in this area compared to most other topics in mathematics).

Within ZFC one can prove that any two models of second order PA are isomorphic. ZFC proves that PA is consistent. ZFC is good enough to capture arithmetical truth.

Unfortunately no, ZFC isn't good enough to capture arithmetical truth. The problem is that there are nonstandard models of ZFC where every single model of second-order PA within is itself nonstandard. There are even models of ZFC where a certain specific computer program, known as the "universal algorithm" [1], solves the halting problem for all standard Turing machines.

https://jdh.hamkins.org/the-universal-algorithm-a-new-simple...

ZFC allows models of second order PA and proves that those models are all isomorphic. Within each model of ZFC there is no such thing as a nonstandard model of second order PA. One can only think it is nonstandard by looking from outside the model, no? What theorem of second order PA is ZFC unable to prove?

This is similar to how there are countable models of ZFC but those models think of themselves as uncountable. They are countable externally and not internally.