Skip to main content
3 of 7
added 237 characters in body
Ali Enayat
  • 17.7k
  • 2
  • 63
  • 105

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^{2\left| x\right| }$, 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. There are (a) other equivalent formulations of $\Omega_1$; and (b) weaker systems than $I\Delta_0 + \Omega_1$ within which the incompleteness theorems can be implemented. See the comments by Goldstern and Jeřábek below.

Ali Enayat
  • 17.7k
  • 2
  • 63
  • 105