I understand Godel'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.

Handbook of Mathematical Logic, by Smorynski, has the details. Look for the term "formalized incompleteness theorem". $\endgroup$ – Carl Mummert Jan 6 '13 at 23:21