(Notations, non-standard concepts, and definitions used commonly in these investigations are detailed in this post.)

An Evidence-Based Proof of Lucas’ Gödelian Thesis and a Definitive Turing Test

Abstract: In this note I detail an evidence-based proof of Lucas’ Gödelian Thesis, and define a definitive Turing Test that differentiates between a human intelligence and a mechanical intelligence.

Introduction

In a paper: `The truth assignments that differentiate human reasoning from mechanistic reasoning: The evidence-based argument for Lucas’ Gödelian thesis’, which appeared in the December 2016 issue of Cognitive Systems Research [An16][1], I briefly addressed the philosophical challenge that arises when an intelligence—whether human or mechanistic—accepts arithmetical propositions as true under an interpretation—either axiomatically or on the basis of subjective self-evidence—without any specified methodology for objectively evidencing such acceptance in the sense of Chetan Murthy and Martin Löb:

“It is by now folklore … that one can view the values of a simple functional language as specifying evidence for propositions in a constructive logic …” … [Mu91][2], Section 1, Introduction.

“Intuitively we require that for each event-describing sentence, \phi_{o^{\iota}}n_{\iota} say (i.e. the concrete object denoted by n_{\iota} exhibits the property expressed by \phi_{o^{\iota}} ), there shall be an algorithm (depending on I, i.e. M^{*} ) to decide the truth or falsity of that sentence.” … [Lob59][3], p.165.

Evidence-based reasoning in Arithmetic: Evidence-based reasoning accepts arithmetical propositions as true under an interpretation if, and only if, there is some specified methodology for objectively evidencing such acceptance.

The philosophical ramifications of formally validating John Lucas’ original Gödelian argument in [Lu61][4]—against a reductionist account of the mind—now raise issues (as in [An15b][5]) that lie, and deserve consideration, beyond the formal argumentation of [An16][1].

For instance, the roots of this note lie in the Mechanist’s counter-argument against Lucas’ Gödelian Thesis, as articulated in [An07a][6] (see also [An07b][7] and [An07c][8]; as also this post and this post), which can now be viewed, and refuted, from a broader perspective that admits an evidence-based, Wittgensteinian, distinction between:

(1) mathematically proven, i.e., algorithmically computable (see Appendix B, Definition 2, here), `truth’; and

(2) meta-mathematically proven, i.e., algorithmically verifiable (see Appendix B, Definition 1, here), `truth’;

to which Theorem 1 (below) appeals.

The distinction formalises the reported (see [Lam17][9]) intent underlying Wittgenstein’s objection—in his `notorious’ paragraph in [Wi78][10]—towards conflating mathematical and meta-mathematical entailments, by showing that:

(a) whereas the Mechanist correctly argues (in [An07a][6]) that, for any given numeral [n] , a Universal Turing machine can always mathematically prove that Gödel’s arithmetic formula [R(n)] (as defined in Theorem 1 below) is a theorem in PA;

(b) no Turing machine can mathematically prove that the formula [(\forall x)R(x)] with Gödel number 17Gen\ r is a theorem in PA; and, ipso facto, meta-mathematically conclude—as a human can—that it could, for any given numeral [n] , prove that Gödel’s arithmetic formula [R(n)] is a theorem in PA.

Accordingly, I restrict myself here to merely drawing attention to Lucas’ concluding remarks in an informal defence of his Gödelian Thesis:

“Thus, though the Gödelian formula is not a very interesting formula to enunciate, the Gödelian argument argues strongly for creativity, first in ruling out any reductionist account of the mind that would show us to be, au fond, necessarily unoriginal automata, and secondly by proving that the conceptual space exists in which it (is) intelligible to speak of someone’s being creative, without having to hold that he must be either acting at random or else in accordance with an antecedently specifiable rule”. [Luxx][11].

and to briefly detailing only the import of the evidence-based reasoning introduced in [An12][12] for:

(i) Formally validating Lucas’ Gödelian Thesis as articulated in [An16][1]; and

(ii) Answering affirmatively Alan Turing’s earlier, but related, query in [Tu50][13] as to whether it is possible to definitively differentiate between a human intelligence and a mechanical intelligence.

Validating Lucas’ Gödelian Argument

We begin by noting that the introduction of evidence-based reasoning into the, conflicting, classical (Hilbert’s) and intuitionistic (Brouwer’s) interpretations of quantification (see [An15a][14], Sections 1.1 and 2.1) yields two—hitherto unsuspected and essentially different—well-defined interpretations of the first-order Peano Arithmetic PA (see Appendix A here), over the structure N of the natural numbers, which are complementary, and not contradictory (see [An16][1]).

