Goedel's proof: a revisionist view
  This note presents a revised assessment of Goedel's proof. I show that the proof can be modified to establish that there exists a system P' such that: either P' is inconsistent (and P is also inconsistent) or P' is consistent and yet has no model. To define P' I firstly present a semantics for Goedel's P, and then define a theory P0 which is syntactically identical to P however the meaning of the type one variables differs in that for any interpretation of P0 these variables range over all and only the individuals assigned to the P0 numerals. P' is the theory obtained by adding the negation of a Goedel sentence for P0 to the proper axioms of P0. 
Stephen Boyce
math.GM