The Lucas argument vs the theorem-provers -- who wins and why?

In his paper, "Minds, Machines and Gödel", J.R. Lucas writes the following:

Gödel's theorem [First Incompleteness Theorem, that is—my comment] must apply to cybernetic machines, because it is of the essence of being a machine, that it should be a concrete instantiation of a formal system. It follows that given any machine which is consistent and capable of doing simple arithmetic, there is a formula which it is incapable of producing as being true—i.e., the formula is unprovable-in-the-system—but which we can see to be true. It follows that no machine can be a complete or adequate model of the mind, that minds are essentially different from machines.

Contrariwise, the following papers,

Wilfrid Sieg and Clinton Field, "Automated search for Gödel's Proofs", Annals of Pure and Applied Logic 133 (2005) 319-338 (MSN)

Lawrence C. Paulson, "A Mechanized Proof of Gödel's Incompleteness Theorems using Nominal Isabelle" (published

suggest that computers can not only show that the Gödel sentence is not provable from ZF − Infinity, but can also show that it is true, provided ZF − Infinity is consistent.

Why this is important is because Lucas, in the paragraph I quoted, makes the mistake that we as humans 'see' that the Gödel sentence is true. In point of fact, we actually infer the truth of the Gödel sentence much as a theorem-prover might infer its truth (if in fact the theorem-prover (via its respective metatheory) can infer the truth of the Gödel sentence, assuming ZF − Infinity is consistent).

So that is the question before us: Can computers that run theorem-proving software infer that that the Gödel sentence is true (note that Sieg and Field, as well as Paulson, use ZF − Infinity rather than PA as the object-theory for their theorem-proving software).

• Since PA+CON(PA)$\vdash$G (the Gödel sentence), humans start by assuming PA is true and therefore consistent, so they infer that G is true. That is, humans use CON(PA) in their inference, rather than PA alone. It's unsurprising that adding this independent postulate lets them prove things that PA can't prove by itself.
– none
Jun 28, 2019 at 10:04
• PA itself can prove Gödel's incompleteness theorem for PA, which itself is an implication that Con(PA) implies that its Gödel in unprovable. What it can't do (if it is consistent) is prove the the hypothesis of that conditional. The fact that automatic theorem provers can prove Gödel's theorem doesn't by itself say that such theorem provers go beyond what can be proved in PA. I'm not a great fan of Lucas's argument, but I don't think that these papers by themselves are particularly relevant. Jun 28, 2019 at 13:07
• This (from Lucas) is nonsense and based on a misunderstanding of Goedel's theorems. What does it mean to say that a person can 'see a statement is true'? If it should mean anything, it means we have some way to demonstrate it is true. But a computer can generate any proof a human can generate; and if the proof is correct then a computer can check it as well as a human. (Both of these are true in principle, in practice it remains the case that a human can generate interesting proofs vastly faster than a computer and can also check much more easily). Jun 28, 2019 at 14:56
• @SylvainJULIEN: If you take a look at Penrose's earlier book, The Emporer's New Mind, I think you will find that book reference's Lucas' Argument explicitly. Jun 28, 2019 at 15:28
• @user76284 I don't think we can really claim to recognise any serious set of axioms as consistent. Peano, for example - I believe this is consistent, but I don't have any evidence. I don't see how this is stronger than a computer printing out 'I think PA is consistent'. Sure, you can point to physical reality which seems to obey PA (and be consistent), but this only tells you anything about small numbers. I think that all I'm doing when I say I believe PA is consistent is extrapolating hopefully from my experience; this is not a proof. Jul 5, 2019 at 8:58

Yes, computers can infer that the Gödel sentence is true. This is performed in a meta-theory which is stronger than the object theory, as it has to be.

For example, Russell O'Connor formalized Gödel's incompleteness theorems in Coq. As he points out in Section 7.1, Coq can prove that the natural numbers form a model of Peano arithmetic $$PA$$. I cannot find in his formalization an explicit statement that Gödel's sentence is true (which is not to say it isn't there), but I am quite confident that it would take little effort to formalize such a statement.

