### "Stepping outside the system" is not enough.

There are two main types of references to stepping or standing "outside the system" in connection with Gödel's theorem, one of which is correct and the other incorrect. These two categories will be illustrated by two quotations.

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 T
is 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.

### The case when we know that the axioms are true.

That we don't in general know of any way of deciding G by stepping outside the system is obscured by the fact that Gödel's theorem is most often illustrated using such theories as PA (Peano arithmetic, a formalization of elementary arithmetic), where we can easily see that the theory is consistent (and hence its Gödel sentence true), because we can see by inspection that the axioms of the theory, and hence all of its logical consequences, are true.

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.