Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

BusyBeaver(6) Is Quite Large

scottaaronson.blog

Post reply on HN
Print view View original

201–210 of 232 posts

Re: BusyBeaver(6) Is Quite Large

#201

Post by wat10000 »

Kranar wrote: post #200
wat10000 wrote: post #199

Earlier quoted context omitted.

Am I understanding you correctly that there’s is one specific finite integer which equals BB(748), but that some models of ZFC will say it’s a different one, and it’s just not correct? And since we can find a four-state Turing machine that runs for more than 100 steps before halting, ZFC’’ is just not correct when it says that BB(4) = 100, but we still say that 100 is the value in that model?

In all models where BB(748) = F and F is actually finite, then F will be the same in all such models. There can't be two models that disagree about the value of F for some actual natural number. It's only in models where BB(748) = Q where Q != F then Q is necessarily not actually finite and hence not an actual natural number. From within those models Q satisfies all the properties of being a natural number but it's n…

I think this is where I get stuck (or it falls apart). The definition of BB requires it to equal an actual natural number. If you have a model where BB(748) = Q not an actual natural number, then what you have isn’t actually BB, but some other function.

Re: BusyBeaver(6) Is Quite Large

#202

Post by Kranar »

wat10000 wrote: post #201
Kranar wrote: post #200

Earlier quoted context omitted.

In all models where BB(748) = F and F is actually finite, then F will be the same in all such models. There can't be two models that disagree about the value of F for some actual natural number. It's only in models where BB(748) = Q where Q != F then Q is necessarily not actually finite and hence not an actual natural number. From within those models Q satisfies all the properties of being a natural number but it's n…

I think this is where I get stuck (or it falls apart). The definition of BB requires it to equal an actual natural number. If you have a model where BB(748) = Q not an actual natural number, then what you have isn’t actually BB, but some other function.

The issue is that it's impossible to formally and uniquely define the actual natural numbers, and hence it's impossible to require as part of the formal definition of some mathematical object like BB(n) to equal an actual natural number.

Yes, between you and me we know that BB(n) needs to be a natural number, but we have no way to formally and uniquely define what natural numbers are. The best we can do is come up with a formal definition of natural numbers that includes the actual natural numbers but will also include other number systems that contain mathematical objects that are infinitely big and hence are not actual natural numbers. Hence our formal definition of natural numbers will not uniquely define a single set of numbers {0, 1, 2, 3, ...}, there will be other sets of numbers such as {0, 1, 2, 3, ..., Q - 1, Q, Q + 1, ...} for some infinitely large object Q that satisfy the formal definition of natural numbers. Between you and me, we both know Q isn't an actual natural number, but what we don't know is what formal rule we need to add to our formal definition of natural numbers in order to get rid of Q. In fact, it's worse than that; we know that even if we add a rule that gets rid of Q, there will always be some other number system {0, 1, 2, 3, ..., Q* - 1, Q*, Q* + 1, ...} to take its place. No formal definition can ever uniquely define the natural numbers (unless that formal system is inconsistent).

It's also true that a model where BB(748) = Q is not the actual BB, it's some other function. The problem is that this model satisfies all of the rules of ZFC and all of the properties that ZFC says natural numbers must satisfy and hence it satisfies the formal definition of BB even though it isn't the actual BB. Remember it is impossible for the formal definition of BB to include the property that BB(n) = an actual natural number, because there is no formal definition that uniquely singles out what the actual natural numbers are. Since there exists one such model that satisfies all of the rules about BB but isn't actually the real BB then we can't use ZFC to formally prove what the value of BB(748) actually is.

What we can do is add new rules to ZFC get rid of this model, but that will only push the issue down to BB(749) or BB(750) or maybe if pick a really powerful rule we push the issue down to BB(800)... but the point stands that adding new rules only pushes the problem further down the road, it never eliminates the problem entirely.

Re: BusyBeaver(6) Is Quite Large

#203

Post by wat10000 »

Kranar wrote: post #202
wat10000 wrote: post #201

Earlier quoted context omitted.

I think this is where I get stuck (or it falls apart). The definition of BB requires it to equal an actual natural number. If you have a model where BB(748) = Q not an actual natural number, then what you have isn’t actually BB, but some other function.

The issue is that it's impossible to formally and uniquely define the actual natural numbers, and hence it's impossible to require as part of the formal definition of some mathematical object like BB(n) to equal an actual natural number. Yes, between you and me we know that BB(n) needs to be a natural number, but we have no way to formally and uniquely define what natural numbers are. The best we can do is come up wi…

Does that mean that “finite” is not well defined? That would be very odd.

Re: BusyBeaver(6) Is Quite Large

#204

Post by drdeca »

nyrikki wrote: post #110
drdeca wrote: post #91

Earlier quoted context omitted.

