Because the byline wasn't easy to find on the device I read it on, and the possibility that someone might be offended by gender neutrality seemed far-fetched at the time.
> The author has the first name "John Carlos". Why not take an educated guess and use (gasp) gendered pronouns?
Because the text of the article could have been generated by a Turing machine with the pseudonym "John Carlos". And on the internet, nobody knows if you're a man, woman, dog, or sufficiently complicated state machine.
tl;dr: Non-gendered pronouns are inclusive and never inappropriate on the internet.
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?
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).
> 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.
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.
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".
You might look at Believing The Axioms (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).
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.
If you're refering to Yedidia and Aaronson's machine, the machine searches for counterexamples in ZFC. We believe, but cannot prove, that ZFC is consistent. Also, we can prove that assuming ZFC is consistent, ZFC cannot prove that ZFC is consistent. Hence, since we believe ZFC is consistent, we believe that the machine will not halt, but we can't prove it. This implies that BB(7910) cannot be computed.
But ZFC isn't the only system in town. It's possible (although highly unlikely) that we could prove its value in another system that we can see to be just as valid as ZFC. (Like adding consistency axioms and so on.)
Yeah, sure, if we agree to do math in the system ZFC+Con(ZFC) we can prove that Yedidia's machine does not halt. But then we can just construct another machine (call it M', a n'-state turing machine) that searches for contradictions in ZFC+Con(ZFC), and now we believe that M' does not halt, but we can't prove it; and now, BB(n') can't be computed.
Sure, but no matter what model of math we choose to work in, I can come up with some n such that I can say "...hence, BB(n) cannot be computed", and you cannot reply "BB(n) can be computed; it's just a finite number. What you mean is the value can't be proven correct..."
> If you're choosing a specific model of math, you need to specify that in your statement.
I mean, in my most recent statement I quantified over all consistent models...
> It will still be computable within that model, just not provably so within that model.
OK, now I'm confused; what is the specific definition of "computable number" you're using?
Also, informally speaking, say we're both working in ZFC. You claim that BB(7910) is computable. What does that mean? Does it mean you can write down its value as a normal decimal number?
>I mean, in my most recent statement I quantified over all consistent models...
Not quite, as I pointed out in https://news.ycombinator.com/item?id=11753020. You can easily have a consistent system that proves the value of all BB numbers, it just won't be computable.
If you restrict us to computable consistent systems, then for any given model there will be some value of BB it doesn't prove, but also for any given value of BB there will be some consistent model that proves it. There's nothing in particular added about knowability by Aaronson's et al result, only about provability.
>OK, now I'm confused; what is the specific definition of "computable number" you're using?
Any finite number is computable, we just can't prove that a specific machine is the one that computes BB(N). We can prove that some machine in a finite set (all TMs of size N we haven't seen to halt or proven nonhalting) computes it, but we can't pin down which one, within that model.
>Also, informally speaking, say we're both working in ZFC. You claim that BB(7910) is computable. What does that mean? Does it mean you can write down its value as a normal decimal number?
Lol nope. We can't even write down anything above BB(6). BB(7) has more digits than atoms in the observable universe.
My claim that BB(7910) is computable means there's a Turing machine that computes it. That's easy to prove, as any finite integer can be computed by a Turing machine.
There's no Turing machine that computes every BB number sequentially, though.
Belief has nothing to do with it. I can believe ZFC is inconsistent and the world will not change a bit.
You can't prove me wrong. (It's almost a religious argument)
If I believe the inconsistency of ZFC then I believe the machine must halt. I can't ever observe it since I can't know the number of steps needed. There's almost a paradox but not quite.
No, if ZFC is inconsistent, then you can know the number of steps needed. Every statement, true or false, is derivable from ZFC if it is inconsistent. If there's contradiction in ZFC, it can be found in finite time by enumerating all the theorems.
I'm trying to get an intuition about why this whole game can even be played, and it's proving (ha) rather tricky. I'm ok with the idea that things sometimes cross into the realm of the impossible when transitioning from discrete/finite to continuous/infinite, or maybe from countably to uncountably infinite, but the notion that there's some constant threshold seems so counterintuitive. The link at the end of the article is pretty good [1] as is wikipedia [2], but I'm clearly missing some intuition here. Help!
You can't solve the halting problem. Therefore, if you take a program that takes a Turing machine as input, searches for a proof in ZFC (or your favorite alternative) that the program halts or that it doesn't, and if it doesn't find a proof either way then it runs forever, your program is not a halting solver.
Therefore, there are some Turing machines which can't be proven to halt or run forever in any given consistent system that can be computed.
(Because if every TM had a proof, then the program above would solve the unsolvable halting problem).
Therefore, there is a smallest such program that's independent of ZFC.
we give a 7,918-state Turing machine, called Z
(and actually explicitly listed in our paper!),
such that:
Z runs forever, assuming the consistency of a large-cardinal
theory called SRP (Stationary Ramsey Property), but
Z can’t be proved to run forever in ZFC [...],
assuming that ZFC is consistent.
edit: Just saw that this was linked at the bottom of the article. As pohl mentioned, the article really buried the lede.
Therefore, there are some Turing machines which can't be
proven to halt or run forever in any given consistent
system that can be computed.
I feel like it's worth clarifying the quantifiers here. For all consistent systems, there exist Turing machines whose halting behavior can't be proven in that system. Unless I have some disastrous misunderstanding...
Well a consistent system that can't be computed can prove things about all Turing machines.
E.g. ZFC plus an infinite set of axioms of the sort "machine X halts" for all machines that halt. We can't compute all the axioms, but the system is perfectly consistent. We could compute the axioms if we had a halting Oracle.
It wouldn't be able to prove the halting behavior of some Turing machines that have halting oracles attached, though.
> searches for a proof in ZFC (or your favorite alternative)
is tripping me up though. It's not obvious to me that you can do this in an automated fashion. I assume this is a standard tool for theorists though? How does such a program work?
The idea is that proof systems can be formulated as a grammar for a recursively enumerable language (Type 0 grammars in the Chomsky hierarchy): https://en.wikipedia.org/wiki/Chomsky_hierarchy#Summary, such that if there is a proof of a particular statement a corresponding word can be derived by the corresponding grammar.
But this can easily be done by a Turing machine (either check through all possible derivations in the grammar or, more abstract, let the Turing machine let non-deterministically choose a possible derivation and use the fact that the expressiveness of non-deterministic Turing machines is the same as for deterministic Turing machines).
May I ask if you are able to visualize things using your mind's eye at at what levels (size, detail, color/brightness)? Just curious about correlation with the subject matter.
I'm confused by the winning TM given for BB(2). It has 3 non-halt states, but N==2 should be a TM with 2, shouldn't it?
Did they merely put the illustration for BB(3) in the wrong place?
Edit: yeah, looks like they just put the illustration for BB(3) in the wrong place: https://en.wikipedia.org/wiki/Turing_machine#/media/File:Sta...