(The following arguments summarise the main points sought to be made in this paper)

Why has Lucas’ and Penrose’s faith in their Gödelian arguments remained unshaken despite unassailable critiques?

Most reasoned critiques [1] of John. R. Lucas’ and Roger Penrose’s philosophical Gödelian arguments [2] against computationalism have been unassailable when viewed from their mathematical and logical perspectives.

However, as John R. Lucas’ latest tour de force, `Reason and Reality’, appears to suggest, they have failed to satisfactorily explain why Lucas and Penrose—reasonable men both—seemingly remain convinced of the essential soundness of their philosophical argumentations.

One reason could be that Lucas’ and Penrose’s philosophical arguments place unquestioning faith in, and uncritically follow, standard logical and mathematical expositions of classical theory in overlooking what Gödel has implicitly proven in Theorem VI of his seminal 1931 paper on `undecidable’ arithmetical propositions [3]; another, that their arguments place similar faith in and, as uncritically, accept Gödel’s own, informal, interpretation [4] of the implications of this Theorem as definitive.

If so, neither the arguments nor their authors should be taken to task on either count for their faith; it is the standard mathematical and logical expositions of Gödel’s reasoning that are ambiguously silent on both issues.

Specifically, we shall first argue that—contrary to the conventional wisdom that Lucas and Penrose may have reasonably accepted in good faith—the Tarskian satisfaction and Tarskian truth [5] of the formulas of an Arithmetic under an interpretation, and the soundness of the Arithmetic itself, can indeed be formally defined in an effectively verifiable manner within the Arithmetic.

We shall then suggest that although this appears to demolish the main reasons offered in support of Lucas’ original Gödelian argument, it yet leaves open the question for consideration in a future post of whether human intelligence and machine intelligence are qualitatively different.

Lucas’ Reason and Reality

The question arises: Why has the possibility of such definitions continued to elude critical philosophical enquiry by Lucas (and perhaps Penrose)?

Part of the answer may lie in Lucas’ panoramic 2006 overview of how the elements of reason and reality have been perceived—and sought to be put in some coherent perspective—by philosophers down the ages, where Lucas reveals candidly what lies at the heart of the philosophy underpinning his Gödelian argument.

It is apparently the belief—presumably based on standard mathematical and logical expositions of Gödel’s reasoning—that the truth of an arithmetical statement—in the context of his argument—is essentially intuitive, and beyond formal verification:

“Gödel’s theorem is difficult to understand, easy to misunderstand. The formal proof shows only that if the system is consistent, then the Gödelian formula is unprovable in the system. Some philosophers have suggested that the system itself is inconsistent. But that is a counsel of despair; and if elementary number theory were inconsistent, deduction would cease to be a paradigm of valid argument. Other philosophers stick their feet in and refuse to recognise the Gödelian proposition as true. And of course if a man refuses to concede as true anything except what can be proved in a formal system, he can avoid any further embarrassment, beyond that of having to be remarkably obdurate to cogent mathematical reasoning. Essentially what he is doing is to deny any application of the word `true’. He can understand what the word `provable’ means, and can be forced to acknowledge that in a consistent formalisation of elementary number theory there must be formulas which can be neither proved nor disproved in the formalised system. But he refuses to understand what the word `true’ means, and see that the proposition expressed by the Gödelian formula must in fact be true.

But we do understand what `true’ means, and we learn from Gödel’s theorem that truth outruns provability. That has always been believed by some thinkers, though denied by others, who have shied away from any concept of truth that could not be established against the sceptic by some copper-bottomed proof. But once the concept of proof has been made explicit, and the criteria for being provable clearly laid down, Gödel’s theorem shows that there are truths which go beyond that concept of provable.

We are led, therefore, to reject certain minimalising views of truth and reason. It is possible for propositions to be true, even though we cannot verify them. It make sense to claim truth, to wonder about truth, to seek truth, beyond the limits of assured knowledge.”

… J. R. Lucas, Reason and Reality, Chapter 2 pp.36-37.

How the Gödelian argument appeals to Tarski’s Undefinability Theorem, and why it shouldn’t!

A not inconsiderable factor in the formation of such a philosophical perspective on the nature of arithmetical—and perhaps even mathematical—truth must surely be that standard mathematical and logical expositions of Gödel’s and Tarski’s reasoning hold Tarski’s Theorem [6] as informally implying that the Tarskian truth of the formulas of Peano Arithmetic under its standard interpretation is of necessity subjectively semantic, and cannot be formalised objectively within the Arithmetic.

Tarski’s Undefinability Theorem: The set of Gödel-numbers of the formulas of any first-order Peano Arithmetic which are true in the standard model of the Arithmetic is not arithmetical.

