[lupire]

Why would Aleph* be necessary or relevant?

ZFC and larger theories are only relevant for infinite objects, not finite objects like BB.

[srcreigh]

I don’t have the understanding, but apparently there are finitary statements which are independent of ZFC. This has been used to prove that BB(745) is independent of ZFC.

https://mathoverflow.net/a/26605

Furthermore, Scott aaronson jokingly conjectured that even BB(20) is independent of ZFC. That’s my reference here where we end up needing Aleph* for BB(18).