But imagine that we could compute BB(n) for any n, even if we need to use a different algorithm for each n. Then, we could build the mapping n -> BB(n). But the existence of this mapping is forbidden by the unsolvability of the Halting Problem, isn't it?
No you can't conclude this and in fact the more general principle is that being able to prove P(0), P(1), P(2), etc... does not mean that it's also possible to prove P(n) for all n. The property of a formal system for which this does follow is known as Omega completeness, but Peano arithmetic and ZFC more broadly are both Omega-incomplete systems, hence there are propositions for which P(0), P(1), P(2)... can all individually be proven and yet it is not possible to prove P(n) for all n.
Wikipedia touches on this subject with an article on omega-consistent systems, which is a very closely related property:
> But imagine that we could compute BB(n) for any n, even if we need to use a different algorithm for each n.
This is itself uncomputable; therefore
> Then, we could build the mapping n -> BB(n).
This mapping is not computable.
Edit as I'm rate-limited:
What I mean is, informally, the incomputability of the algorithm to select the correct algorithm to compute BB(n) is sufficient to make that mapping uncomputable.
However, that does not mean that an algorithm to compute BB(n) for a specific n does not exist. Trivially, it does; "output BB(n)". It's just very uninteresting! What you're asking for, rather, is more like "an algorithm to prove BB(n)=x", which is a closely related but distinct problem.