Now, what this Theorem asserts formally is that there is no PA formula [F(x)] such that, if [p] is the numeral corresponding to the Gödel number of the PA formula [P], then [F(p)] is true under the standard interpretation of PA if, and only if, P^{*} is true (where P^{*} is the interpretation of [P] under the standard interpretation of PA).

However, what it is taken to informally imply in standard mathematical and logical expositions of current theory is reflected in the following representative remarks:

“This result can be paraphrased by saying that the notion of arithmetical truth is not arithmetically definable.”


“… arithmetical truth cannot be defined in arithmetic.”


So, perhaps Lucas and Penrose have—not unreasonably—relied unquestioningly on such informal—but unarguably authoritatively postulated—implication in the formation of philosophical perspectives for their Gödelian arguments.

We shall now argue that the implication does not withstand scrutiny from a finitary perspective.

In what sense should Tarski’s definitions of satisfiability and truth be decidable unequivocally?

We note first that, in order to avoid ambiguity, it is implicitly accepted as self-evident in standard mathematical and logical expositions of current theory that Tarski’s standard definitions of the satisfiability, and truth, of the formulas of a formal language L under a well-defined interpretation M must be capable of being interpreted unequivocally.

For instance, under Tarski’s definitions a formula [R(x)] of L is defined as satisfied under M if, and only if, its corresponding interpretation, say R^{*}(x), holds in M for any assignment of a value s that lies within the range of the variable x in M.

From a finitary perspective however (such as the one detailed here), Tarski’s definitions can be considered mathematically significant only if we assume that, given any s in M, we can unequivocally decide whether, or not, R(s) holds, or must hold, in M.

The formula [(\forall x)R(x)] of L could also, then, be unequivocally defined as true under the interpretation M if, and only if, [R(x)] were satisfied under M.

Moreover, the formula [\neg(\forall x)R(x)] of L would, further, be definable as true under the interpretation M if, and only if, [(\forall x)R(x)] were false under M.

In other words, from a finitary perspective, definitions of mathematical satisfaction and truth under an interpretation can be considered significant only if they can be defined relative to an unequivocal decidability under the interpretation.

What gives an illusory legitimacy to Lucas’ and Penrose’s Gödelian arguments?

Lucas’ and Penrose’s arguments gain an illusory appearance of legitimacy only because standard mathematical and logical expositions of current theory either do not highlight, or are unaware of, both the significance of, and the ambiguity implicit in, a failure to meet such a requirement of unequivocal decidability [8].

For instance, taking L as PA, we have on the one hand the Church-Turing Thesis which suggests that such decidability ought to be algorithmic.

On the other hand, however (as we show here), the decidability of mathematical satisfaction and truth under the standard interpretation of PA is not only left implicit, but invites an ambiguity that is compounded further by weakening the decidability to effective instantiational, rather than algorithmic, decidability.

Moreover, the intuitive perception underlying such implicit weakening is justifible since, by the principle of Occam’s razor, the former decidability is the minimum requirement of Tarski’s definitions.

Both Lucas and Penrose, quite reasonably therefore, attempt to draw philosophical conclusions—from standard mathematical and logical expositions of the content and meaning of Gödel’s meta-logical argument—that cannot but reflect the absence of an explicit definition of formal decidability for the formulas of Peano Arithmetic under its standard interpretation.

Clearly, they should not be held accountable for the validity of the mathematical and logical premises on which they base their philosophical conclusions, since the onus of making the foregoing decidability explicit can only rest upon standard mathematical and logical expositions of classical theory.

Can we explicitly define satisfaction and truth verifiably?

That we can explicitly define the satisfaction and truth of the formulas of a language L under an interpretation M in a verifiable manner becomes evident if we take M to be an interpretation of L in L itself.

We then have the formalisation of the verifiable concepts of formal satisfaction, and formal truth, of the formulas [R(x)] and [(\forall x)R(x)] of L, respectively, in L, as:

The formula [R(x)] of L is defined as formally satisfied under L if, and only if [R(s)] is provable in L for any term [s] that can be substituted for the variable [x] in [R(x)].

The formula [(\forall x)R(x)] of L is formally true in L if, and only if, [R(x)] is formally satisfied in L.

Can we define formal soundness verifiably?

If we, further, define formal soundness as the property that the axioms of a theory are satisfied in the theory itself, and that the rules of inference preserve formal truth, then, it follows that the theorems of any formally sound theory must be formally true in the theory.

(Question: Is the first-order Peano Arithmetic formally sound?)

Gödelian propositions are formally true but formally unprovable

Now, even if the formula [(\forall x)R(x)] is not provable in L, it would be formally true in L if, and only if, the formula [R(s)] were provable in L for any well-defined term [s] of L that could be substituted for [x] in [R(x)].

The constructive existence of such a Gödelian proposition is precisely what Gödel proves by his Theorem VI [9] for any simply consistent Peano Arithmetic such as PA.

