6 ms·

The article says "if the usual axioms of set theory are consistent, we can never use them to determine the value of BB(7910)." But why does this imply that BB(7

The article says "if the usual axioms of set theory are consistent, we can never use them to determine the value of BB(7910)." But why does this imply that BB(7910) is uncomputable? Perhaps another axiomatic system could compute its value?

wolfgke 10y ago
> Perhaps another axiomatic system could compute its value? Of course another axiomatic system could. If you could tell us such an axiomatic system for which you can prove that it can determine the value of BB(7910) and have strong arguments why it is probably consistent (by Gödel one will not be able to prove this property if it is able to express basic arithmetic) mathematicians would love to get to know it, since they really have no idea how such a system might look like.
- ikeboy 10y ago
  It's easy to specify such a system that's more powerful than ZFC and has strong arguments for its consistency: ZFC+con(ZFC), which is consistent iff ZFC is consistent. And it's easy to go one level up, I.e that system plus it's own consistency. These systems will be stronger than ZFC, and will prove the machine in question halts. Of course, the lowest unknowable from ZFC BB number is probably around BB(15), so likely none of those systems get that high, but they do probably give us more than just ZFC does. See also http://www.scottaaronson.com/blog/?p=697 http://www.scottaaronson.com/blog/?p=697 for some limitations on this. Also, there are large cardinal axioms which imply the consistency of ZFC and are believed to be consistent, but I'm not so familiar with them. I think mathematicians would consider those axioms as "what such a system would look like".
- hyperpape 10y ago
  I think they do have some ideas. You might look at Believing The Axioms (http://cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf http://cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf, but it's two parts) which studies set theorists who are investigating new axioms for set theory, especially large cardinal axioms, iirc. Honestly, that work is a ways beyond what I can understand, but it's clear that it's an active area of research. You might also read about Hugh Woodin has a very developed program arguing for axioms which would imply the negation of the Continuum Hypothesis. (This doesn't necessarily apply to this specific question, but in general, research into axiomatic foundations of math is ongoing).
poppingtonic 10y ago
That's what he means. We need a formal system more powerful than ZFC, i.e. new mathematics. If a formal system can compute BB(7910), then it is more powerful than ZFC. I'm not sure anyone knows how to build that yet.
- ikeboy 10y ago
  See https://news.ycombinator.com/item?id=11753046 https://news.ycombinator.com/item?id=11753046 You can get more powerful, it's just unlikely anything we can build will get that high.
  - poppingtonic 10y ago
    I'm surprised it's that simple. Then again, simplicity is usually surprising.
versteegen 10y ago
Be careful with the word "incomputable" (the article never said it was "undecidable" or "incomputable"); in computability theory BB(7910) is computable because it's just a single finite number. You could in theory specify a TM that writes down the answer without doing any calculation - incomputable problems necessarily involve unbounded outputs or inputs which prevents such trivial solutions. I realise you're talking about formal systems specifically (which corresponds to a some theorem-checking TM implementing that system) but when you allow any system of axioms (e.g. one with the value of BB(7910) of axioms) you basically ask whether any TM can compute that number (including one that already 'knows' it).

wolfgke 10y ago

> Perhaps another axiomatic system could compute its value? Of course another axiomatic system could. If you could tell us such an axiomatic system for which you can prove that it can determine the value of BB(7910) and have strong arguments why it is probably consistent (by Gödel one will not be able to prove this property if it is able to express basic arithmetic) mathematicians would love to get to know it, since they really have no idea how such a system might look like.

ikeboy 10y ago
It's easy to specify such a system that's more powerful than ZFC and has strong arguments for its consistency: ZFC+con(ZFC), which is consistent iff ZFC is consistent. And it's easy to go one level up, I.e that system plus it's own consistency. These systems will be stronger than ZFC, and will prove the machine in question halts. Of course, the lowest unknowable from ZFC BB number is probably around BB(15), so likely none of those systems get that high, but they do probably give us more than just ZFC does. See also http://www.scottaaronson.com/blog/?p=697 http://www.scottaaronson.com/blog/?p=697 for some limitations on this. Also, there are large cardinal axioms which imply the consistency of ZFC and are believed to be consistent, but I'm not so familiar with them. I think mathematicians would consider those axioms as "what such a system would look like".
hyperpape 10y ago
I think they do have some ideas. You might look at Believing The Axioms (http://cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf http://cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf, but it's two parts) which studies set theorists who are investigating new axioms for set theory, especially large cardinal axioms, iirc. Honestly, that work is a ways beyond what I can understand, but it's clear that it's an active area of research. You might also read about Hugh Woodin has a very developed program arguing for axioms which would imply the negation of the Continuum Hypothesis. (This doesn't necessarily apply to this specific question, but in general, research into axiomatic foundations of math is ongoing).

poppingtonic 10y ago

That's what he means. We need a formal system more powerful than ZFC, i.e. new mathematics. If a formal system can compute BB(7910), then it is more powerful than ZFC. I'm not sure anyone knows how to build that yet.

ikeboy 10y ago
See https://news.ycombinator.com/item?id=11753046 https://news.ycombinator.com/item?id=11753046 You can get more powerful, it's just unlikely anything we can build will get that high.
- poppingtonic 10y ago
  I'm surprised it's that simple. Then again, simplicity is usually surprising.

versteegen 10y ago

Be careful with the word "incomputable" (the article never said it was "undecidable" or "incomputable"); in computability theory BB(7910) is computable because it's just a single finite number. You could in theory specify a TM that writes down the answer without doing any calculation - incomputable problems necessarily involve unbounded outputs or inputs which prevents such trivial solutions. I realise you're talking about formal systems specifically (which corresponds to a some theorem-checking TM implementing that system) but when you allow any system of axioms (e.g. one with the value of BB(7910) of axioms) you basically ask whether any TM can compute that number (including one that already 'knows' it).