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

221–230 of 232 posts

Re: BusyBeaver(6) Is Quite Large

#221

Post by Straw »

SAI_Peregrinus wrote: post #114
dtech wrote: post #24

Earlier quoted context omitted.

I am also not an expert, but this does not sound right to me. Godel's incompleteness theorem shows that there are certain things that cannot be proven. Being independent of ZFC means that something is such a case. So BB(643) being independent of ZFC means that we cannot prove or disprove that a certain number is BB(643). Aka we don't have the math to know for certain.

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…

Don't you want the weakest (ie makes the fewest assumptions) theory that works?

Re: BusyBeaver(6) Is Quite Large

#222

Post by Straw »

Straw wrote: post #13
Scarblac wrote: post #4

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.

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

To downvoters:

I'm well aware that BB(748) is an integer definable in classical logic. My claim is that "integer definable in classical logic" does not actually correspond well to what people mean by "number" in almost any other setting when pushed to extremes such as this.

Re: BusyBeaver(6) Is Quite Large

#223

Post by Straw »

ajkjk wrote: post #20
Straw wrote: post #14

Earlier quoted context omitted.

Sure, if someone just gives you the number, ZFC can represent it. But ZFC cannot prove that the value is correct, so how do you know you have the right number? Use a stronger proof system? Go a bit bigger and same issue.

Not an expert, but I've read about this a bit because it bothered me also and I think this is the answer: Most of these 'uncomputable' problems are uncomputable in the sense of the halting problem: you can write down an algorithm that should compute them, but it might never halt. That's the sense in which BB(x) is uncomputable: you won't know if you're done ever, because you can't distinguish a machine that never hal…

It likely comes from the smallest machine that someone has been able to construct that can diagonalize over all proofs in ZFC, or something similar.

Re: BusyBeaver(6) Is Quite Large

#224

Post by Straw »

falcor84 wrote: post #49
lupire wrote: post #32

Earlier quoted context omitted.

Only if you believe that a number you can't count is a number. You can believe that, but it's a leap.

Couldn't you make the same argument for sqrt(2), or better yet for zero [0]? [0] https://en.wikipedia.org/wiki/Zero:_The_Biography_of_a_Dange...

sqrt(2), and pretty much everything else you can think if, is computable- there's a program that can output rational numbers arbitrarily close.

BB(n) is not.

Re: BusyBeaver(6) Is Quite Large

#225

Post by edanm »

raincole wrote: post #196
wat10000 wrote: post #193

Earlier quoted context omitted.

My argument has nothing to do with the universe. My argument is that there is a single definition of the BB function and its definition does not allow for different values in different circumstances. What is “a model” here? Can I say that there’s a model ZFC’ which is the same as ZFC except that 107 is considered to be equivalent to 200, and therefore BB(4) in ZFC’ is actually 200? Or can I say that ZFC’’ says intege…

> Or can I say that ZFC’’ says integers only go up to 100 and therefore BB(4) is 100 in that model? You'd be defining a new axiomatic system here, not just a model of ZFC. I don't know how we're going to formalize Turning machine in this system, but if we managed to do it, the value of BB(4) is likely to be indeed 100, at least for some models of this new system. Roughly speaking, a model of ZFC is a set and a binary…

> An axiomatic system can be consistent, but wrong.

But then its unsound, isn't it? Isn't our background assumption that ZFC is consistent and sound? It can't prove its own consistency, but we are assuming that under standard models, it is sound.

> For example, if ZFC is consistent, then T = ZFC+~Con(ZFC) would be consistent as well.

It would be consistent if ZFC didn't also prove ZFC+Con(ZFC), but then it would indeed be unsound.

> Similarly, if ZFC is indeed consistent, then T is wrong about which Turing machines halt. Therefore it would have a wrong value of BB(748) (and many other BB(n)).

No, if it's sound, it just doesn't have a proof of the form "BB(748)=K" for any K.

> However, since ZFC can't prove its own consistency, it can't prove that value is wrong. That's why there are different values of BB(748). Those values are not necessarily equally correct, it's just that ZFC isn't strong enough to prove which one is wrong.

No, ZFC is just not strong enough to prove any of these.

Re: BusyBeaver(6) Is Quite Large

#226

Post by red75prime »

red75prime wrote: post #206
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…

> 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 s…

It seems to be even easier: BB codomain is a set of standard natural numbers regardless of which model of ZFS we are using. Therefore BB(748)=Q is false for every non-standard natural number Q.

We can come up with some function BB' that admits that, but it's just a different function.

It seems we can't even define a function with standard domain and non-standard codomain while not using literals for non-standard numbers in its definition.

That is ~(BB(748)=ActualValueOfBB748) is false even if it can't be proven in ZFC. In a sense, busy beaver creates its own mathematical reality.

Re: BusyBeaver(6) Is Quite Large

#227

Post by wat10000 »

Kranar wrote: post #216
wat10000 wrote: post #214

Earlier quoted context omitted.

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…

That sounds to me like "your model might not be what you want it to be and it might define an infinite value for BB(748)," not "BB(748) has different values depending on the model."

Re: BusyBeaver(6) Is Quite Large

#228

Post by red75prime »

wat10000 wrote: post #227
Kranar wrote: post #216

Earlier quoted context omitted.

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…

That sounds to me like "your model might not be what you want it to be and it might define an infinite value for BB(748)," not "BB(748) has different values depending on the model."

BB(748) has a single value. It is a finite number of steps (N) of some specific Turing machine. ZFC can't prove neither BB(748)=N, nor ~(BB(748)=N). But BB(748)=N is true and ~(BB(748)=N) is false anyway. The end.

Re: BusyBeaver(6) Is Quite Large

#229

Post by Kranar »

wat10000 wrote: post #227
Kranar wrote: post #216

Earlier quoted context omitted.

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…

That sounds to me like "your model might not be what you want it to be and it might define an infinite value for BB(748)," not "BB(748) has different values depending on the model."

Ultimately, I am addressing the original point that was made:

>I think the more correct statement is that there are different models of ZFC in which BB(748) are different numbers.

You asked how this was possible and that's the specific question that I am addressing. As I mentioned elsewhere, to fully appreciate this answer requires parsing some very subtle and nuanced details that simply can not be glossed over or dismissed, if you genuinely want to know how it's possible that ZFC can be consistent even though different models give different values of BB(748).

If you want to argue something else, about what model is correct or what model is incorrect, that's a perfectly fine argument to have but it's more in the realm of philosophy than it is in the realm of formal mathematics.

Re: BusyBeaver(6) Is Quite Large

#230

Post by SAI_Peregrinus »

Straw wrote: post #221
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…

Don't you want the weakest (ie makes the fewest assumptions) theory that works?

Yes, which is why ZFC gets used. NBG & MK are stronger and occasionally used, but ZFC being weaker meant it got more popular since it's almost always good enough.
Post reply on HN