The former yields the classical, weak, standard interpretation I_{PA(N, SV)} of PA over N (see Appendix B here), which is non-finitarily well-defined relative to the assignment of weak algorithmically verifiable Tarskian truth values (see Appendix C here) to the compound formulas of PA under I_{PA(N, SV)} (see [An16][1], Theorem 5.6). The well-definedness follows from the non-finitary proof of consistency for PA detailed in [An16][1], Theorem 5.7.

The latter yields an unsuspected, strong, finitary interpretation I_{PA(N, SC)} of PA over N , which is finitarily well-defined relative to the assignment of strong algorithmically computable Tarskian truth values to the compound formulas of PA under I_{PA(N, SC)} (see [{An16][1], Theorem 6.7). The well-definedness follows from the finitary proof of consistency for PA detailed in [An16][1], Theorem 6.8.

We shall now see that the complementarity can also be viewed as validating Lucas’ Gödelian argument, if we treat it as the claim that (see [An16][1], Thesis 1):

Theorem 1 There can be no mechanist model of human reasoning if the standard interpretation I_{PA(N, SV)} of the first-order Peano Arithmetic PA can be treated as circumscribing the ambit of human reasoning about `true’ arithmetical propositions, and the finitary interpretation I_{PA(N, SC)} of PA can be treated as circumscribing the ambit of mechanistic reasoning about `true’ arithmetical propositions.

Notation: We use square brackets to differentiate between a symbolic expression—such as [(\exists x)P(x)] —which denotes a formula of a formal language L , and the symbolic expression—such as (\exists x)P^{*}(x) —that denotes its intended meaning under a well-defined interpretation of L , where the L -formula [P(x)] interprets as the relation P^{*}(x) .

Proof: We note that Kurt Gödel has shown meta-mathematically how to construct an arithmetical formula with a single variable, say [R(x)] —Gödel refers to this formula only by its Gödel number r in [Go31][15], p.25(12)—such that:

\bullet [R(x)] is not PA-provable; but

\bullet [R(n)] is PA-provable for any PA numeral [n] .

Hence, for any numeral [n] , Gödel’s primitive recursive relation xB \lceil [R(n)] \rceil must hold for some natural number m :

\bullet where xBy denotes Gödel’s primitive recursive relation (see [Go31][15], p. 22(45)):

`x is the Gödel-number of a proof sequence in PA whose last term is the PA formula with Gödel-number y ‘;

\bullet and \lceil [R(n)] \rceil denotes the Gödel-number of [R(n)] ;

We also note (see [An16][1], Theorem 2.1), that we cannot conclude finitarily from Tarski’s definitions (see Appendix C, Definitions 3 to 10 here) whether, or not, a quantified PA formula [(\forall x)F(x)] is algorithmically verifiable as always true, under I_{PA(N, SV)} , if [F(x)] is algorithmically verifiable (see Appendix B, Definition 1 here) under I_{PA(N, SV)} , but not algorithmically computable (see Appendix B, Definition 2 here) under I_{PA(N, SC)} .

Now:

(i) Since Gödel has shown meta-mathematically that the PA-formula [R(n)] is PA-provable for any PA-numeral [n] , it follows that:

(a) For any natural number n , there is always a deterministic algorithm which will provide evidence that the interpretation R^{*}(n) of [R(n)] under I_{PA(N, SV)} is an algorithmically verifiable true arithmetical proposition.

Moreover:

(ii) By [An16][1], Corollary 8.2, the formula [\neg(\forall x)R(x)] is provable in PA. Hence, since PA is finitarily consistent (see [An16], Theorem 6.8), we can mathematically conclude, under I_{PA(N, SC)} , that:

(a) There is no deterministic algorithm which, for any numeral [n] , will provide evidence that the interpretation R^{*}(n) of [R(n)] under I_{PA(N, SC)} is an algorithmically computable true arithmetical proposition.

However:

(iii) Since PA is also non-finitarily consistent (see [An16][1], Theorem 5.7), we cannot contradict (i)(a) by non-finitarily interpreting quantification under I_{PA(N, SV)} and mathematically concluding from the PA-provability of the formula [\neg(\forall x)R(x)] either that:

(a) For some unspecified natural number n , there is a deterministic algorithm which provides evidence that the interpretation R^{*}(n) of [R(n)] under I_{PA(N, SV)} is not an algorithmically verifiable true arithmetical proposition.

or that:

(b) For some unspecified natural number n , there is no deterministic algorithm which will provide evidence that the interpretation R^{*}(n) of [R(n)] under I_{PA(N, SV)} is an algorithmically verifiable true arithmetical proposition.

Instead:

(iv) By [An16][1], Corollary 8.3, we can only conclude, under I_{PA(N, SV)} , that the PA-provability of the formula [\neg(\forall x)R(x)] implies that we cannot mathematically conclude from the axioms and rules of inference of PA that:

(a) For any natural number n , there is always a deterministic algorithm which will provide evidence that the interpretation R^{*}(n) of [R(n)] under I_{PA(N, SV)} is an algorithmically verifiable true arithmetical proposition.

If we now assume that the finitary interpretation I_{PA(N, SC)} of PA can be treated as circumscribing the ambit of mechanistic reasoning about `true’ arithmetical propositions, whence any mechanical witness can only reason mathematically—i.e., finitarily from the PA axioms and rules of inference, as in (iv) (see [An16][1], Theorem 7.1)—then although, for any numeral [n] , a mechanical witness can give evidence under the finitary interpretation I_{PA(N, SC)} that the PA formula [R(n)] holds in N , no mechanical witness can conclude finitarily under the finitary interpretation I_{PA(N, SC)} of PA that, for any numeral [n] , the PA formula [R(n)] holds in N (since, by Corollary 8.2 in [An16][1], the formula [\neg (\forall x)R(x)] is provable in PA).

Whereas, if we assume that the standard interpretation I_{PA(N, SV)} of PA can be treated as circumscribing the ambit of human reasoning about `true’ arithmetical propositions—whence a human witness can also reason meta-mathematically, i.e., non-finitarily, from the PA axioms and rules of inference, as in (i)—then a human witness can conclude under the non-finitary standard interpretation I_{PA(N, SV)} of PA that, for any numeral [n] , the PA formula [R(n)] holds in N . The theorem follows. … \Box

Significance of differentiating between strong algorithmically computable truth, and weak algorithmically verifiable truth

We note that the importance of differentiating between:

(i) the strong, algorithmically computable, `truth’—of the provable formulas of a formal mathematical language L —which follows by finitary mathematical reasoning from the axioms and rules of inference of L under a well-defined interpretation; and

(ii) the weak, algorithmically verifiable, `truth’—of the provable formulas of L —which follows by non-finitary meta-mathematical reasoning from the axioms and rules of inference of L under a well-defined interpretation;

is:

(a) reflected in Thoralf Skolem’s ([Sk22][16], p.295) cautionary remarks against inviting paradox by conflating entailments of different formal systems over different domains;

(b) implicit in, and an essential component of, Lampert’s interpretation of Ludwig Wittgenstein’s objection—in the latter’s `notorious’ paragraph in [Wi78][10]—to the conclusions that Gödel drew from his undifferentiated mathematical/meta-mathematical reasoning in [Go31][15]:

“The most crucial aspect of any comparison of two different types of unprovability proofs is the question of what serves as the “criterion of unprovability” (I, Section 15). According to Wittgenstein, such a criterion should be a purely syntactic criteria independent of any meta-mathematical interpretation of formulas. It is algorithmic proofs relying on nothing but syntactic criteria that serve as a measure for assessing meta-mathematical interpretations, not vice-versa.” … [Lam17][9]

A definitive Turing Test

“Let us fix our attention on one particular digital computer C. Is it true that by modifying this computer to have an adequate storage, suitably increasing its speed of action, and providing it with an appropriate programme, C can be made to play satisfactorily the part of A in the imitation game, the part of B being taken by a man? \ldots 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.” … [Tu50][13], Section 5 and Objection (3).

Theorem 1 can also be viewed as a definitive Turing Test between a logician and any Turing machine TM.

In other words, we can demonstrate that the algorithmically computable architecture of any conceivable Turing machine (digital computer) has inherent limitations which constrain it from answering the following Query in the affirmative; whereas the human brain is not constrained similarly.

Query 1: Can you prove that, for any numeral [n] , Gödel’s arithmetic formula [R(n)] is a theorem in the first-order Peano Arithmetic PA, where [R(x)] is defined by its Gödel number r in eqn.12, and [(\forall x)R(x)] is defined by its Gödel number 17Gen\ r in eqn.13, on p.25 of [Go31][15]? Answer only either `Yes’ or `No’.

Logician: Yes.

By Gödel’s meta-mathematical reasoning on p.26(2) of [Go31][15], a logician can conclude, for any numeral [n] , that the formula [R(n)] is a theorem in PA; even though the formula [(\forall x)R(x)] is not a theorem in PA.

TM: No.

By Corollary 8.2 in [An16][1], the formula [\neg (\forall x)R(x)] is provable in PA and so, by Theorem 7.1 in [An16], no Turing machine can prove that the formula [(\forall x)R(x)] with Gödel number 17Gen\ r is a theorem in PA and, ipso facto, conclude that, for any numeral [n] , Gödel’s arithmetic formula [R(n)] is a theorem in PA.

Appendix A: The Peano Arithmetic PA

Appendix B: The Two Interpretations of PA

Appendix C: Tarski’s Inductive Definitions

References

Return to 1 [An16] Anand, B. S. 2016. The truth assignments that differentiate human reasoning from mechanistic reasoning: The evidence-based argument for Lucas’ Gödelian thesis. In Cognitive Systems Research, 40. Elsevier.

Return to 2 [Mu91] Murthy, C. R. 1991. An evaluation semantics for classical proofs. In Proceedings of Sixth IEEE Symposium on Logic in Computer Science, 96–109. Also Cornell TR 91-1213, 1991.

Return to 3 [Lob59] Löb, M. H. 1959. Constructive Truth. In Proceedings of the Colloquium Held at Amsterdam, 1957, Studies in Logic and the Foundations of Mathematics, Eds. L. E. J. Brouwer, E.W. Beth, A. Heyting, Constructivity in Mathematics, A. Heyting (ed.), pp.159-168, North-Holland Publishing Company, Amsterdam.

Return to 4 [Lu61] Lucas, J. R. 1961. Minds, Machines and Gödel. Philosophy XXXVI:112–127. Reprinted in The Modeling of Mind. Kenneth M.Sayre and Frederick J.Crosson, eds., Notre Dame Press, 1963, pp.269-270; and Minds and Machines, ed. Alan Ross Anderson, Prentice-Hall, 1964, pp.43-59.

Return to 5 [An15b] Anand, B. S. 2015. Algorithmically Verifiable Logic vis à vis Algorithmically Computable Logic: Could resolving EPR need two complementary Logics? Paper presented on 26’th June at the Workshop on Emergent Computational Logics at UNILOG’2015, 5th World Congress and School on Universal Logic, 20th June 2015 – 30th June 2015, University of Istanbul, Istanbul, Turkey.

Return to 6 [An07a] Anand, B. S. 2007. The Mechanist’s Challege. The Reasoner, Vol(1)5 p5-6.

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

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

Return to 9 [Lam17] Lampert, T. 2017. Wittgenstein and Gödel: An Attempt to Make “Wittgenstein’s Objection” Reasonable. In Philosophia Mathematica. nkx017.

Return to 10 [Wi78] Wittgenstein, L. 1937. Remarks on the Foundations of Mathematics. Cambridge: MIT Press, 1978 edition.

Return to 11 [Luxx] Lucas, J. R. 19xx. The Gödelian Argument: Turn Over the Page. Web essay.

Return to 12 [An12] Anand, B. S. 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 13 [Tu50] Turing, A. M. 1950. Computing Machinery and Intelligence. In Mind, Volume LIX, Issue 236, 1 October 1950:433–460.

Return to 14 [An15a] Anand, B. S. 2015. Why Hilbert’s and Brouwer’s interpretations of quantification are complementary and not contradictory. In Epsilon 2015 Workshop on Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics, 10th June 2015 – 12th June 2015. Paper presented on 10th June at the University of Montpellier, Montpellier, France.

Return to 15 [Go31] Gödel, K. 1931. On formally undecidable propositions of Principia Mathematica and related systems I. Translated from the German original by Elliott Mendelson. In Martin Davis (ed.), The Undecidable, 1965. Dover edition 2004, pp.5-38, Dover Publications Inc., Mineola, NY 1150.

Return to 16 [Sk22] Skolem, T. 1922. Some remarks on axiomatized set theory. Text of an address delivered in Helsinki before the Fifth Congress of Scandinavian Mathematicians, 4-7 August 1922. In Jean van Heijenoort (ed.) From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931, 1967 edition, pp.464-479, Harvard University Press, Cambridge, Massachusetts.

References in Appendices

[Ba16] Bauer, A. 2016. Five Stages of Accepting Constructive Mathematics. In Bull. Math. Soc. (N. S.). Electronically published on October 3, 2016.

[Ct75] Chaitin, G. J. 1975. A Theory of Program Size Formally Identical to Information Theory. In Journal of the ACM (JACM), volume 22, Issue 3, July 1975, pp.329-340. Association for Computing Machinery, New York.

[Ct82] Chaitin, G. J. 1982. Gödel’s Theorem and Information. In International Journal of Theoretical Physics, volume 21, pp.941-954. Kluwer Academic Publishers-Plenum Publishers.

[Hi27] Hilbert, D. 1927. The Foundations of Mathematics. Text of an address delivered in July 1927 at the Hamburg Mathematical Seminar. In Jean van Heijenoort (ed.) From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931, 1967 edition, pp.464-479, Harvard University Press, Cambridge, Massachusetts.

[Me64] Mendelson, E. 1964. Introduction to Mathematical Logic. Princeton: Van Norstrand, 1964 edition.