[This paragraphs has been made obsolete as the question was edited to address the issue.] Also, let me point out that you might be confusing meta-theory with object-theory. Paulson uses the meta theory called "Nominal Isabelle" to prove Gödel's incompleteness theorem, but the way you phrased your question sounds as if you think Paulson's mechanised proof is carried out in $$ZF$$ without infinity.

Lastly, I would just like to say that I never understood how one could hold the position that ugly bags of mostly water are superior to machines in their ability to understand and create mathematics. A machine is not subject to uncontrollable chemical processes, fatigue, emotions, and temptations to sacrifice just a little bit of truth for a great deal of fame.

• What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics? Jun 27, 2019 at 22:41
• "ugly bags of mostly water are superior to machines in their ability to understand and create mathematics" Well, aren't we machines too? As to uncontrollable chemical processes, take a glass of water and spill it first on yourself and then on your computer. Who will emerge in a better shape? Everything has its advantages and disadvantages compared to everything else. The question is not which technology is superior but how to combine the two in the most efficient way ;-) Jun 28, 2019 at 0:53
• Did I say that machines were superior? I said I don't understood an ugly bag of mostly water when it says it is superior to machines. Jun 28, 2019 at 8:41
• A machine may be very good at creating mathematics, but -- like a philosophical zombie or a Chinese room -- I don't see any reason to believe that it is capable of understanding it. Jun 28, 2019 at 14:09
• Can an admin please kick off the bots, they're hogging this discussion thread with irrelevant stuff. Thanks! Jul 6, 2019 at 13:59

One can try to rescue Lucas's reasoning by arguing that humans can see the consistency of ZF - Infinity (or any other formal system under consideration) by mathematical intuition, and then infer the Godel sentence by logic. The difference between the human mind and the computer is then taken to be this mathematical intuition, rather than the logic that follows it. I think Penrose has given this version.

This argument is problematic because humans clearly do not just look at a formal system and see whether it is consistent (except for very simple ones, perhaps). Instead we guess the consistency of sets of axioms by using various heuristics, mathematical experience, analogies to the physical world.... We could also equip the computer with a set of heuristics for guessing the consistency of formal systems. The only downside to this would be that the heuristics would likely get some things wrong and therefore output a false answer to some mathematical queries (thereby evading Godel/Turing problems).

But this is no big deal as humans also make mistakes. In particular, top mathematicians have made serious errors about the consistency of formal systems, most famously Frege writing an entire book in a formal system to Russell's paradox. Some mathematicians have even doubted the consistency of Peano arithmetic - either a few great mathematicians are wrong about this question, or almost all of them are.

So there does not seem to be any real difference between humans and machines on this point.

I believe this argument is essentially the same as one given by Turing in his paper Computing Machinery and Intelligence (where he also introduced the Turing test), 9 years before Lucas.

The result in question refers to a type of machine which is essentially a digital computer with an infinite capacity. It states that there are certain things that such a machine cannot do. If it is rigged up to give answers to questions as in the imitation game, there will be some questions to which it will either give a wrong answer, or fail to give an answer at all however much time is allowed for a reply. [ ..... ] This is the mathematical result: it is argued that it proves a disability of machines to which the human intellect is not subject.

The short answer to this argument is that although it is established that there are limitations to the powers of any particular machine, it has only been stated, without any sort of proof, that no such limitations apply to the human intellect. But I do not think this view can be dismissed quite so lightly. Whenever one of these machines is asked the appropriate critical question, and gives a definite answer, we know that this answer must be wrong, and this gives us a certain feeling of superiority. Is this feeling illusory? It is no doubt quite genuine, but I do not think too much importance should be attached to it. We too often give wrong answers to questions ourselves to be justified in being very pleased at such evidence of fallibility on the part of the machines. Further, our superiority can only be felt on such an occasion in relation to the one machine over which we have scored our petty triumph. There would be no question of triumphing simultaneously over all machines. In short, then, there might be men cleverer than any given machine, but then again there might be other machines cleverer again, and so on.

