Notation:
Q - formal system(logical&nonlogical axioms, etc.) of robinsons
arithmetic
wff - well formed formula

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. (mathlogic is a formal system too)

In my opinion, some correct answer is to state thm 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 godels proof)

but I'm confused because I haven't found such statement(or
explanantion) anywhere.

Thank You Very Much