Suppose someone offers a program that can inspect any other program and tell you whether it will eventually finish. It always answers correctly, and it always finishes its own inspection. You might want it before starting a long calculation. You might also use it to catch a service that will hang forever.
The promise contains its own undoing. Feed the inspector a program designed to do the opposite of its prediction, and then make that program inspect itself. A few lines of reasoning are enough to defeat the universal guarantee.
Roger Penrose’s argument about the mind begins near this territory: the difference between following a formal procedure and recognizing why that procedure has limits. The mathematical limit is firm. What it tells us about a person is harder to establish. Following the distinction gives us a better account of both human understanding and useful machine checking.
The inspector that meets its opposite
Call the imagined inspector H. It takes a program and an input, and returns either “halts” or “runs forever.” Here is a new program, D, described in ordinary language:
- Ask H whether the program supplied as input will halt when given itself as input.
- If H says it will halt, run forever.
- If H says it will run forever, stop.
Now supply D with D.
If H predicts that D halts on itself, D follows its second instruction and runs forever. If H predicts that D runs forever, D follows its third instruction and stops. Either prediction is wrong. We did not find a slow inspector or one with too little memory. We found an impossible specification: a terminating, always-correct procedure for every program-input pair.
This is the familiar modern halting argument. Turing’s original 1936 paper develops related undecidability results using his formal account of computation; its circle-free-machine formulation should not be mistaken for exactly this classroom presentation. Turing’s original paper and MIT’s undecidability lecture materials provide the historical and teaching context.
Many particular programs remain easy to classify. A loop that increments a natural-number counter until it reaches ten finishes. A loop whose condition is permanently true and whose body never exits does not. The universal failure does not erase these local answers. It tells an inspector designer to choose a restricted domain, accept occasional uncertainty, or give up the guarantee of finishing every inspection.
That distinction matters outside a logic course. A tool can be excellent at detecting certain bugs while leaving other cases unresolved. “Unknown” can be its correct output.
Checking a proof and finding a proof
A formal proof is a finite sequence of steps governed by specified rules. Once the statements, axioms and inference rules have been made precise, a checker can inspect a proposed proof step by step. A searcher has a different job: find a proof, if one exists. It may try possibilities for a very long time.
There is a third demand beyond either task: decide every mathematical truth. Gödel’s incompleteness results show why sufficiently expressive, effectively axiomatized, consistent systems cannot settle every arithmetic statement. “Sufficiently expressive” matters: the system must support enough arithmetic for the construction. “Effectively axiomatized” matters too: its axioms can be mechanically enumerated. Removing those conditions changes the question.
Consistency means the system does not derive a contradiction. Soundness, in the interpretation being discussed, means its conclusions are true. They are different requirements. A consistent collection of rules can still describe a structure other than the intended natural numbers or assert a false arithmetic sentence. The familiar explanation of a Gödel sentence as a truth beyond the system needs its relevant assumptions made explicit. Feferman’s technical review sets out these distinctions and the soundness assumptions behind Penrose’s computational formulation.
A finite proof can therefore be mechanically checkable without there being a complete mechanical catalogue of arithmetic truth. The limitation does not make checking pointless. It tells us what a checked proof establishes: that this conclusion follows in this formal setting, from these premises.
The step Penrose wants to take
Penrose argues that mathematical understanding reaches beyond any fixed computational procedure offered as a complete account of it. Given a suitable sound procedure, a mathematician can reason about a statement it cannot establish. That ability to look at the procedure from outside is the heart of the attraction. We seem able to change our rules and understand the reason for changing them.
His position is more demanding than the casual slogan that people have intuition and computers have rules. In his reply to critics, Penrose discusses an idealized totality of humanly accessible methods of valid mathematical reasoning. He defends the inference from that idealization to soundness, and addresses the objection that human reasoning cannot simply certify its own reliability. His target is a complete computational account of mathematical understanding, rather than a single unsuccessful AI program. Penrose’s 1996 reply, especially section 3, is the source for this argument.
Here is the crucial hinge in a simpler conditional form: if a proposed formal procedure is sound in the required sense, then the relevant diagonal construction reveals a limitation. Understanding the conditional does not automatically establish its premise for every proposed account of the human mind.
An analogy helps locate the gap. You can understand why a bridge would carry a load if its materials and design satisfy certain conditions. That understanding does not test the steel. Likewise, recognizing the implication from soundness to a mathematical conclusion does not by itself establish the soundness of an unknown model of your reasoning. The analogy concerns conditional reasoning; bridges are not formal systems.
A criticism that leaves the question open
Solomon Feferman criticized Penrose’s logical argument while also expressing skepticism about computational accounts of mind. That combination is revealing. Rejecting a proposed proof of noncomputability does not require believing that a brain is just a familiar computer. It can mean that the proof has not supplied what it needs.
Human mathematicians make mistakes, disagree over methods and correct their work. Penrose’s idealization deliberately reaches beyond that everyday fallibility. The dispute then concerns whether the idealized capacity can be assigned the soundness and accessibility his conclusion requires. An observer who says “I see the truth beyond this system” still owes an account of the assumptions that make the seeing reliable.
Nor does changing axioms settle the matter by itself. A computer can also be programmed to extend a theory according to a specified rule. If the total extension process remains effective and the resulting system has the relevant properties, an incompleteness limitation applies again. Human novelty needs an argument about the complete capacity, not a comparison with a machine temporarily held fixed.
We can preserve the open question without pretending the competing views have been decided. Gödel gives a mathematical theorem. Penrose proposes a consequence for mathematical understanding. A physical account of how a brain achieves such understanding would add another layer of explanation.
A useful limit
For an AI user, there are two different questions to carry away. Can a machine check a particular answer against clear rules? Often it can. Does that capability explain every aspect of human thought or subjective experience? The proof checker does not answer that question.
The universal inspector fails because of the breadth of its guarantee. A narrower checker succeeds by making its contract visible. Once we ask exactly which statement it checks, under which assumptions, a mathematical limit becomes guidance for building something dependable.
Loading comments…