Q:

Does Gödel's argument that minds are more powerful than computers have the inconsistency loophole?

In "Raatikainen, P., 2005, “On the Philosophical Relevance of Gödel's Incompleteness Theorems,” , the author argues that Penrose's and others use of Gödel's theorem as an argument against mechanism (and presumably strong AI) - that minds are more powerful than computers because of human's ability to recognize the truth of Gödel sentences - are all flawed. 

The basic error of such an argument is actually rather simply pointed out. The argument
  assumes that for any formalized system, or a finite machine, 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. Yet Gödel’s theorem has in reality
  the conditional form, and the alleged truth of the Gödel sentence of a system depends on
  the assumption of the consistency of the system. That is, all that Gödel’s theorem allows
  us humans to prove with mathematical certainty, of an arbitrary given formalized theory
  F, is:
  F is consistent -> GF.

What he is saying here is that there is no guarantee that a formal system realized by a computer is consistent. Hence there's no guarantee that the Gödel sentences that humans recognize but computers don't are indeed themselves true, and human's aren't necessarily pulling off anything that a computer can't do. 
My questions: 

How could we possibly construct a computer that isn't consistent? It seems to me that any computer we build would be based on Turing Machines, which are themselves limited by Gödel theorem (via the halting problem). 
Can a Turing machine generate an inconsistent formal system? Isn't anything generated by a Turing consistent by definition, since it's rules are contained in the Turing machine's memory?  
And if this is the case, that Turing Machines can only generate consistent systems, then is Raatikainen's refutation of Penrose's and similar arguments false?  

A:

For detailed discussions of the so-called Lucas-Penrose arguments, see :

Torkel Franzén, Gödel's theorem : An incomplete guide to its use and abuse (2005), Ch.6 Gödel, Minds, and Computers, page 115-on 

and 

Francesco Berto, There's Something about Gödel : The Complete Guide to the Incompleteness Theorem (2009), Ch.11 Mind versus Computer: Gödel and Artificial Intelligence, page 174-on.

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 :

Solomon Feferman, Gödel, Nagel, minds and machines

and :

Stewart Shapiro, Incompleteness, mechanism, and optimism.

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}.

A:

We can construct a computer that implements an inconsistent formal theory to which Gödel theorem does not apply just like we can construct a computer that implements Peano arithmetic. A simple example is Meyer's relevant arithmetic R# that allows some contradictions, but uses paraconsistent logic (without the law of explosion) to limit their effect. In R# Meyer was able to prove by finitary means that arithmetical calculations never produce contradictory results despite the presence of more abstract contradictions, not quite what Hilbert wanted, but more than consistent Peano arithmetic allows. Recently McKubre-Jordens and Weber extended R# to inconsistent analysis, there are other interesting inconsistent formal theories that can be implemented just like consistent ones.
However, one does not need inconsistency to question Gödelian arguments. Human "superpower" to recognize the truth of Gödel sentences derives from the non-mystical fact that they are provable in meta-theory, e.g. Gödel sentence for Peano arithmetic is provable in second order arithmetic. Of course, any effective proof theory for second order arithmetic will have its own Gödel sentence, provable in the next one, etc., and none of them can prove them all. But neither can any human. Constructing a Gödel sentence for an effectively axiomatized theory is also a perfectly algorithmic process (after Gödel). 
So what this comes down to is the historically attested human ability to find new axioms and new forms of reasoning that were not formalized in advance. As humans "find" them however they disagree about their truth and validity. According to humans called intuitionists, Gödel sentences are not true (or false), and neither is the axiom of choice or even the law of excluded middle. The parallel postulate is only "approximately true" these days. "True" axioms are not so much "recognized" as picked up and adopted because they come handy. But why can't a fancy AI attached to a random number generator and with robotic parts to interact with "reality" do the same? There are already computer programs that generate conjectures, like Graffitti, and something like Prolog can already be used to find proofs for them too. Neural networks, simulated on computers, can "induce" new patterns by "learning", what's to stop them from "inducing" the parallel postulate?
What Gödelian arguments demonstrated so far is that their authors make presuppositions that imply their conclusions without any mediation from Gödel. We might as well say it straight: "history shows that humans can do what no computer can do in principle". Either you believe it or you don't, no theorem can prove or disprove it.
Franzen's Gödel's Theorem: An Incomplete Guide to Its Use and Abuse is a canonical reference for dispelling the mythology surrounding Gödel's result.

A:

Inconsistent systems are trivial to develop.  The issue regarding inconsistent systems and strong AIs is that it is difficult for us to make a proof statement to prove that any specific AI is "strong," by whatever metric we choose.  Mathematical consistency is important for all of our existing proving systems.
Accordingly, if the AI was developed using an inconsistent system, we have few tools available to intentionally make it "strong."
Making an inconsistent system is trivial.  Simply create rules which conflict.  For example, in programming, there is a very real issue that arises during the end of a process regarding reachable memory. Many languages (java, python, C#, to name a few, plus C++'s shared_ptr) have objects that give lifespan guarantees: as long as you hold a reference to the object, it has to stay around.  However, you can come across situations where object A refers to object B and object B refers to object A -- a "reference cycle."  If neither object stops referring to the other, they are provably eternal.
At least, they're eternal until the end of a process comes along, which came with its own consistency guarantees: "Processes can be terminated in a finite period of time" and "processes free all of their memory when they are terminated."  So we have to break our own rule.  There's a period of time at the end of a process where you can't guarantee that you're still pointing at something that's alive.  In C++ in particular, this can result in situations that crash because you were promised one invariant (this object will outlive me), while another invariant conflicted (the process ended).
If you needed to adapt it into a Turing machine, simply seek to implement a Turing machine within a system which cannot actually implement all Turing machines "perfectly."  The system is inconsistent, because it claims to be a Turing machine, while axioms defining the implementation contradict these claims.

