alt Hacker News>You can compute a number that is equal to BB(n), but you can't prove that it is the right number you are looking for.
You can't categorically declare that something is unprovable. You can simply state that within some formal theory a proposition is independent, but you can't state that a proposition is independent of all possibly formal theories.
Replies
IsTom • yesterday at 9:41 PM
It's not that there "exists n, such that for all theories", but that "for all theories there exists n", that BB(n) will get independent eventually.
They didn't claim that. They claimed that any (sound and consistent) finitely axiomatizable theory (basically, any recursively enumerable set of theorems) can only prove finitely many theorems of the form BB(n) = N.