First, a correct version:
The mathematician Godel proved that a system of axioms can never be
based on itself: statements from outside the system must be used in
order to prove its consistency.
This makes good sense, since a consistent system T
subject to Gödel's theorem can't prove its own consistency (or,
equivalently, can't prove the so-called Gödel sentence for system T,
which for all the usual systems T is equivalent in T to "T is
consistent"). Thus, to prove the consistency of T it is necessary to
"step outside the system" T in the sense of "bring to bear some principle
not contained in T itself". It should be noted, however, that this
does not mean that the consistency of T can only be proved in a system
stronger than T. All that follows is that to prove the
consistency of T, some principle must be used which is not contained
in T itself.
Now an incorrect version:
Godel's theorem states that in any consistent system
which is strong enough to produce simple arithmetic there are formulae
which cannot be proved-in-the-system, but which we [standing outside
the system] can see to be true.
Let's take a closer look at this. The impression that "standing
outside the system" is all that is required to see the truth of the
Gödel sentence G for a theory T often arises, it seems, because of
the striking character of the last step in an argument that G is
true. Such an argument might go as follows:
We have shown that G is not provable in T, if T is consistent. But this is just what G states - that it is not provable in T! Thus we see, by stepping outside the system, that G is in fact true, although unprovable in T.Here we must note that the fact that G states that it is not provable in T is not something that requires "stepping outside the system" to see. On the contrary, it is essential to the proof of Gödel's theorem (as usually presented) that the equivalence
G holds if and only if G is not provable in Tis in fact provable in T itself. So in the observation that "this is just what G states" there is no "stepping outside the system". Next, we need to note that what G states is not exactly what we have proved in Gödel's theorem. What we have shown is that G is not provable in T if T is consistent. What G states is not this conditional statement, but the categorical statement "G is unprovable in T". We can't conclude that G is true from what we have shown, we can only conclude that G is true if T is consistent - and this, again, is provable in T itself (as shown in the proof of Gödel's second incompleteness theorem). When we say that we see G to be true, we are tacitly saying that we see T to be consistent, and this we do in some cases but not in others. It's a simple matter to find examples of T where we have no idea whether or not the Gödel sentence of T is true, since we have no idea whether or not T is consistent.
Thus the quoted statement "Godel's theorem states..." is quite simply false. Gödel's theorem does indeed establish that "stepping outside the system" is sometimes necessary to decide the truth or falsity of statements. It does not establish that we, standing outside the system, can decide the truth or falsity of the Gödel sentence, or of any other statement undecidable in the system.
On the net and elsewhere, one can one can expect to encounter many
startling claims about the implications of Gödel's theorem for the
powers of the human mind. The following has actually appeared in print:
Church's theorem states the existence of an absolutely undecidable
statement. This statement is produced by combining the Goedel
sentences of all formal systems together... Church took all those
unprovable statements and made one new statement from them, thereby
arriving at a statement which remains undecidable no matter what
formal systems we introduce. However, interestingly, even this
"Church-sentence" is decidable by humans: in fact it is pre-decided
through its contruction by Church. Church defined it so we can know:
this statement is actually true. We can demonstrate this truth but no
formal system can.
It's unclear exactly what the author has in mind, but there is not in
fact any such "Church sentence". What is usually called Church's
theorem states that there is no algorithm for determining whether
or not a sentence in the formalism of predicate logic is logically valid.
In such a case, Gödel's theorem has a striking positive aspect: it gives us a way of extending any mathematical theory all axioms of which are true to a stronger theory, which still satisfies the condition that all axioms are true. We can do this by adding to T as a new axiom the statement "T is consistent". This theory can then itself be extended in the same way, and so on. The "and so on" turns out to involve some mathematical technicalities when we pursue this line of thought, as is done in the logical literature dealing with series of theories obtained by repeatedly adding consistency statements or stronger so-called reflection principles to theories.