The 8000th Busy Beaver number eludes ZF set theory (2016) | Hacker News Reader

The 8000th Busy Beaver number eludes ZF set theory (2016)

scottaaronson.blog

114 pointsjkubicek97 comments

These theses are technically very complicated, but what they do is actually easy to explain: they construct a short "program" that basically enumerates all possible statements and checks their validity. And then terminates if it detects a contradiction.

A program that checks the axioms of Peano arithmetic, or of ZF set theory is undecidable, we know that from Gödel's incompleteness theorems.

So then it becomes a sort of competition: who can write the shortest Turing machine that encodes that program. Kinda like a demo-scene for mathematicians.

But let's note that "undecidable" has a specific meaning here, that batches of logic axioms can't prove their own consistency. There's still a possibility of using more powerful logic to prove that one of those will never cause a contradiction.

In particular, ZF can't prove itself, but it can prove that Peano is consistent.

These are very interesting machines, but mostly for reasons that go beyond the normal meaning of the word "undecidable". We have lots of unsolved math problems that can be encoded into vastly shorter turing machines.

> But let's note that "undecidable" has a specific meaning here, that batches of logic axioms can't prove their own consistency

It's not actually that specific. There are many statements that we know are unprovable in ZF. ZFs own consistency is just one of them. The original work to find the 8000 state TM independent of ZF encodes an entirely different statement about graphs.

We are talking about finding TMs which encode a statement which is unprovable in say ZF. Specifically, the TM loops forever iff the statement (which is unprovable in ZF) is true. Not necessarily looking for inconsistencies Godel-style

That's an interesting elaboration. It's also true that we can go beyond undecidability with an oracle, but that introduces a new "undecidable" barrier. Is there a relation between the tower of more powerful logics and the tower of more powerful oracles?

AFAIK yes. see the Large Cardinal Axioms (and combinatorial statements!)

""" The proposition that such cardinals exist cannot be proved in the most common axiomatization of set theory, namely ZFC, and such propositions can be viewed as ways of measuring how "much", beyond ZFC, one needs to assume to be able to prove certain desired results. In other words, they can be seen, in Dana Scott's phrase, as quantifying the fact "that if you want more you have to assume more" """

https://en.wikipedia.org/wiki/Large_cardinal

And https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof for a similar theme with Peano arithmetic and the epsilon_nought ordinal.

> In particular, ZF can't prove itself, but it can prove that Peano is consistent.

Consistent within Peano, or consistent within ZF? That is to say, could another large system of axioms exist which fully contains the Peano axioms, but in which the Peano axioms are inconsistent (in a non-trivial manner)?

I really don't know much about formal logical consistency, but am mildly curious as I see these sorts of claims mentioned.

Consistent means that it doesn't contradict itself. Peano is consistent within Peano. The system that checks if Peano is consistent doesn't have to be similar at all or share any axioms.

The technical answer to your question is yes, another axiomatic system can exist that is able to prove that Peano is inconsistent.

However, assuming that ZF is consistent, then that other axiomatic system would have to be inconsistent.

I recently learned that the physical world is also undecidable. For example, the spectral gap problem in quantum mechanics is one such problem. Scientists have proven that no matter how perfectly and completely we can mathematically describe a material on the microscopic level, we're never going to be able to predict its macroscopic behavior.

This has profound implications, such as for the possibility of a theory of everything. This does not necessarily mean that a theory of everything is impossible, but it does indicate that such a theory might not be able to provide a complete description or prediction of all physical phenomena, which is contrary to the belief of some physicists.

There is of course a catch, since physics can be simulated (with an exponential slowdown) by a Turing machine.

The catch is that "macroscopic behavior" in this context includes things that are not really macroscopically observable, or require conditions that cannot easily be specified. For the spectral gap, I think the way this manifests is that you can't ever be certain that you're in the ground state, but I'm not sure this is correct.

> since physics can be simulated

I must object. Our current models of physics can be simulated. But we cannot model what we do not understand, such as quantum gravity. And even then, we don't even have that many decimal places for certain bits of our models.

By definition the universe can “simulate” itself. Although it’s true we have no proof that this doesn’t go beyond Turing machine in power (yet it’s a reasonable assumption).

Of course the goal of physics is to compress the universe into simpler laws. But there’s no inherent reason that it should be possible.

> By definition the universe can “simulate” itself.

A 1:1 scale map is still just a map. Simulation isn't an identity operation.

> yet it’s a reasonable assumption

What are the reasons for this claim?

>Scientists have proven that no matter how perfectly and completely we can mathematically describe a material on the microscopic level, we're never going to be able to predict its macroscopic behavior

