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. For any fixed set of axioms you'll eventually run into BB(n) too big that gets indepentent.

▲

Kranar 3 days ago | parent [-]

>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.

▲

tromp 3 days ago | parent | next [-]

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.

▲

Kranar 3 days ago | parent [-]

I quoted the specific statement that I refuted.

	▲	IsTom 3 days ago \| parent [-]
		Only if your goalpost of what "mathematics" is endlessly shifting. To prove values of BB(50000) you're probably going to need some pretty wacky axioms in your system. With BB(any large number) that's just going to be unfeasible to justify that the system isn't tailored to prove that fact, just short of adding axiom of "BB(x) = y".

▲

IsTom 3 days ago | parent | prev [-]

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.