He constructs a formula, [(\forall x)R(x)], of PA that is, itself, unprovable in a simply consistent PA even though, for any given numeral [n], the formula [R(n)] is provable in the PA.

So, Gödel has constructed a formally unprovable Arithmetical formula that is not only implicitly true in the standard interpretation of the Arithmetic, but which is also formally true in the Arithmetic in a verifiable, and intuitionistically unobjectionable, manner that leaves no room for dispute as to its `truth’ status vis-á-vis the PA axioms!

Moreover, if the Arithmetic can be shown to be formally sound—again in a verifiable, and intuitionistically unobjectionable, manner—then we no longer need appeal to the arguable assumption that the Arithmetic is implicitly sound under the standard interpretation.

We note that PA is said to be sound for a class S of sentences if, whenever PA proves [\phi] with [\phi] in S, then \phi^{*} is true in the structure \mathbb{N} of the natural numbers.

Replacing the philosophically debatable concept of implicit decidability with constructively verifiable definitions of formal decidability under the standard interpretation of PA should, thus, place Lucas’ and Penrose’s Gödelian arguments in better perspective.

Can we define arithmetic truth verifiably within PA?

The significance of the above remarks is highlighted by the following.

Let [F(x_{1}, \ldots, x_{n})] be a PA-formula whose Gödel number in Gödel’s notation [10] is f, and let F^{*}(x_{1}, \ldots, x_{n}) be its standard interpretation over the structure \mathbb{N} of the natural numbers under which:

(a) the set of non-negative integers is the domain,

(b) the integer 0 is the interpretation of the numeral [0],

(c) the successor operation (addition of 1) is the interpretation of the S function (i.e., of [f_{1}^{1}],

(d) ordinary addition and multiplication are the interpretations of [+] and [\star],

(e) the interpretation of the predicate letter [=] is the identity relation.

… Mendelson. [11]

(We note that, by the above definition, the structure of the real numbers is isomorphic to the structure of the PA numerals, and any decidability of the satisfaction and truth of PA formulas under the standard interpretation over \mathbb{N} must therefore reflect a corresponding decidability of the satisfaction and truth of PA formulas under a formal interpretation over the PA numerals. Curiously, standard texts do not highlight this point.)

Now, following Gödel [12], we can define the concept `f is a PROVABLE FORMULA of PA’ as:

Bew_{PA} (f) \equiv (\exists y)y \hspace{+.5ex}B_{PA}\hspace{+.5ex}f

However, we can also define the concept `f is a TRUE FORMULA of PA’ in the above notation as (where p_{n} denotes the n^{th} prime number):

Tr_{PA} (f) \equiv (\forall u_{1}) \ldots (\forall u_{n})(\exists y)y \hspace{+.5ex}B\hspace{+.5ex} \{ Sb_{PA}(f \begin{array}{c} 17 \\ Z(u_{1}) \end{array} \ldots \begin{array}{c} p_{n+6} \\ Z(u_{n}) \end{array})\}

In other words, Tr_{PA} (f) holds if, and only if, for any given sequence [a_{1}, \ldots, a_{n}] of numerals, the PA-formula [F(a_{1}, \ldots, a_{n})] is PA-provable.

Hence, if Tr_{PA} (f) holds then [F(x_{1}, \ldots, x_{n})] interprets as instantiationally true under any sound interpretation of PA.

Now Gödel has also shown that there are arithmetical relations R(y) and S(y, u_{1}, \ldots, u_{n}) such that:

(i) for any natural number a:

a \hspace{+.5ex}B_{PA}\hspace{+.5ex}f \equiv R(a)

(ii) for any natural number sequence a, b_{1}, \ldots, b_{n}:

a \hspace{+.5ex}B\hspace{+.5ex} \{ Sb_{PA}(f \begin{array}{c} 17 \\ Z(b_{1}) \end{array} \ldots \begin{array}{c} p_{n+6} \\ Z(b_{n}) \end{array})\} \equiv \ S(a, b_{1}, \ldots, b_{n})

Hence, contrary to the current interpretations of Tarski’s and Gödel’s formal reasoning, both PA-provability and PA-truth (under any sound interpretation of PA) are `arithmetical’, in the sense that both can be defined unequivocally within the language of PA itself!

The road ahead for the Gödelian argument

