BusyBeaver(6) Is Quite Large

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

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

But why? Gödel's theorem does not depend on number of axioms but on them being recursively enumerable.

Gödel's theorem shows that you need an infinite number of axioms to describe reality (given that available reality isn't finite), so any existing axiomatic system isn't enough.

Well, obviously we could simply take every true sentence of Peano arithmetic as an axiom to obtain a consistent and complete system, but if we think in that spirit, then almost every mathematician in the world is working on finding a better set of axioms (because every proof would either give us new axiom or show that something should not be included as axiom), right?

Right, Hilbert’s goal was (loosely speaking) to “find a finitely describable formal system” sufficient to “capture all truths”. When Gödel showed that can’t be done, that shouldn’t imply we just stop with the best theory we have so far and call it a day—it means there are an infinite number of more powerful theories (with necessarily longer minimal descriptions) waiting to be discovered.

In fact, both Gödel and Turing worked on this problem quite a bit. Gödel thought we might be able to find some sort of “meta-principle” that could guide us toward discovering an ever increasing hierarchy of more powerful axioms, and Turing’s work on ordinal progressions followed exactly this line of thinking as well. Feferman’s completeness theorem even showed that all arithmetical truths could be discovered via an infinite process. (Now of course this process is not finitely axiomatizable, but one can certainly extract some useful finite axioms out of it — the strength of PA after all is equivalent to the recursive iteration up to ε_0 of ‘Q_{n+1} = Q_n + Q_n is consistent’ where Q_0 is Robinson arithmetic).

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.

This ignores the fact that it is not so easy to find natural interesting statements that are independent of ZFC.

Statements that are independent of ZFC are a dime a dozen when doing foundations of mathematics, but they're not so common in many other areas of math. Harvey Friedman has done interesting work on finding "natural" statements that are independent of ZFC, but there's dispute about how natural they are. https://mathoverflow.net/questions/1924/what-are-some-reason...

In fact, it turns out that a huge amount of mathematics does not even require set theory, it is just a habit for mathematicians to work in set theory. https://en.wikipedia.org/wiki/Reverse_mathematics.

> obviously we could simply take every true sentence of Peano arithmetic as an axiom to obtain a consistent and complete system

If you’re talking about every true sentence in the language of PA, then not all such sentences are derivable via the theory of PA. If you are talking about the theorems of PA, then these are missing an infinite number of true statements in the language of PA.

Harvey Friedman’s “grand conjecture” is that virtually every theorem that working mathematicians actually publish can already be proved in Elementary Function Arithmetic (much weaker than PA in fact). So the majority of mathematicians are not pushing the boundaries of the existing foundational theories of mathematics, although there is certainly plenty of activity regardless.

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

Yeah, I’m quite familiar with Friedman’s work. I mentioned him and his Grand Conjecture in another comment.

> This ignores the fact that it is not so easy to find natural interesting statements that are independent of ZFC.

I’m not ignoring this fact—just observing that the sheer difficulty of the task seems to have encouraged mathematicians to pursue other areas of work beside foundational topics, which is a bit unfortunate in my opinion.

I agree most working mathematicians have limited interest in foundational topics. To me, that seems harmless enough.

> approximate those aspects of physical reality that are primarily relevant to the endeavors of humanity.

This is the comment that made me think that you were saying we needed more work on foundations for math as it is used in the sciences, and that doesn't match my understanding. Did I read it differently than you meant it?

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.

The consistency of ZFC is (presumably) a theorem of second order PA, and ZFC is unable to prove it (unless ZFC is inconsistent).

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

ZFC is way overpowered for that. https://mathoverflow.net/questions/39452/status-of-harvey-fr...

I don’t understand your post. You’re linking to a discussion about the same conjecture I mentioned in another comment 11 hours prior to your comment. Did you mean to link something else?

Indeed yes. But in a sense within ZFC one can say what N is given the categorical nature of second order PA. Each model of ZFC will have, up to isomorphism, one model of N.

I didn't notice your other post mentioning the conjecture. Anyway, one thing it might mean is that we humans have a very limited understanding of mathematics.