# Is there actually a universal notion of computability?

A few weeks ago, I came upon this great post by JDH and it has been troubling me ever since. The TL;DR for the proof is that we can encode the outputs of any function into the axioms of a set theory so that we simply require a single Turing Machine capable of acting as a clever "parser" which can extract the information from the axioms and compute the desired function - this I understand (at least, conceptually and somewhat formally).

What confuses me though is the philosophical implications this has for conceptions of computability... I believed that there was, in some sense, a universal notion of computability (i.e. there were problems that either are or aren't decidable) but this suggests that such notions depend on the set-theoretic background for your computation - for example, this post by Scott Aaronson discusses the work of one of his students in showing that there is a specific Turing Machine whose behaviour is independent of ZFC (suggesting again, implicitly, that the behaviour is platonic but that we simply can't prove it either way).

Forgive me for my lack of well-definedness in my question but: Is there a way in which this can be resolved? Why are there seemingly uncomputable problems (whose proof of uncomputability often use proofs by contradiction seemingly without reference to any set-theoretic background, e.g. the Halting Problem) which can be computed by a Turing Machine, without the use (officially) of an oracle? Does this have any impact on the Church-Turing Thesis, as presumably no human could compute reliably the Busy Beaver function while the universal algorithm (if put in the right universe) can?