Looking at [3], they seem to argue that the system isn’t complete for the usual Gödel reasons, which, sure, it isn’t, but then they call the claim that the system fails to decide, which is a statement about probability, a “scientific fact”. This seems to me like a mistake? Like, a TOE is not expected to decide all statements expressible in the theory, only to predict particular future states from past states, with as…

I will admit that I added that cite mostly because of the very real barriers to even learning RUSS. By the typos etc.. you. can probably also tell I was doing this on mobile, unfortunately as a passenger in a car. To quote Chaitin’s explanation here: > In contrast I would like to measure the power of a set of axioms and rules of inference. I would like to be able to say that if one has ten pounds of axioms and a twen…

Their notation of “ K_{ℱ_{QG}}” wasn’t a problem. Seems a reasonable name for a constant associated with Kolmogorov complexity and a formal system which they’ve named ℱ_{QG}.

The issue is that what they said seemingly was not

"There exists a natural number L such that we can't prove the Kolmogorov complexity of any specific string of bits is more than L."

But

"There exists a natural number L such that we can't prove (in ℱ_{QG}) any statement S whose complexity is more than L.",

which is wrong.

They later go on to say “These strings cannot be generated by programs of length <= n, and hence cannot correspond to provable statements in ℱ_{QG}.” which follows from the previous wrong statement but doesn’t follow from the accurate statement you gave, which seems to suggest that they really did mean the inaccurate statement that they wrote, not the correct one you wrote.

Re: BusyBeaver(6) Is Quite Large

#205

Post by Scarblac »

Kranar wrote: post #202
wat10000 wrote: post #201

Earlier quoted context omitted.

I think this is where I get stuck (or it falls apart). The definition of BB requires it to equal an actual natural number. If you have a model where BB(748) = Q not an actual natural number, then what you have isn’t actually BB, but some other function.

The issue is that it's impossible to formally and uniquely define the actual natural numbers, and hence it's impossible to require as part of the formal definition of some mathematical object like BB(n) to equal an actual natural number. Yes, between you and me we know that BB(n) needs to be a natural number, but we have no way to formally and uniquely define what natural numbers are. The best we can do is come up wi…

If we just use the successor function, so 0 is a natural number, and if n is a natural number then so is S(n). That should be enough to count steps of a halting Turing machine.

How could such a definition give rise to such a set with Q in it?

Re: BusyBeaver(6) Is Quite Large

#206

Post by red75prime »

Kranar wrote: post #202
wat10000 wrote: post #201

Earlier quoted context omitted.

I think this is where I get stuck (or it falls apart). The definition of BB requires it to equal an actual natural number. If you have a model where BB(748) = Q not an actual natural number, then what you have isn’t actually BB, but some other function.

The issue is that it's impossible to formally and uniquely define the actual natural numbers, and hence it's impossible to require as part of the formal definition of some mathematical object like BB(n) to equal an actual natural number. Yes, between you and me we know that BB(n) needs to be a natural number, but we have no way to formally and uniquely define what natural numbers are. The best we can do is come up wi…

> a model where BB(748) = Q is not the actual BB, it's some other function

What it means specifically? ZFC+~(BB(748)=N) allows to extend definition of the Turing machine to a non-standard number of steps?

Can "BB(748) is undefined" be a provable theorem in ZFC+~(BB(748)=N) instead?

While we know that ZFC+~(BB(748)=N) is consistent, we don't know whether \exist Q!=N where ZFC+(BB(748)=Q) is consistent.

Intuitively I see it as: by adding axiom ~(BB(748)=N), we codify that this formal system isn't powerful enough to describe a Turing machine with 748 states (and probably all the machines with number of states greater than 748).

Re: BusyBeaver(6) Is Quite Large

#207

Post by Nevermark »

fwip wrote: post #190
Nevermark wrote: post #70

Earlier quoted context omitted.

True but this is a ratio. However many universes in question, there is a qualitative difference between that many empty universes (with 1 grain), and that many completely packed with grain. Ask anybody who lives in one!

At very large numbers, even ratios don't really matter. For instance, if you personally owed $100 trillion, you wouldn't be much relieved by a court order that reduced your liability by 99%. Or, if you're looking at numbers in scientific notation, you don't much care about the difference between 2e40 and 5e40. In this case, the ratio is around 10^200. An incomprehensibly vast number, to be sure. But because tetration…

> For instance, if you personally owed $100 trillion, you wouldn't be much relieved by a court order that reduced your liability by 99%.

It is *never• true that differences don’t matter. Only true that in some respects the difference matters, others it does not.

You manufactured a reasonable situation for differences not mattering.

But if I had $1 trillion, 99% off $100 trillion would matter.

As I noted, from the perspective of anyone in those universes, a 1 grain universe, or a solid grain universe would each be a spotty context to make a living.

But in very different ways!

