I understand [Godel's Incompleteness Theorems][1] to be statements *about* effectively generated [formal systems][2], 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][3] is used to express them, how to I [interpret][4] 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][5]", which has been given to be 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.

Thanks!


  [1]: http://en.wikipedia.org/wiki/G%25C3%25B6del's_incompleteness_theorems
  [2]: http://en.wikipedia.org/wiki/Formal_system
  [3]: http://en.wikipedia.org/wiki/Formal_language
  [4]: http://en.wikipedia.org/wiki/Interpretation_(logic)
  [5]: http://en.wikipedia.org/wiki/Zermelo%25E2%2580%2593Fraenkel_set_theory