Surely this has more nuance, as it is some ways we can falsify the statement as is

Yes there absolutely is nuance. The mathematics used to determine whether a quantum system has a gap or not is indeed undecidable, but that undecidability only kicks in as the size of your system approaches infinity.

For any finitely sized system, basically any actual system in the universe, the solution is computable/decidable.

People might like this lecture by High Woodin. The message/gist I got from lecture is that infinity is needed to support the finite.

https://youtu.be/1STrev8KcoM

This is the correct video : https://www.youtube.com/watch?v=_FOnZv-R94E (The way I recognize this video is when Hugh Woodin says "Don't worry, I am not going crazy")

This is a great summary. BB is thought provoking because it shows that a simple computation completely destroys any possible conception of mathematics. Probably not very useful but still very interesting.

> completely destroys any possible conception of mathematics

Hyperbolic, to put it gently. It changes our conception of mathematics to a different conception.

But programming is math[1], so is the conclusion that math will eat itself?

[1]: as many argue in the software patent cases

Math is mostly about proofs, and many behaviors of computation are simply not provable, but are still useful. Of course it's possible to use models, formal systems, simulation, formulas, and other tools of mathematics, but arguably there's a clear symmetry breaking. (But it's not really surprising, as most numbers are unnameable and uncomputable. So many things in math are like Turing machines, just they are not that useful.)

FTA this is an interesting tidbit about Busy Beavers:

  But the BB function has a second amazing property: namely, it’s a perfectly well-defined integer function, and yet once you fix the axioms of mathematics, only finitely many values of the function can ever be proved, even in principle.  To see why, consider again a Turing machine M that halts if and only if there’s a contradiction in ZF set theory.  Clearly such a machine could be built, with some finite number of states k.  But then ZF set theory can’t possibly determine the value of BB(k) (or BB(k+1), BB(k+2), etc.), unless ZF is inconsistent!  For to do so, ZF would need to prove that M ran forever, and therefore prove its own consistency, and therefore be inconsistent by Gödel’s Theorem.

> consider again a Turing machine M that halts if and only if there’s a contradiction in ZF set theory. Clearly such a machine could be built, with some finite number of states k.

I am a small brain here. How is this so clear?

I wouldn’t defend the idea that it’s “clear”, but the idea is to build a machine that combines the axioms of ZF set theory in all possible ways to generate all possible conclusions, checking each one for contradiction as it goes. If it never generates a contradictory conclusion from those axioms, it’ll run forever.

This sounds like it relies on the halting problem, or maybe the other way around? Really interesting stuff, been a while since I read about a higher level math topic and been able to sorta kinda understand the "quanta-level" summaries out there

The Nth Busy Beaver number lets you solve the halting problem for Turing Machines up to size N.

Only a handful of them are known, for very small N, and they increase incredibly rapidly. For the most common version of the problem (S for 2-symbol machines), they go: 1, 6, 21, 107, some number greater than or equal to 47176870, and some number greater than 10⇈15 (that's up arrow notation on the last one).

Ooh, are they basically the number of possible turing programs encodable in a state of N?

It's the maximum amount of time a Turing machine of size N can run. So if you want to know whether a Turning machine of size N or less will halt, just run it for BB(N) steps. If it hasn't halted by then, it never will.

I think the part that eludes me here is that it's not clear that such a Turing machine could be built from a finite number of states.

Checking whether a string of bits encodes a proof of False in ZF is decidable. Now enumerate the bitstrings and check each.

> and check each.

"Now, draw the rest of the owl." Not saying you're wrong, just, this jump is super non-obvious even to most mathematicians.

If you can check any given bitstring for whether it encodes a valid ZFC proof of the (in)consistency of ZFC in finite time, then you can write a program to enumerate over all possible bit strings in shortlex order and halt the first time you see a valid proof.

There are infinite many such strings, so that alone can't be used to prove the Turing machine of k states can check all strings. So that leaves open the original question, how do we know that a Turing machine of k states is able to have one of the stated outcomes for any possible bit string?

> There are infinite many such strings

And they can be enumerated by a finite program. For example, in lazily evaluated pseudocode:

    bits = ["0", "1"]
    bitstrings = bits + [(bit + suffix for bit in bits) for suffix in bitstrings]

Because it says 'clearly'. (but yeah, agree with you)

Previously discussed at https://news.ycombinator.com/item?id=36658506

Quoting from https://scottaaronson.blog/?p=7388 :

> Johannes Riebel, an undergraduate at the University of Augsburg in Germany, has produced a tour-de-force bachelor’s thesis that contains, among other things, the first careful writeup of Stefan O’Rear’s result from six years ago that the value of BB(748) is independent of the ZFC axioms of set theory. Regular readers might recall that O’Rear’s result substantially improved over the initial result by me and Adam Yedidia, which showed the value of BB(8000) independent of ZFC assuming the consistency of a stronger system. Along the way, Riebel even gets a tiny improvement, showing that BB(745) independent of ZFC.

BB(748) - BB(745) is probably the largest value that anyone has ever described as "tiny" :-)

It's actually really hard to come up with an interesting lower bound that value.

IIRC no one has proven that BB(n) + 1 < BB(n + 1) for large 2

Take the machine for BB(n) with non-end states {1,2,3,…n} and end state E.

In its program, change every transition that goes to state E to go to a new state n+1 instead.

Add transitions “when in state n+1 and on a 1, move right” and “when in state n+1 and on a 0, write a 1 and stop”.

Doesn’t that give you a Turing machine with n+1 states that stops after writing one more 1 than BB(n) writes, thus proving that BB(n+1) is at least one more than BB(n+1)?

yeah, that shows BB(n+1) >= BB(n) + 1, but if you want to make the inequality strict you need to find a way to add another step.

Oops. Reversing your “BB(n) + 1 < BB(n + 1)” turned out to be too difficult for me today. Thanks for the reply.

Hm, is there some way to “concatenate” Turing machines which would let you prove something like

BB(n) + BB(m) <= BB(n+m+c)

for some fixed c independent of n and m?

It seems very unlikely: the full joint state space has n*m states, so you're throwing away almost everything for large n and m.

You can, but BB(1) = 1 so that doesn't help with BB(n + 1) > BB(n) + 1

It's hard to comprehend just how big that number is. It may indeed be among the largest numbers ever conceived, and we'd have no clue. I wouldn't be surprised if it is larger the number of possible permutations of all particles in the observable universe, for instance. I'd be more surprised if it was less than that.

A commonly quoted number for the number of particles in the observable universe is 10^80 give or take a few orders of magnitude an they have very roughly 10^10^10^2 permutations if you consider all particles distinguishable. The best known lower bound for BB(6, 2) seems to be 10^10^10^10^10^10^10^10^10^10^10^10^10^10^10 which is more like the number of permutations of permutations of permutations of permutations of permutations of permutations of permutations of permutations of permutations of permutations of permutations of permutations of the particles in the universe. Trying to comprehend or compare the size of BB(745) is just futile. Here [1] is a well known attempt to convey the size of 52!, the number of permutations of a deck of cards.

[1] https://www.youtube.com/watch?v=ObiqJzfyACM&t=947s

Right, but we are talking about the difference between two busy beavers here.

Sure, but BB(n) - BB(n - 1) ≈ BB(n) because the function grows so quickly that BB(n - 1) is essentially zero compared to BB(n). Even for factorials the difference between n! and (n - 1)! is essentially n! [1] and the busy beaver function grows much faster.

BB(748) and BB(748) - BB(745) will have the same number of digits and if you compare them left to right, they will agree for way more digits than there are permutations of particles in the observable way before you find the first difference.

[1] (1 - 1/n) n! to be precise.

I agree intuitively, but do you have a formal proof of such? This thread seems to struggle to find one: https://news.ycombinator.com/item?id=38121507

First a correction, I got the lower bound for BB(6, 2) wrong, what I quoted is the runtime, the number of ones is only 10^18267 which is tiny compared to the number of permutations of the particles in the observable universe.

I think proofing a good estimate of the difference will be hard to impossible. We have lower bounds but by definition we can not have a computable upper bound, at least not for arbitrary n. But we need both because we would have to find the difference between the lower bound for BB(748) and the upper bound for BB(745) in order to get an lower bound on the difference between the two.

So yes, in principle the difference BB(748) - BB(745) could be small, but given that the difference BB(n) - BB(n - 1) itself grows faster than any computable function [1] that would be quite surprising. Which is of course a terrible argument.

For BB(748) we have three additional states that we can use to modify the machine for BB(745). And it does not seem completely implausible that we could kind of stretch one state transition, instead of going from state A to state B writing one 1 we go through one of the additional states in between and write another one, writing twice as many 1s as before.

But finding a general construction that provably works for all relevant Turing machines is probably at least not trivial and might as well be impossible. But if one could show this, then we would get something like BB(748) >= 2 * BB(745) and therefore BB(748) - BB(745) >= BB(745). And this we could then combine with a lower bound for BB(745).

[1] If it would not, we could have a computable upper bound for the differences BB(n) - BB(n - 1) which we could turn into a computable upper bound for BB(n) by just summing the bound for the differences up to n.

Just because the difference between values is not computable does not mean that it grows faster than any computable function. The sequence iBB(n) = -1/BB(n) also has incomputable deltas, but it grows more slowly than any increasing computable function.

That’s not to say the entries aren’t large, I agree that they almost certainly are, but rather that the derivative is interesting in it’s own right, and making interesting statements about it is more difficult yet fun than guessing.

We know that asymptotically BB(n) > f(n) for every computable function f. Assume there is a computable upper bound d for the difference so that BB(n) - BB(n - 1) <= d(n). But now note that this gives you BB(n) <= d(1) + d(2) + ... + d(n) and that the right hand side is computable by assumption but that this contradicts the fact that there is no computable upper bound for BB(n). Therefore our assumption was incorrect, there is no computable upper bound for the differences, hence the differences themselves grow faster than any computable function.

The assumption was indeed incorrect, but it was that there exists a computable upper bound d(n) for all n.

My claim is that there may be a computable upper bound for some n. For instance it might be that particular d(n) values represent local maxima wherein a particular "mode" of computation is "unlocked" that uncomputably increases BB(n), leaving BB(n+ε) only computably greater for small natural numbers ε.

Sure, that could potentially be the case. But as said before, I would argue that it does not seem unreasonable to me that you generally can increase BB(n) to twice BB(n) with one or a few additional states by slightly tweaking the machine. And that would be enough to get BB(n) - BB(n - 1) >= BB(n) which together with the size of BB(n) prevents really small differences. But I of course see that proving that you can increase the length of the output of any busy beaver by some constant using some number of additional states is far from trivial.

That must of course be BB(n) - BB(n - 1) >= BB(n - 1). Also I have to retract the correction from a few comments ago, the currently best lower bound for BB(6, 2) is indeed 10 ⇈ 15, I looked at an outdated source when writing the correction.

Graham's number used to be the largest number ever used in a proof, but BB(745) is much larger—Graham's number has been proven to be smaller than BB(16)[1] (although I don't know how carefully the proof has been checked).

[1] https://www.sligocki.com/2022/07/11/bb-16-graham.html

A number much larger than Graham's can be represented in less than 64 bits [1], using a functional flavored Busy Beaver function [2].

[1] https://googology.fandom.com/wiki/User_blog:JohnTromp/The_la...

[2] https://oeis.org/A333479

If BB(745) is independent of ZFC can it even be called a value? It seems like you could easily run into paradoxes if you treated it like just any other value.

just because it's not provably constructable from axioms it doesn't mean it's not just a finite number. that's the really mindbreaking part in this. it's really just like 5. except 5 is provably constructable, describable, nameable. (most numbers are not, just as - for example - angle trisection is impossible with just a straightedge and a compass )

https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na...

http://uu.diva-portal.org/smash/get/diva2:1715729/FULLTEXT01...

There is no paradox and yes, BB(745) is a specific integer, so it's nothing more than a sequence of finite digits.

The fact BB(745) can't be constructed using ZFC only means that there is at least one Turing machine among the set of all 745 state Turing machines that runs forever, but can't be proven to run forever using the axioms of ZFC. You'd need a more powerful axiomatic system to prove that this Turing machine actually runs forever.

This does not imply any kind of paradox or any kind of issue whatsoever in fact. It just means that ZFC is not powerful enough to prove that certain 745 state Turing Machines run forever.

> The fact BB(745) can't be constructed using ZFC only means that [...]

...so what?

The claim wasn't that BB(745) can't be constructed using ZFC, or that it's not computable.

The claim was that its value is independent of ZFC, that the ZFC axioms do not make any logical implication about the value. This necessarily means that there are multiple possible values; if there were only one value, that value would be logically implied by ZFC regardless of whether it was provable in ZFC.

I should also note that these two observations are not compatible with each other:

> BB(745) is a specific integer, so it's nothing more than a sequence of finite digits

> BB(745) can't be constructed using ZFC

All finite digit sequences can be constructed.

>This necessarily means that there are multiple possible values; if there were only one value, that value would be logically implied by ZFC regardless of whether it was provable in ZFC.

This is a false statement. The fact that BB(745) can't be constructed using ZFC does not mean that it has multiple values. All it means is that there is at least one Turing Machine that never halts but can't be proven to run forever using ZFC, that is it.

BB(745) is one specific integer, there is nothing really special about ZFC in this sense, it's just one axiomatic system that happens to be very useful as the foundation of most of the mathematics that is studied, but one could just as easily work with a different axiomatic system instead.

There are values of BB(n) that have no construction using Peano arithmetic but do have a construction in ZF, and there are values of BB(n) that do not have a construction in ZF but have one in ZFC, and there are values of BB(n) that do not have a construction in ZFC but do have one in ZFC + Inaccessible Cardinal Axiom, so on so forth.

ZFC does not have some kind of authoritative status in the universe of mathematics; it's possible that an alien race is doing mathematics using a far more powerful axiomatic system in which case BB(745) is constructible but BB(7450) is not.

>All finite digit sequences can be constructed.

A construction is a proof that provides a means of calculating a given value [1]. The set of all theorems that can be enumerated in ZFC do not contain a construction for the value of BB(745).

[1] https://en.wikipedia.org/wiki/Constructive_proof

> A construction is a proof that provides a means of calculating a given value [1]. The set of all theorems that can be enumerated in ZFC do not contain a construction for the value of BB(745).

Of course they do. They just don't contain a proof that that value has the relevant properties that define the Busy Beaver sequence.

There's a big difference between constructing the value 107 and proving that that same value satisfies a given set of constraints.

We'll agree to disagree on this point then. My stance is you're using the word construction in a more layman like manner whereas I am using it in the more formal sense. It's not a particularly big deal either way.

Think of it this way:

Is it possible to construct the value 2?

Is it possible to construct 3?

Is it possible to construct 4?

[...]

The answer to all of these questions is obviously "yes".

Is BB(745) one of those constructible numbers? This is harder to answer, except that you have firmly taken the position that it is. Hence it must be constructible.

> The claim was that its value is independent of ZFC, that the ZFC axioms do not make any logical implication about the value.

This is not what "independent from ZFC" means: e.g. ZFC easily proves that BB(745) is larger than 10000. It even proves that BB(745) is a sum of at most six primes.

Independence here just means that for any fixed (meta-theoretic) numeral n, ZFC cannot prove that BB(745) is exactly n -- unless ZFC is inconsistent, a possibility we can't really rule out.

This implies that ZFC (again, if it's consistent) does not suffice to establish an explicit upper bound BB(745) < n either. But that's very far from ZFC not making _any_ logical implications about the value.

> This is not what "independent from ZFC" means: e.g. ZFC easily proves that BB(745) is larger than 10000. It even proves that BB(745) is a sum of at most six primes.

I would respond to the first example by noting that you're correct, but I am limited to using a finite number of words when I talk, and to the second one by not considering it a contradiction of what I said. (Though I'm making the assumption here that you're applying a theorem that holds for every integer to BB(745).)

> Independence here just means that for any fixed (meta-theoretic) numeral n, ZFC cannot prove that BB(745) is exactly n -- unless ZFC is inconsistent, a possibility we can't really rule out.

My understanding was that the independence of the continuum hypothesis takes the following form:

(1) If ZFC is consistent, then ZFC ∪ {CH} is also consistent.

(2) If ZFC is consistent, then ZFC ∪ {¬CH} is also consistent.

This is quite explicit that independence allows for the selection of (one of) multiple values. It happens to be an exact match to what is given on Wikipedia right now:

> The answer to this problem is independent of ZFC, so that either the continuum hypothesis or its negation can be added as an axiom to ZFC set theory, with the resulting theory being consistent if and only if ZFC is consistent.

You appear to be saying that a proposition that is entailed by ZFC, but not proven by ZFC, is nevertheless independent of ZFC, but I don't think that can be right?

"The proposition CH is independent of ZFC" and "the value of BB(745) is independent of ZFC" are two different statements.

A proposition P is independent of ZFC if it's not possible to prove P and not possible to prove its negation ~P either.

If P(-) is a unary predicate, we say that the value of an integer v with definition P(-) is independent of ZFC if ZFC proves that there is a unique integer v such that P(v), but fails to prove that P(v) implies v=n for any specific (meta-theoretic) numeral n. This means that no propositions of the form v=n are provable in ZFC. It does not imply that all propositions of the form v=n (v≠n) are independent of ZFC!

Basically, two different (but not unrelated) senses of independent.

Thanks!

> This means that no propositions of the form v=n are provable in ZFC. It does not imply that all propositions of the form v=n (v≠n) are independent of ZFC!

Doesn't it mean that there are at least two such propositions, v=n_1 and v=n_2, which are both independent of ZFC?

Assume there is a fixed unique integer i such that i = BB(745).

We know that v=n is unprovable for all n, including i.

We know that v≠i is unprovable because (a) it is a false statement; and (b) we assumed ZFC was consistent.

All that remains to be shown is that there is some other integer j for which v≠j is unprovable. This must be the case: if v≠j were provable for all integers j not equal to i, that would constitute a proof that v=i,† and v=i is unprovable.

So v=i and v=j are both simple truth-valued propositions that are independent of ZFC.

Why are i and j not equally valid choices for the value of v?

† because "ZFC proves that there is a unique integer v such that P(v)"

Sure you are right there would be at least two propositions with different values of n_1 and n_2 that are independent of ZFC. But this does not mean that BB(745) has two values that are actually true, it just means that ZFC is unable to determine which of those two propositions is correct and which one is incorrect.

In fact, from outside of ZFC, it's trivial to see that the correct value would be whichever of the two standard integers is larger, if n_1 is a standard integer and is greater than n_2 then BB(745) would be n_1, otherwise it would be n_2. If there are X such propositions involving standard integers that are independent of ZFC then the actual value of BB(745) would be max(n_1, n_2, ..., n_X).

Of course ZFC can't prove this but that doesn't mean that the real value is unknowable or that the actual value is ambiguous or could take on different values. All it means is that ZFC does not have a sufficiently powerful axiom to prove which of the two values is the true value.

Furthermore because the busy beaver function is co-recursively enumerable, then it follows that any axiomatic system that was able to prove that BB(745) is a different standard integer from max(n_1, n_2, ..., n_X) would be inconsistent, even though ZFC would be unable to prove its inconsistency.

As I said before, ZFC holds no special status or authority on the nature of the busy beaver function so just because ZFC is not powerful enough to discriminate between a set of propositions about what the value of BB(745) is does not mean that BB(745) can actually take on multiple values depending on your interpretation.

I think this is wrong. Because we can run the Turing machines for max(n1, n2) steps. If a machine halts after that many steps, then it rules out the lesser value. If none of them halts after that many steps it rules out the greater value.

So our only uncertainty is between one specific number, and some unspecific bigger number that forever recedes into the distance as we try to approach it.

You propose that the issue is some pesky non-standard numbers that are bigger than any other number. But I'm thinking the issue is rather the for-all symbol.

Like from the outside of the theory we can see that we can prove a certain property for 1, for 2, for 3 etc, in fact we can prove this property for any number. But inside the theory we cannot prove that for-all n the property holds. So there is a divergence between what we want for-all to mean and what it actually ends up meaning?

Or using the there-exists perspective, if there exists an actual object inside a theory that satisfies a property P, then there-exists x such that P(x) will be true. But it can also be true without such an actual object existing.

The more I think about this the more I start to doubt it..

No at all, you are absolutely correct and what you describe is known as omega-consistency!

https://en.wikipedia.org/wiki/%CE%A9-consistent_theory

However, your description is just another way of saying what I'm saying about nonstandard numbers. From outside of the theory you can prove P(1), P(2), P(n) for any N that is an actual natural number, but from inside of the theory you can't do that. Why not? Because from inside of the theory there is a model that is completely consistent with Peano arithmetic but contains some object E that is greater than any standard natural number. The theory can not eliminate the existence of this E and in fact it's possible to construct an E such that P(E) is false.

> In fact, from outside of ZFC, it's trivial to see that the correct value would be whichever of the two standard integers is larger, if n_1 is a standard integer and is greater than n_2 then BB(745) would be n_1, otherwise it would be n_2. If there are X such propositions involving standard integers that are independent of ZFC then the actual value of BB(745) would be max(n_1, n_2, ..., n_X).

This doesn't sound trivial to me. It's easy to see that the largest such value is an upper bound on BB(745), but even that isn't worth much. There could be an infinite number of such values. (In which case your definition of which value was correct would contradict the earlier statement that ZFC proves a unique value of BB(745) exists!)

Also...

> In fact, from outside of ZFC, it's trivial to see that the correct value would be whichever of the two standard integers is larger

What part of your analysis takes place outside of ZFC? This looks to me like you're about to propose that ZFC contains a proof of the value of BB(745), contradicting the stipulation that it doesn't.

-----

In particular, let's say that we have two values, n_1 < n_2, for which BB(745)≠n [either n] cannot be proved.

The definition of the busy beaver sequence tells us that BB(745) is the maximum number of steps a 745-state Turing machine can take without halting, if it's ever going to halt at all.

Describing a 745-state Turing machine which halts after k > n_1 steps would prove BB(745)≠n_1, and therefore cannot be done. But unless we believe that there are Turing machines which ZFC is not able to describe, this would also mean that no such Turing machine exists (since existence would imply description, and description would prove the unprovable). That would make n_1 the "true" value.

But now we have the problem that we just proved v=n_1, which also can't be done.

Did I make a mistake somewhere? Where did we leave ZFC?

>It's easy to see that the largest such value is an upper bound on BB(745), but even that isn't worth much.

Having an upper bound on the value of a BB(N) is all you need to solve BB(N). Why? Because if you have an upper bound called U, then you know that any Turing Machine that runs for more than U steps will run forever. So an upper bound is as good as a solution.

>There could be an infinite number of such values.

No there can't be an infinite number of these because the number of 745 state Turing Machines is finite and each Turing Machine represents one possible value for what BB(N) can be. The number of possible binary Turing Machines with N states is 6 * (N + 1) ^ (3 * N).

As for the rest of your post, I think to address it we should step back from busy beavers and just focus on one specific aspect of it that is easier to reason about.

Let's say there's some Turing Machine H, and whether H halts is independent of ZFC, that is ZFC is unable to prove whether H halts or runs forever. Does this mean that in fact H can both halt and not halt depending on our interpretation? Is it possible that H both halts and does not halt? Can we as humans just decide to choose one axiomatic system where H halts, or we can decide to choose another axiomatic system where H does not halt and both systems are perfectly valid and legitimate?

Of course not. If whether H halts or runs forever is independent of ZFC, then in fact H never halts. It's not a matter of personal choice, or a matter of interpretation, or something we can just arbitrarily choose, H simply runs forever.

We can tell from outside of ZFC that H must run forever, even though from inside of ZFC the proposition is unprovable. That does not mean that ZFC is able to prove that H halts; what it means is that ZFC is unable to precisely define what a natural number is and that from inside of ZFC there are two possible systems of natural numbers:

In one system of natural numbers H runs forever, which is the system of natural numbers that corresponds to the actual truth. This system of natural numbers is what we call the standard model of arithmetic and is the intended interpretation of the natural numbers [1].

In another system of natural numbers, the nonstandard model of arithmetic, H halts after X steps where X is a nonstandard natural number [2]. You can think of a nonstandard natural number as a number that is larger than any standard natural number, for example imagine a whole number with an infinite number of digits. Now we know that a natural number is only supposed to have a finite number of digits, but ZFC is not powerful enough to define natural numbers this way, so it can not eliminate every model of natural numbers that have infinite digits and in one such model H does halt.

In fact, no consistent first order system is powerful enough to define natural numbers in such a way that they only have a finite number of digits, every single first order system will have some model of natural numbers that have an infinite number of digits.

So no, the fact that HALT(H) is independent of ZFC does not mean that we can just decide to pick an axiomatic system where H halts or one where it does not halt and both are valid choices, because in the system where H halts we are no longer working with the actual natural numbers. It's only in the axiomatic system where H never halts that we get to work with the natural numbers.

Given these concepts, you can now apply them to better understand how the busy beaver function can only have one single value. Yes there are propositions of ZFC where BB(745) = n1, and BB(745) = n2, and both of these propositions are independent of ZFC. No, that does not mean that BB(745) can actually be either n1 or n2 and the choice is a matter of preference. Only one axiomatic system represents the actual natural numbers, and the other ones represent the nonstandard natural numbers whose values can be infinitely large and have infinitely many digits.

[1] https://en.wikipedia.org/wiki/Interpretation_(logic)#Intende...

[2] https://en.wikipedia.org/wiki/Non-standard_model_of_arithmet...

> All finite digit sequences can be constructed.

You can construct the particular natural number that it is, obviously. Constructing BB(745) means providing that number and a proof that it's the right one.

BB(745) is some specific number N. Numbers cannot be independent of ZFC.

Only boolean valued formulas can be.

In this case, the relevant formula F expresses that all 745 state TMs that do not halt within N steps, will never halt. Assuming consistency of ZFC, formula F is true but unprovable in ZFC, and thus independent.

Another formula G expresses that some specific 745 state TM halts in exactly N steps. Formula G is true and provable in ZFC. F and G together imply that BB(745) = N.

I would assume tiny refers to three.

See also this article (shared on Hacker News 2 weeks ago): https://www.sligocki.com//2023/10/16/bb-3-3-is-hard.html

Basically, they showed that a VERY small Turing Machine -- of a size many had hoped we would be able to exhaustively solve -- turns out to depend on whether something similar to the Collatz sequence ever haults.

In other words, research published just 2 weeks ago shows that we don't need a Turing machine with a couple thousand states to be beyond the reach of modern human mathematics -- even one with just a few states can stimy us.

Also, for a nice deepening of the situation.. in the 70's John Conway proved that generalized Collatz problems are undecidable. AKA, you can compile turing machines to Collatz problems

This means all the characteristics of busy beaver numbers, including how every axiom system has a limit in what it can prove, is actually true of Collatz problems too.

What does "exhaustively solve a Turing Machine" mean is this context?

I interpreted that to mean "exhaustively determine whether or not every single (3,3) Turing machine halts", thereby computing BB(3,3). After all, there are only 19^9 (around 2^39) of them.

“Solve” means “solve the halting problem for” (i.e. prove whether it will halt or not), and “exhaustively” means “for all possible Turing machines with a given number of states”

But intuitively a Turning machine, no matter how small number of states, can't be exhaustively solved, since there are infinite number of possilbe strings on the tape?

Proving properties hold over sets of infinite cardinality is fairly routine in mathematics.

We know that not every Turing Machine can be “solved”, because this would give us an oracle for HALT, but there are machines that can be.

A trivial example is a TM that halts immediately, regardless of the input; a less trivial example is one that reads an arbitrarily large integer input on the tape and outputs its factorisation (or, if we don’t want to consider output, decides whether an input pair is formed of an integer and it’s factorisation).

Given that the set of Turing Machines with a certain number of states (or less) is finite for a given alphabet, it’s “just” a case of solving that finite set.

EDIT: Note that as the sibling comment points out, BB is usually considered to start with an empty tape, but fundamentally, proving that a machine always halts regardless of their starting tape is not intrinsically impossible as you suggest.

Generally, when we talk about the halting problem in the Busy Beaver context, we're talking about the halting problem starting from an empty tape. However, some authors have analyzed the behavior of Turing machines on certain classes of infinite tapes. For instance, in [0], the authors surveyed the behavior of TMs starting on a tape with an arbitrary word in the middle, and an infinitely repeating word on one or both sides; one finding is that no 2-state 2-symbol TM is a universal Turing machine, for any of these input tapes.

[0] https://arxiv.org/abs/1110.2230

Be sure to also read the referenced essay "Who Can Name The Biggest Number?", it's loads of fun and a great explanation of the BB function: https://www.scottaaronson.com/writings/bignumbers.html

Adam Yedidia had a claim to fame other than being SBF’s roommate.

> In more detail, we know that it’s possible with our laws of physics to build a self-replicating machine: say, DNA or RNA and their associated paraphernalia. We also know that tiny molecules like H2O and CO2 are not self-replicating. But we don’t know how small the smallest self-replicating molecule can be—and that’s an issue that influences whether we should expect to find ourselves alone in the universe or find it teeming with life.

DNA and RNA typically isn't self-replicating. As indicated in this very quote is takes a machine to do so.

In a world with 'volcanoes' that emit pure hydrogen gas and pure oxygen gas (not from the same 'volcano', H2O could indeed be self-replicating by generating a greenhouse effect raising the temperature to the autoignition point of hydrogen gas (535°C according to Wikipedia).

These are nitpicks, though. I get the general point.

I'm always delighted by how the real content is always in the comments. I wish I understood the principle of sociology/psychology that caused this to be true.

It's probably pretty simple: someone writes a thought-provoking article, and then the experts cone together to discuss it. Among the experts there are people with interesting views or ability explain complicated things simply.

I wonder if we could switch to "ation scale" where every number is notated as fractional N-ation required to make it. Then we can fit any natural number we use betwern 3 and 4, and even BB numbers will not be very scary. We get them back to the realm of writedownity.

Is there a function to convert fractional numbers between natural and ation scale? A(2) = 4, A(3) = 27, A(4) = 10 ^ (10 ^ 154), but what's A(3.5)?

This program is at least related to what you want: https://googology.fandom.com/wiki/Hypercalc -- and the community there has devised other systems for representing huge numbers with compact notations.

What is "fractional N-ation"?

You can regard multiplication as repeated additions, exponentiation as repeated multiplications, tetration as repeated exponentiation and so on. Of course they are not just repeated operations; you've got to define them for negative, fractional and complex operands in a justifiable way as well. Note that those operations also form a sequence, so let's rename addition to 1-ation, ..., tetration to 4-ation (in fact tetra- prefix exactly means this) and so on. Now, what could be 2.5-ation or pi-ation?

The point being, what's the pi-ation of pi.

https://hn.algolia.com/?query=The%208000th%20Busy%20Beaver%2...

Reply on news.ycombinator.com