  Now Gödel’s first incompleteness theorem (G1) states that for any sufficiently strong, consistent formal theory \(S\) there is a sentence \(G_S\) which is true but not derivable in \(S\). \(G_S\) is a real sentence according to Smorynski’s definition. Now consider a theory \(T\) which formalizes ideal mathematics and its subtheory \(S\) which formalizes real mathematics. \(S\) satisfies the conditions of G1 and hence \(S\) does not derive \(G_S\). Yet, \(T\), being a formalization of all of mathematics (including what is required to see that \(G_S\) is true), does derive \(G_S\). Hence, we have a real statement which is provable in ideal mathematics and not in real mathematics.