Lucas's article responds to Turing's:

He argues that the limitation to the powers of a machine do not amount to anything much. Although each individual machine is incapable of getting the right answer to some questions, after all each individual human being is fallible also: and in any case "our superiority can only be felt on such an occasion in relation to the one machine over which we have scored our petty triumph. There would be no question of triumphing simultaneously over all machines." But this is not the point. We are not discussing whether machines or minds are superior, but whether they are the same. In some respect machines are undoubtedly superior to human minds; and the question on which they are stumped is admittedly, a rather niggling, even trivial, question. But it is enough, enough to show that the machine is not the same as a mind. True, the machine can do many things that a human mind cannot do: but if there is of necessity something that the machine cannot do, though the mind can, then, however trivial the matter is, we cannot equate the two, and cannot hope ever to have a mechanical model that will adequately represent the mind.

This argument seems to be "For each machine, there is some Godel sentence it cannot verify. There exists some mind that can verify all these Godel sentences. Therefore, (some) minds are not machines." The second premise is the problem - some Godel sentences take 150 years to state, say, and no human mind could understand them, let alone verify them.

He also responds to Turing again later, but it's a different argument of Turing's, so not relevant to my answer.

• You might be interested in Kurt Ammon's arXiv preprint (arXiv:1302.1155v1 [cs.AI] 5 Feb 2013) preprint, "An Effective Procedure for Computing "Uncomputable" Functions (seeing that he wrote, "An automatic proof of Godel's incompleteness theorem," Artificial Intelligence, 61(2): 291-306, 1993). It is somewhat like the Lucas argument, only using the notion of productive sets. Jun 28, 2019 at 15:25
• Also, Coq can prove that the natural numbers form a model of $PA$ (and therefore of $ZF^{*}$) and in this sense can have an 'intuition' of the consistency of arithmetic. What say you? Jun 28, 2019 at 17:07
• @ThomasBenjamin I don't see how your second comment contradicts or casts doubt on anything I said. Jun 28, 2019 at 17:25
• So you are saying then that one cannot rescue Lucas' reasoning by arguing that humans can see the consistency of $ZF^{*}$ by mathematical intuition when Coq can show that the natural numbers form a model of $ZF^{*}$? Jun 28, 2019 at 19:49
• @ThomasBenjamin For any specific formal system, the fact that humans can see the consistency of that formal system by mathematical intuition doesn't rescue Lucas's reasoning, because one could construct a computer program that assumes the correctness of that formal system. (For instance, Coq in the case of $ZF^*$). To make Lucas's argument work you need to know that, for every formal system, humans can determine the consistency of that system, which is absurd. Jun 28, 2019 at 20:00

What is wrong with Lucas’ argument:

Any attempt to mechanize our mathematical intuitions is doomed to fail because the very fact of mechanization yields new intuitive knowledge, e.g. Goedel’s sentence, which is not captured by the machine.

The problem is that you have to know quite a lot about the machine to conclude that its corresponding Goedel’s sentence is true. For example, if you know that this machine produces only true sentences you may infer that its Goedel’s sentence is true (this is Tarski’s theorem) and if you know that this machine is consistent (i.e. does not produce contradictions) you may infer that its Goedel’s sentence is even provable (this is Goedel’s theorem).

But even the machine can prove that its Goedel’s sentence is provable if the machine is consistent, as commented by John Coleman before (this is Goedel’s theorem again).

On the other hand, it remains possible that there may exist (and even be empirically discoverable) a mathematical machine which in fact is equivalent to our mathematical intuitions. For example, I could be such a machine.

Lucas confused the incorrect proposition:

There is no machine which could capture all our mathematical intuitions.

With the correct proposition:

There is no machine which could capture all our mathematical intuitions and which we could understand well enough to see that its Goedel’s sentence is true.

Hence, as far as Goedel’s incompleteness theorem is concerned I could well be a machine. But if I am then I am definitely not capable of the complete knowledge of the machine, i.e. of the complete knowledge of myself.