Although lying beyond the scope of the immediate issue addressed in this post, we shall show in a future post that the TRUE and PROVABLE formulas defined above are, in fact, the Algorithmically verifiable and Algorithmically computable formulas of PA respectively as defined in the paper `Evidence-based Interpretations of PA‘ (presented at the Symposium on Computational Philosophy at the AISB/IACAP World Congress 2012-Alan Turing 2012, 2-6 July 2012, University of Birmingham, Birmingham, UK).

The argument of the paper is that the former define the standard non-finitary interpretation of PA (which does not yield a finitary proof of consistency for PA), whilst the latter define a sound finitary algorithmic interpretation of PA (which does establish the consistency of PA finitarily).

We further showed in this paper that, if the standard interpretation of PA is assumed to be sound, then PA is \omega-consistent, and so Aristotle’s particularisation must hold in the underlying logic.

Since Aristotle’s particularisation is a non-constructive postulation, the Gödelian argument against computationalism could be restated as asserting that whereas human intelligences can `para-consistently’ derive consequences from a first-order logic that admits Aristotle’s particularisation, a machine intelligence cannot.

Another way of stating this is that the standard interpretation of PA characterises the way in which human intelligences reason, whereas the algorithmic interpretation of PA characterises the way in which mechanical intelligences reason, and that the two are not identical.


BBJ03 George S. Boolos, John P. Burgess, Richard C. Jeffrey. 2003. Computability and Logic. (4th ed). Cambridge University Press, Cambridge.

EC89 Richard L. Epstein, Walter A. Carnielli. 1989. Computability: Computable Functions, Logic, and the Foundations of Mathematics. Wadsworth & Brooks, California.

Go31 Kurt Gödel. 1931. On formally undecidable propositions of Principia Mathematica and related systems I. Translated by Elliott Mendelson. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York. pp.5-38.

Lu61 John Randolph Lucas. 1961. Minds, Machines and Gödel. In Philosophy. Vol. 36, No. 137 (Apr. – Jul., 1961), pp. 112-127, Cambridge University Press.

Lu03 John Randolph Lucas. 2003. The Gödelian Argument: Turn Over the Page. In Etica & Politica / Ethics & Politics, 2003, 1.

Lu06 John Randolph Lucas. 2006. Reason and Reality. Edited by Charles Tandy. Ria University Press, Palo Alto, California.

Me64 Elliott Mendelson. 1964. Introduction to Mathematical Logic. Van Norstrand. pp.145-146.

Pe90 Roger Penrose. 1990. The Emperor’s New Mind: Concerning Computers, Minds and the Laws of Physics. 1990, Vintage edition. Oxford University Press.

Pe94 Roger Penrose. 1994. Shadows of the Mind: A Search for the Missing Science of Consciousness. Oxford University Press.

Sc67 Joseph R. Schoenfield. 1967. Mathematical Logic. Reprinted 2001. A. K. Peters Ltd., Massachusetts.

Ta33 Alfred Tarski. 1933. The concept of truth in the languages of the deductive sciences. In Logic, Semantics, Metamathematics, papers from 1923 to 1938. (p152-278). ed. John Corcoran. 1983. Hackett Publishing Company, Indianapolis.

Wa63 Hao Wang. 1963. A survey of Mathematical Logic. North Holland Publishing Company, Amsterdam.

An07a Bhupinder Singh Anand. 2007. The Mechanist’s challenge. In The Reasoner, Vol(1)5 p5-6.

An07b … 2007. Why we shouldn’t fault Lucas and Penrose for continuing to believe in the Gödelian argument against computationalism – I. In The Reasoner, Vol(1)6 p3-4.

An07c … 2007. Why we shouldn’t fault Lucas and Penrose for continuing to believe in the Gödelian argument against computationalism – II. In The Reasoner, Vol(1)7 p2-3.

An08 … 2008. Can we really falsify truth by dictat?. In The Reasoner, Vol(2)1 p7-8.

An12 … 2012. Evidence-Based Interpretations of PA. In Proceedings of the Symposium on Computational Philosophy at the AISB/IACAP World Congress 2012-Alan Turing 2012, 2-6 July 2012, University of Birmingham, Birmingham, UK.


Return to 1: See for instance: PSYCHE, 1996, 2(23); Journal of Experimental and Theoretical Artificial Intelligence, 2000, 12: 307-329; Behavioral and Brain Sciences, 1993, 16, 611-612).

Return to 2: See Lu61, Lu03, Lu06 and Pe90, Pe94.

Return to 3: See Theorem VI on p.24 of Go31.

Return to 4: On p.27 of Go31.

Return to 5: For purposes of this investigation we take Mendelson’s exposition (in Me64, pp.49-53) of Tarski’s definitions (cf. Ta36) as definitive.

Return to 6: Me64, p.151, Corollary 3.38.

Return to 7: Me64, p.151.

Return to 8: We highlight in An12 the far reaching consequences of the failure to insist upon unequivocal decidability for the satisfaction and truth of the formulas of PA under an interpretation.

Return to 9: Go31, p.24, Theorem VI.

Return to 10: Go31, p.13.

Return to 11: This definition is excerpted from Me64, p.107.

Return to 12: Go31, p.22 (Dfn.46).

Bhupinder Singh Anand