Mfcttrf

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

Godel'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 Godel's Proofs", Annals of Pure and Applied Logic 133 (2005) 319-338 (MSN)

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

suggest that computers can not only show that the Godel 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 Godel sentence is true. In point of fact, we actually infer the truth of the Godel sentence much as a theorem-prover might infer its truth (if in fact the theorem-prover can infer the truth of the Godel sentence, assuming ZF − Infinity is consistent).

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

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.

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.