Q : formal system (logical & nonlogical axioms, etc.) of Robinson's arithmetic;
wff : well formed formula;
|- : proves.
G1IT is always stated in the form:
If Q is consistent then exists wff x: ¬(Q |- x) & ¬(Q |- ¬x)
but we cannot prove it within Q (simply because there is no deduction rule to say "Q doesn't prove" (there is only modus ponens and generalization)), so it's incomplete statement, I don't see WHERE (in which formal system) IS IT STATED. (Math logic is a formal system too.)
In my opinion, some correct answer is to state the theorem within a copy of Q:
Q |- Con(O) |- exists x ((x is wff of O) & ¬(O |- x) & ¬(O |- ¬x))
where O is a copy of Q inside Q, e.g. ¬(O |- x) is an arithmetic formula of Q, Con(O) means contradiction isn't provable...such formulas can be constructed (see Godel's proof).
But I'm confused because I haven't found such statement (or explanation) anywhere.
Thank You Very Much
One thing the questioner seems to want to know is in what kinds of theories the first incompleteness theorem can itself be proved. As Peter says, the proof of the theorem is fine given informally, as almost all actual mathematical results are. But still, one might want to know: Where is this theorem provable? The answer is: Not in Q, but in fairly weak theories. It can certainly be proven in PA---full Peano arithmetic---though that hardly counts as a "weak" theory. I am fairly certain, though, that it can be proven in the theory known as "I-Sigma-1"---though I'd have to check that before betting my life on it. Part of the reason I'm sure about this, though, is that I-Sigma-1 is susceptible to the second incompleteness theorem. What you get in such cases is (e.g.) that PA |- Con(PA) --> G PA ; but then, if PA |- Con(PA), then PA |- G PA , and PA is inconsistent, by the first incompleteness theorem, and this works for any theory T that extends Q and is capable of proving: Con(T) --> G T . ...