[HN Gopher] The 8000th Busy Beaver number eludes ZF set theory (...
___________________________________________________________________
The 8000th Busy Beaver number eludes ZF set theory (2016)
Author : jkubicek
Score : 81 points
Date : 2023-11-02 14:13 UTC (8 hours ago)
(HTM) web link (scottaaronson.blog)
(TXT) w3m dump (scottaaronson.blog)
| jkubicek wrote:
| Adam Yedidia had a claim to fame _other_ than being SBF's
| roommate.
| vecter wrote:
| 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 Godel's
| Theorem.
| adverbly wrote:
| > 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?
| _a_a_a_ wrote:
| Because it says 'clearly'. (but yeah, agree with you)
| meithecatte wrote:
| Checking whether a string of bits encodes a proof of False in
| ZF is decidable. Now enumerate the bitstrings and check each.
| tomstuart wrote:
| 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.
| tromp wrote:
| 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.
| arethuza wrote:
| BB(748) - BB(745) is probably the largest value that anyone has
| ever described as "tiny" :-)
| danbruc wrote:
| I would assume tiny refers to three.
| sebzim4500 wrote:
| 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
| cyberax wrote:
| 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 Godel'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.
| henry2023 wrote:
| 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.
| magicalhippo wrote:
| But programming is math[1], so is the conclusion that math
| will eat itself?
|
| [1]: as many argue in the software patent cases
| andrewflnr wrote:
| > completely destroys any possible conception of mathematics
|
| Hyperbolic, to put it gently. It changes our conception of
| mathematics to a different conception.
| Dylan16807 wrote:
| 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.
| winwang wrote:
| 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?
| srcreigh wrote:
| > 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
| tutfbhuf wrote:
| 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.
| VirusNewbie wrote:
| >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
| snarkconjecture wrote:
| 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.
| passion__desire wrote:
| 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
| NoMoreNicksLeft wrote:
| 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.
| karmakurtisaani wrote:
| 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.
| SonOfLilit wrote:
| 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
| mcherm wrote:
| 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.
| raincole wrote:
| What does "exhaustively solve a Turing Machine" mean is this
| context?
| pxeger1 wrote:
| "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"
| raincole wrote:
| 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?
| denotational wrote:
| 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.
| LegionMammal978 wrote:
| 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
| klyrs wrote:
| 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.
| thriftwy wrote:
| 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)?
| UncombedCoconut wrote:
| 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.
| srcreigh wrote:
| What is "fractional N-ation"?
| cryptonector wrote:
| https://hn.algolia.com/?query=The%208000th%20Busy%20Beaver%2...
___________________________________________________________________
(page generated 2023-11-02 23:00 UTC)