I understand Gödel's Incompleteness Theorems to be statements about effectively generated formal systems, which basically makes them theorems about algorithms. This is cool, because despite being very abstract, they actually constrain my expectations about how computers and human beings can behave. But, being theorems, what formal system are they theorems in? That is, what formal language is used to express them, how do I interpret that language as being about algorithms, what axioms are assumed, and what rules of inference are used to derive the incompleteness theorems?

I ask because I am looking for a better answer than "ZFC", which has been given to me in person a few times now. ZFC refers to all sorts of things I don't believe exist (e.g. non recursively enumerable sets, choice functions for uncountable families…), at least not in the same way I believe in concrete things like computers and algorithms. I can see from skimming the proofs that I could probably make up a formal system in which the theorems could be expressed and proven, which did not refer to all the monstrosities of ZFC. I just want to know what standard, "simplest" formal system(s) can be used for this purpose.