I understand [Godel's Incompleteness Theorems](http://en.wikipedia.org/wiki/G%25C3%25B6del%27s_incompleteness_theorems) to be statements *about* effectively generated [formal systems](http://en.wikipedia.org/wiki/Formal_system), 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](http://en.wikipedia.org/wiki/Formal_language) is used to express them, how do I [interpret](http://en.wikipedia.org/wiki/Interpretation_%28logic%29) 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](http://en.wikipedia.org/wiki/Zermelo%25E2%2580%2593Fraenkel_set_theory)", 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.



What axioms are used to prove Godel's Incompleteness Theorems?
As Andres Caicedo points out in his comment (to the Question), the modest fragment $\sf{PRA}$ (Primitive Recursive Arithmetic) of $\sf{PA}$ (Peano arithmetic) is already is able to verify the incompleteness theorems.



> 
> 
> > 
> > Indeed, the proof of the Gödel-Rosser incompleteness proof is entirely syntactic and can be readily implemented in a fragment of $\sf{PRA}$ known as $I\Delta\_0 + exp$, where $I\Delta\_0$ is the weakening of $PA$ in which the induction scheme is only available for $\Delta\_0$-formulas, and $exp$ asserts the totality of the exponential function $2^x$ (it is well-known that $I\Delta\_0$ is unable to prove the totality of the exponential function).
> > 
> > 
> > 
> 
> 
> 


It is worth noting that in the above $I\Delta\_0 + exp$ can be even reduced to $I\Delta\_0 + \Omega\_1$, where $\Omega\_1$ is the axiom asserting the totality of the function $2^{\left| x\right|^2 }$, where $\left| x\right|$ denotes the length of the binary expansion of $x$. The theory $I\Delta\_0 + \Omega\_1$ is commonly viewed as the weakest fragment of $\sf{PA}$ in which one can develop a workable "theory of syntax".


**PS.** As pointed out by Jeřábek, the incompleteness theorems can be implemented in even weaker systems. 


