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

211–220 of 232 posts

Re: BusyBeaver(6) Is Quite Large

#211

Post by SAI_Peregrinus »

ajkjk wrote: post #143
SAI_Peregrinus wrote: post #114

Earlier quoted context omitted.

Independence from ZFC means we can't prove that any given number is BB(643) using ZFC . It doesn't mean we can't prove it at all, e.g. one could use a stronger set theory like NBG which can prove the consistency of ZFC to verify the value of BB(643). But there would be some n for which BB(n) is independent of that set theory, requiring a yet-stronger theory, and so on ad infinitum. ZF & ZFC are as important as they a…

sure, but it is still very hard to wrap one's head around how the value of a function can be independent of ZFC, and how it could not be for (e.g.) 642 but then be true for 643. That was the point of my post. It seems like you could just... run the function on every 643-state input and see what the value is, which would in some sense constitute a "proof" in ZFC? but maybe not, because you wouldn't even know if you ha…

Some 643-state inputs never halt. Some 643-state inputs do eventually halt. Only if you can run them for infinite time can you determine whether a given machine halts in a finite length of time: for any finite time you pick, if the machine is still running it could still halt eventually. That's just the halting problem, the impossibility of solving it is quite famous and it's easy to find the proof stated more formally than I want to with the limits of HN's markdown.

The interesting bit is they were able to construct a machine that halts if ZFC is consistent. Since a consistent axiomatic system can never prove its own consistency (another famous proof) ZFC can't prove that this machine halts. And ZFC can't prove that it never halts without running it for infinite steps.

That ZFC-consistency-proving machine has 643 states, so BB(643) either halts after the ZFC-consistency-proving machine or the ZFC-consistency-proving machine never halts. If BB(643) halts after the ZFC-consistency-proving machine, then ZFC is consistent and ZFC can't prove BB(643) halts since ZFC can't prove the ZFC-consistency-proving machine halts.

Re: BusyBeaver(6) Is Quite Large

#212

Post by wat10000 »

raincole wrote: post #209
Scarblac wrote: post #205

Earlier quoted context omitted.

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, i…

"This is a perfect valid axiom. And it does rule out the nonstandard shit"

But the other commenter said:

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

Is there some subtlety that allows both of these statements to be true, or is this just a contradiction? Was the other commenter implicitly assuming "unless you involve second-order logic"?

Re: BusyBeaver(6) Is Quite Large

#213

Post by Kranar »

wat10000 wrote: post #203
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…

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

In first order logic this is correct, "finite" is not uniquely defined. Usually finite is defined in terms of natural numbers, but since natural numbers are not uniquely defined then it follows that finite is also not uniquely defined. Every model has its own interpretation of what it means to be finite, and in the model {0, 1, 2, ..., Q - 1, Q, Q + 1, ...}, Q is finite relative to that model.

In first order logic it's impossible to uniquely define any property that would also uniquely define the natural numbers.

Re: BusyBeaver(6) Is Quite Large

#214

Post by wat10000 »

Kranar wrote: post #213
wat10000 wrote: post #203

Earlier quoted context omitted.

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

In first order logic this is correct, "finite" is not uniquely defined. Usually finite is defined in terms of natural numbers, but since natural numbers are not uniquely defined then it follows that finite is also not uniquely defined. Every model has its own interpretation of what it means to be finite, and in the model {0, 1, 2, ..., Q - 1, Q, Q + 1, ...}, Q is finite relative to that model. In first order logic it…

From a sibling comment, it seems that using second-order logic resolves this. I'm comfortable saying that if you want to stick to first-order logic then you can say that BB(748) has different values depending on the model in some sense, but that the "real" BB function is defined using what we normally think of as the counting numbers as you'd define with second-order logic, and that's the value that's actually correct.

Re: BusyBeaver(6) Is Quite Large

#215

Post by [deleted] »

wat10000 wrote: post #212
raincole wrote: post #209

Earlier quoted context omitted.

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, i…

"This is a perfect valid axiom. And it does rule out the nonstandard shit" But the other commenter said: "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 c…

[deleted]

Re: BusyBeaver(6) Is Quite Large

#216

Post by Kranar »

wat10000 wrote: post #214
Kranar wrote: post #213

Earlier quoted context omitted.

In first order logic this is correct, "finite" is not uniquely defined. Usually finite is defined in terms of natural numbers, but since natural numbers are not uniquely defined then it follows that finite is also not uniquely defined. Every model has its own interpretation of what it means to be finite, and in the model {0, 1, 2, ..., Q - 1, Q, Q + 1, ...}, Q is finite relative to that model. In first order logic it…

