Gödel's Incompleness Theorems and the "Minds vs. Machines" conundrum As a part of my self-learning about Gödel's Incompleness Theorems, I try to dive a little bit into their different interpretations and (possible) philosophical implications. One that immediately catches the eye relates to artifical intelligence. It seems like some people believe Gödel's theorems indicate that the mind is somehow transcendent to machines. As J. R. Lucas, puts it in his book (which I did not read) "Minds, Machines and Gödel": there is "some elusive and ineffable quality to human intelligence, which makes it unattainable by machines".
In short, Lucas' argument goes as follows:

However complicated a machine we construct, it will, if it is a machine, correspond to a formal system, which in turn will be liable to the Gödel procedure for finding a formula unprovable-in-that- system. This formula the machine will be unable to produce as true, although a mind can see that it is true. And so the machine will not be an adequate model of the mind.

Following this line of reasoning, it seems like the "elusive quality" Lucas mentions lies not within human consciousness, feelings or imagination but rather within the short textbook-proof that Gödel's sentence is true.
To me that sounds quite ridiculous (as you might have guessed). However, when I do try to point out exactly where Lucas' argument breaks down, I mainly get confused. So I'd appriciate your help with clearing things up.
It seems like the key here is to carefully follow the mathematical details of that textbook proof and try to see what's so "human" about it and why. Recall that given an arithmetical formal system $S$, its Godel sentence $G$ satisfies $S\vdash G\leftrightarrow \neg{\rm Prov}(\left\lceil G \right\rceil )$, where $${\rm Prov}(\left\lceil \varphi \right\rceil):=\exists x ({\rm Prf} (x, \left\lceil \varphi \right\rceil))$$ is the "provability" formula (and $\left\lceil \cdot \right\rceil$ means Gödel numbering).
Now, the textbook proof goes like this. In the proof of Gödel's first incompleteness theorem it is shown that if $S$ is consistent then it cannot prove $G$. Therefore, in that case, for every natural $n\in\mathbb{N}$, $\neg {\rm Prf} (n, \left\lceil G \right\rceil)$ is true (in the standard model $\mathbb{N}$). Thus $\forall x(\neg {\rm Prf} (x, \left\lceil G \right\rceil))$ is true (in $\mathbb N$) which is exactly $\neg{\rm Prov}(\left\lceil G \right\rceil )$. But it is known to be equivalent to $G$ by definition. Therefore $G$ is true.
How much of that does $S$ "know" (able to prove)? As shown in the proof of the second theorem, the system $S$ knows that if it is consistent it cannot prove $G$. It can also be shown that $S$ knows, for every $n\in \mathbb{N}$, that $\neg {\rm Prf} (n, \left\lceil G \right\rceil)$. So it seems like the only thing that $S$ is missing is the knowledge that if $\psi(n)$ is true for every $n\in\mathbb{N}$ then $\forall x (\psi(x))$ is true. This is where I get confused:

*

*I was able to say "true in the standard model $\mathbb{N}$" but $S$ doesn't have that privilege; when it asserts that something is true, it has to be the case in all of its models (which might be non-standard). Wouldn't that be an "unfair advantage" that I have?

*If "concluding that $\forall x (A(x))$ from $A(n)$ for every $n\in\mathbb{N}$ "is really the thing that seperates my mind from $S$ (regarding the truth of $G$), what is it about my human mind that causes that? What's so "human" here?

*I know that $G$ is true only assuming that I know $S$ is consistent. So maybe Lucas' argument doesn't prove that the human mind transcends all machines, but only those it "knows" their consistence. In that case, the human mind might still reducable to a formal system, but simply one we will never be aware of its consistence. Perhaps that's where the Lucas' argument fails?

 A: First, I want to commend you on not dismissing Lucas' argument simply because the conclusion seems outlandish (this is what many people do: "Oh, so Lucas must be thinking that there is something about the human mind that cannot be captured by any formal system, but since by Lucas' own admission we can correspond a formal system with any physical system, that would mean that there is something about the human mind that is non-physical, and hence Lucas must be some weird dualist who believes that the human mind must have some 'soul-like' aspect to it that is non-physical. Well, Pffhbt to that!").  Sure, Lucas' argument may have an (to many people) unpalatable conclusion to it, but you are doing the right thing in demanding to know where the argument goes wrong if indeed it is wrong.
