For detailed discussions of the so-called Lucas-Penrose arguments, see :
and
Particularly relevant are the comments Gödel gave one of the prestigious Gibbs
Lectures at the American Mathematical Society in 1951.
Gödel claimed that what the Theorems do entail (specifically, the Second Theorem) is that mathematics is inexhaustible:
It is this theorem [i.e., the Second Theorem] which makes the incompletability of mathematics particularly evident. For, it makes it impossible that someone should set up a certain well-defined system of axioms
and rules and consistently make the following assertion about it: All
of these axioms and rules I perceive (with mathematical certitude) to
be correct, and moreover I believe that they contain all of mathematics.
If someone makes such a statement he contradicts himself.
In the Gibbs Lecture, thus, Gödel acknowledged that [his theorems] do
not rule out the existence of an algorithmic procedure (a computing machine, an automated theorem prover) equivalent to the mind in the relevant sense [...]. However, if such a procedure existed “we could never know with mathematical certainty that all the propositions it produce[d were] correct.” Consequently, it may well be the case that “the human mind (in the realm of pure mathematics) [is] equivalent to a finite machine that … is unable to understand completely its own functioning”: a machine too complex to analyze itself up to the point of
establishing the correctness of its own procedures. Gödel inferred that
what follows from the incompleteness results is, at most, a disjunctive
conclusion:
Either mathematics is incompletable in this sense, that its evident
axioms can never be comprised in a finite rule, that is to say, the
human mind (even within the real of pure mathematics) infinitely
surpasses the powers of any finite machine, or else there exist absolutely
unsolvable Diophantine problems of the type specified… It is
this mathematically established fact which seems to me of great philosophical
interest.
In other words, either the mind actually has a non-algorithmic and not
fully “mechanizable” nature, or else there exist absolutely undecidable
mathematical problems. But [Gödel's Theorems] don’t allow us to go further
and conclude that the true disjunct is the first one. According to Gödel,
then, what follows from [them], and especially from [the Second one], is that if our mind is a computing machine, it is one such that it “is unable to understand completely its own functioning.”
For further discussions, see :
and :
Comment
I do not agree on statements like :
there exists the Gödel sentence (saying that it is not provable in that system) which is unprovable in that system, but which the human mind can see to be true.
Let assume some "technical" facts regarding Gödel's Incompleteness Theorems :
Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F
The unprovable statement is built-up in such a way that :
F ⊢ G ↔ ¬ProvF(⌈G⌉)
and the proof amounts to : :
if F is consistent, then F ⊬ G,
ff F is 1-consistent [or other condition, strictly "stronger" than consistency], then F ⊬ ¬G.
Up to now, we have only a "syntactical" result, about provability in a (suitable) formal system.
In order to speak of truth, we have to add the "semantical" side [see : Daniel Isaacson, Sufficient conditions undecidability of the Gödel sentence and its truth (2007)].
Assuming that the system F is sound with respect to truth in the structure of the natural numbers (called N), we have that :
F ⊬ G, G is true, and F ⊬ ¬G.
Proof
Assume F ⊢ G; then ProvF(⌈G⌉) and, by the condition F ⊢ G ↔ ¬ProvF(⌈G⌉), we have that G is false. Then, by soundness of F (i.e. F proves only true sentences) : F ⊬ G, contradicting our assumption that F ⊢ G. Thus, by propositional logic : F ⊬ G.
Again by the condition F ⊢ G ↔ ¬ProvF(⌈G⌉), we have that ¬ProvF(⌈G⌉) is true. But G ↔ ¬ProvF(⌈G⌉), and thus G is true
Then ¬G is false; so, by soundness of F : F ⊬ ¬G.
Conclusion : it is not a question of "seeing the truth of ...". We have a strict mathematical proof of a conditional :
"if F is sound, then the Gödel's sentence G (for F) is true".
Thus, the mathematical proof regarding the truth of G relies on assumptions. The basic assumption of the above proof is the soundness of the system F with regards to the natural numbers : a condition that is stronger than consistency.
In fact :
soundness implies consistency, while consistency is strictly weaker than soundness.
There are theories that are consistent but unsound; a simple example is : F ∪ {¬G}.