So in this case, the ratio between two incomprehensibly large numbers, happens to be highly comprehensible under the circumstances in which they were described. I.e. universes and grains.

One can imagine that one of unexplained constants of nature might be a result of differences between unimaginably large numbers. Which again shows, that there is no such things as numbers so large differences don’t matter. Only cases where they don’t matter, or do. As with all approximations.

Re: BusyBeaver(6) Is Quite Large

#208

Post by [deleted] »

Scarblac wrote: post #205
Kranar wrote: post #202

Earlier quoted context omitted.

The issue is that it's impossible to formally and uniquely define the actual natural numbers, and hence it's impossible to require as part of the formal definition of some mathematical object like BB(n) to equal an actual natural number. Yes, between you and me we know that BB(n) needs to be a natural number, but we have no way to formally and uniquely define what natural numbers are. The best we can do is come up wi…

If we just use the successor function, so 0 is a natural number, and if n is a natural number then so is S(n). That should be enough to count steps of a halting Turing machine. How could such a definition give rise to such a set with Q in it?

[deleted]

Re: BusyBeaver(6) Is Quite Large

#209

Post by raincole »

Scarblac wrote: post #205
Kranar wrote: post #202

Earlier quoted context omitted.

The issue is that it's impossible to formally and uniquely define the actual natural numbers, and hence it's impossible to require as part of the formal definition of some mathematical object like BB(n) to equal an actual natural number. Yes, between you and me we know that BB(n) needs to be a natural number, but we have no way to formally and uniquely define what natural numbers are. The best we can do is come up wi…

If we just use the successor function, so 0 is a natural number, and if n is a natural number then so is S(n). That should be enough to count steps of a halting Turing machine. How could such a definition give rise to such a set with Q in it?

You're right... with a catch.

What you described doesn't rule out {0,1,2... Q-1,Q,Q+1...}, because you only defined how to yield new natural number, but not exclude things that are not yielded that way from N (the set of all natural numbers).

Now, our intuition is to add this missing part into our axioms, right?

So instead:

> 0 is a natural number, and if n is a natural number then so is S(n)

We say:

> For any X⊆N, if 0 ∈ X, and for every n ∈ X, S(n) ∈ X, then X=N.

This is a perfect valid axiom. And it does rule out the nonstandard shit: for a set N' that looks like {0,1,2... Q-1,Q,Q+1...}, we can get X = {0,1,2...}, which is a subset of N'. According to this axiom, if N'=N then X=N', but it clearly doesn't because Q∈X while ~(Q∈N'). Therefore, N' isn't N.

However, this axiom is not included in the commonly accepted Peano Arithmetic! The reason is that this uses second-order logic, and Peano Arithmetic is a first-order theory.

The above axiom effectively defines a predicate, f(X), which accepts a set as input and returns whether the set is N. This is second-order logic.

Peano Arithmetic, being first-order logic, doesn't have such predicate. This is why we can't rule out these nonstandard {0,1,2... Q-1,Q,Q+1...}.

When it comes to ZFC, it's more complicate as in ZFC, 'natural numbers' are ordinals of sets. But ZFC is written in first-order logic as well, and it's known that an axiomatic system written in first-order logic will have nonstandard models. Even if you can rule out {0,1,2... Q-1,Q,Q+1...} by defining PA in ZFC in some unusual way or adding new axioms to ZFC, as long as it's still a first-order theory, it will have 0 (if inconsistent) or multiple (if consistent) models[0].

[0]: https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_...

Re: BusyBeaver(6) Is Quite Large

#210

Post by legobmw99 »

woopsn wrote: post #131
tromp wrote: post #57

Earlier quoted context omitted.

What makes BB(748) independent of ZFC is not its value, but the fact that one of the 748-state machines (call it TM_ZFC_INC) looks for an inconsistency (proof of FALSE) in ZFC and only halts upon finding one. Thus, any proof that BB(748) = N must either show that TM_ZF_INC halts within N steps or never halts. By Gödel's famous results, neither of those cases is possible if ZFC is assumed to be consistent.

Does the fact that BB(k)=N is provable up to some k < 748 mean that all halting problems for machines with k states are answered by a proof in ZFC?

748 is not tight. As given in the article, k=643 is independent of ZFC, and the author speculates that it's possible that something as small as BB(9) could be as well.

The 748/745/643 numbers are just examples of actual machines people have written, using that many states, that halt iff a proof of "false" is found.

At any rate, given the precise k, I believe your intuition is correct. I've heard this called 'proof by simulation' -- if you know a bound on BB(N), you can run a machine for that many steps and then you know if it will run forever. But this property is exactly the intuition for why it grows so fast, and why we will likely never definitively know anything beyond BB(5). BB(6) seems like it might be equivalent to the Collatz conjecture, for example.

Post reply on HN