From a sibling comment, it seems that using second-order logic resolves this. I'm comfortable saying that if you want to stick to first-order logic then you can say that BB(748) has different values depending on the model in some sense, but that the "real" BB function is defined using what we normally think of as the counting numbers as you'd define with second-order logic, and that's the value that's actually correc…

No second order logic does not resolve this, it actually makes the situation significantly worse since there is no effective proof system in second order logic. Second order logic is studied for its philosophical properties, as a way to understand the limits of logic and the relationship between syntax and semantics, but it's not used for the study of formal mathematics since it lacks an effective proof system.

What second order logic does let you do is deal with only one single model, called the categorical model. So instead of having a theory that has a whole bunch of different models including the actual natural numbers along with undesirable models that contain infinitely large values... you can force your theory to have one single model, no more "It's true in this model, but it's false in that other nonstandard model that's getting in the way." So yes in a particular theory of second order logic BB(748) has one single value because there is only one single model.

So problem solved right? Not even close... because that one single categorical model being used to represent the natural numbers may not be the actual natural numbers, the intended natural numbers where every number is actually finite. Having one single categorical model does not imply working with the actual model you intended to work with. Depending on your choice of second order theory you may be operating within a theory where the single categorical model is indeed unbeknownst to you {0, 1, 2, 3, ..., Q - 1, Q, Q + 1, ...} and hence BB(748) is equal to Q and you'll have no way of knowing this before hand since you lack an effective proof system.

Re: BusyBeaver(6) Is Quite Large

#217

Post by Kranar »

raincole wrote: post #209
Scarblac wrote: post #205

Earlier quoted context omitted.

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, i…

I think your contribution to this discussion has been very thorough but I need to nitpick some details:

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

You're right that this is a perfectly valid axiom in SOL, but it's not true that it rules out non-standard "shit". What this axiom does is it forces your theory to have a single model, the categorical model. But this axiom does not in anyway pick out the standard model as the categorical model, it doesn't force the categorical model to be the standard model. It's possible that N = {0, 1, 2, ..., Q - 1, Q, Q + 1, ...} in which case the categorical model ends up being nonstandard. This axiom has no way to force N to be intended standard model.

Re: BusyBeaver(6) Is Quite Large

#218

Post by josephcsible »

thaumasiotes wrote: post #182
Scarblac wrote: post #160

Earlier quoted context omitted.

What happens if you take the larger of a and b and run all the Turing machines for that many steps?

What are a and b?

Does it matter? My reading is basically "if you have two distinct candidates, isn't that a way to always disprove at least one of them?"

Re: BusyBeaver(6) Is Quite Large

#219

Post by Straw »

jerf wrote: post #19
Straw wrote: post #13

Earlier quoted context omitted.

The category error is in thinking that BB(748) is in fact, a number. It's merely a mathematical concept.

No, that's one of the freakiest things about things like the Busy Beaver function. There is an exact integer that BB(748) defines. You can add one to it and then it would no longer be that number anymore. If you are refering to the idea that nothing that can't exist in the real universe "really exists", then the "Busy Beaver" portion of that idea is extraneous, as 100% of integers can't exist in the real universe, an…

You say the busy beaver function is a function. But I can claim it's not, because you cannot make it constructively- in constructive analysis, all functions are computable.

Many other numbers and functions are computable, including e, pi, 10^100, etc- these are fundamentally different than BB.

So in what sense is it actually a number? There is no algorithm which can resolve questions such as BB(748) In fact, for some x, such questions will depend on the consistency of ZFC. All normal math we do is expressible in ZFC, but by incompleteness, ZFC cannot prove it's own consistency or is inconsistent. So, we cannot really ever know the value, we can only ever find lower bounds. Does this seem like a number to you? It's not in the English sense and neither is it in what I would consider a reasonable definition of numbers you actually encounter, the computable numbers. Real numbers are in fact, not very real at all.

Re: BusyBeaver(6) Is Quite Large

#220

Post by Straw »

bmacho wrote: post #55
Straw wrote: post #13

Earlier quoted context omitted.

The category error is in thinking that BB(748) is in fact, a number. It's merely a mathematical concept.

Let S be a statement. S is called semidecidible (also: Turing recognizable, most commonly "recursively enumerable", abbreviated as "r.e.", but I hate that one) if there is a Turing machine that halts if and only if S is true. With this definition, we can say that "ZFC is inconsistent" is semidecidible: you run a program that searches for a contradiction. The question BB(748) =/= 1000 is similarly semidecidable. You c…

Yes, I would say that neither is really a number in the traditional sense of the word, nor in constructive analysis.
Post reply on HN