OK, so on that, a couple of comments:
Lucas writes:

However complicated a machine we construct, it will, if it is a machine, correspond to a formal system which in turn will be liable to the Gödel procedure for finding a formula unprovable-in-that- system.

Well, I would say Lucas needs to be very careful here, as there are a number of issues to be resolved:
First, I would say that Lucas is really glossing over a few things here. There is a big difference between something being a machine and something being a formal system for proving theorems. I can see how the human body and brain can be regarded as a 'machine' (a 'meat machine'), and how any machine can be an implementation of some formal system, i.e. how it realizes some computation.  However, any physical system can be implementing many kinds of computations all at the same time, simply depending on what level of abstraction you take. Moreover, computations are not the same thing as formal-systems-for-proving-theorems: even if I had some artificial neural network, whose mechanisms can be fully described computationally, it is still far from clear how that network would actually be used to prove theorems. In sum, even if we had a full description of how our brain works in terms of physical/chemical processes, it is far from clear how that would tell us what the proving abilities are as implemented by that physical system: that is a huge gap.
Second, it isn't even clear that a description of just the workings of our brain alone is sufficient to tell me what my formal abilities are. For example, I use pen and paper to solve any complex mathematical problems; do you think we can solve those just in our heads with our naked brain?!  In other words, the physical 'machine' that implements my abilities to prove theorems is likely to be a highly complex system that involves not just our brains, but also our hands, our eyeballs, and our environment that contains pens, paper, and, most importantly, handy dandy linguistic symbol systems.  This makes the translation from such a physical system to what we can prove even more difficult.
Then again, maybe it doesn't make it more difficult at all! If our abilities to prove theorems relies inherently on the very external formal/symbolic/linguistic systems that as a community of mathematicians and logicians we have created over time, then our abilities to prove mathematical theorems might be likewise limited by those very formal systems. So, whatever incompleteness results hold true for those formal systems would therefore automatically be true of our own abilities as well. Indeed, many mathematicians believe that we are 'working within ZFC', i.e. that all of human proving abilities can, in theory, be formalied by the ZFC system. But if ZFC is consistent, then that means that there is a Godel sentence for it that it cannot prove ... but that we would therefore not be able to prove either.
OK, but let's suppose that we can somehow got a full description of the formal system through which we prove theorems.  Lucas claims that we can then use Godel's procedure to point to a claim that we know is true, but that is not provable in that system ... and hence we cannot be that system:
Again, Lucas glosses over a number of serious potential pitfalls here:
As you yourself point out in point 3 of your post: Such a Godel sentence only exists for consistent systems, and so we would first need to know that the formal system that we are looking at is consistent. Well, that is again far from easy.  I already was pointing out that this could well be a super complicated system if it is indeed one that is implemented by the neural networks in our brain. And, from computability theory, we know that there are some very simple machines whose halting behavior is unknown (e.g. see the holdouts in the Busy Beaver problem), and if the system's ability to prove theorems is dependent on the halting behavior of its subsystems, I don't think there is a snowball's chance in hell for us to tell whether that system is consistent. And without that knowledge, we cannot say that there is something that that system cannot prove. And again, let's point to ZFC here here: compared to a neural networks involving trillions of connections, the consistency properties of ZFC should be child's play to analyze ... but we don't know if ZFC is in fact consistent ... and again, if that's the system that can capture all our proving abilities, then we will never be able to prove its consistency, by Godel's second Incompleteness theorem.
And finally, all of this is assuming that the system we are looking at is in fact consistent ... it may well be inconsistent, in which case Lucas' argument fails immediately.  And frankly, I don't believe humans are very consistent ... at least not individual ones. As a community, we can at least try to make sure that everything we do will still conform to the formal systems as laid out by something like ZFC (or at least the 'laws' of logic and math), so it isn't like we suddenly start proving that 1+1=3 either :)
