#
Notation:
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

Read another response by Peter Smith, Richard Heck

Read another response about Logic