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.
