Re: Some ambiguities about the Busy Beaver sequence.


ram.rachum@xxxxxxxxx wrote:
Rupert wrote:
ram.rachum@xxxxxxxxx wrote:
Hello everyone. There are some things that are unclear to me about the
fascinating Busy Beaver sequence.

I will explain my reasoning, and please correct me if I made any
mistake.
Let's take the Turing machine that searches for a proof of Godel's G.
Let's say it has 2000 states. We can neither prove that this machine
halts, since that would prove that G has a proof, and we can't prove
that this machine would not halt, since that would prove that G doesn't
have a proof, which is G. So it seems like we can't prove whether this
machine halts. But that also means that we can't prove what is
BB(2000), even if we had all the other machines completely analyzed.

Can anyone resolve the matter?

What you're saying is basically right. Given a natural number n, let #n
be the numeral for n. If, for each m, there existed an n such that
"BB(#m)=#n" was a theorem of ZFC, and ZFC were consistent, then BB
would be a recursive function. But it's not. So, if ZFC is consistent,
there must be an m such that there is no theorem of ZFC of the form
"BB(#m)=#n". There's no reason why we should have to be able to prove
every conceivable fact about the Busy Beaver function in ZFC.

So does that mean that in our example BB(2000) does not exist?

No. It cannot be calculated in ZFC, but it can still be proven to
exist. Of
course, the higher values can't be calculated either. But they too are
provably existent.

[...]
If BB(2000) does exist, how can we prove what it is if we cannot
determine whether G is provable?

We would have to use a stronger set theory. For example, it might be
that assuming the existence of measurable cardinals allows us to
calculate BB(2000), but not BB(2001). (Every theory will fail at some
point, of course.)

.

Relevant Pages

  • Re: Some ambiguities about the Busy Beaver sequence.
    ... fascinating Busy Beaver sequence. ... I will explain my reasoning, and please correct me if I made any ... "BB=#n" was a theorem of ZFC, and ZFC were consistent, then BB ... every conceivable fact about the Busy Beaver function in ZFC. ...
    (sci.logic)
  • Re: Some ambiguities about the Busy Beaver sequence.
    ... I will explain my reasoning, and please correct me if I made any ... halts, since that would prove that G has a proof, and we can't prove ... "BB=#n" was a theorem of ZFC, and ZFC were consistent, then BB ... every conceivable fact about the Busy Beaver function in ZFC. ...
    (sci.logic)
  • Re: Some ambiguities about the Busy Beaver sequence.
    ... fascinating Busy Beaver sequence. ... I will explain my reasoning, and please correct me if I made any ... "BB=#n" was a theorem of ZFC, and ZFC were consistent, then BB ... every conceivable fact about the Busy Beaver function in ZFC. ...
    (sci.logic)
  • Re: What is the 1st order formal system known as PA?
    ... > certain reasoning agent]. ... > any model of ZFC is one of ZF; and the ZFC theory is effectively also ... >> David C. Ullrich ...
    (sci.logic)
  • Re: What is the 1st order formal system known as PA?
    ... David C. Ullrich wrote: ... And then once we've set up the formal system the symbol ... We know ZF and ZFC are 2 *different theories*, ... reasoning framework so that it would also encompass the main principle of "Multi-Agent Reasoning", where do you think we could begin? ...
    (sci.logic)