Index                                                                                                                                      Main essay

 

Is there a “loophole” in Gödel’s interpretation of his formal reasoning and its consequences?

Bhupinder Singh Anand[1]

(A .pdf  file of this essay before the current update is available at http://arXiv.org/abs/math/0304309)

We formally define a “mathematical object” and “set”. We then argue that expressions such as “(Ax)F(x)”, and “(Ex)F(x)”, in an interpretation M of a formal theory P, may be taken to mean “F(x) is true for all x in M”, and “F(x) is true for some x in M”, respectively, if, and only if, the predicate letter “F” is a mathematical object in P.

In the absence of such a meta-proof, the expressions “(Ax)F(x)”, and “(Ex)F(x)”, can only be taken to mean that “F(x) is true for any given x in M”, and “It is not true that F(x) is false for any given x in M”, respectively, indicating that the predicate “F(x)” is well-defined, and effectively decidable individually, for any given value of x, but that there may be no uniform effective method (algorithm) for such decidability.

We show how some paradoxical concepts of Quantum mechanics can then be expressed in a constructive interpretation of standard Peano's Arithmetic.

1. Introduction

Is there a “loophole” in Gödel’s conclusion, in his seminal 1931 paper [Go31a], that his formally unprovable arithmetical proposition GUS - which we may formally write as the string[2] [(Ax)R(x)] - is, firstly, undecidable in any formal system, PA, of Arithmetic based on Dedekind’s formulation of the Peano Axioms, and, secondly, true, under the standard interpretation M of PA, in a constructive, and intuitionistically unobjectionable, way[3]?

Now, classically, the string [(Ax)R(x)] does translate formally as a true proposition under the standard interpretation of PA. However, there is nothing intuitive or constructive (in the sense of being effectively verifiable) about such “truth”. The proposition is “true” only in a formal sense, where we accept Tarski’s definition[4]: a string [(Ax)F(x)] is true under an interpretation M if, and only if, the interpreted relation, F(x), is true for every x in M.

Although this appears to be a fairly innocent definition of intuitive truth, we note that it implicitly commits us to the acceptance of Platonic elements in the domain of the interpretation M; it (implicitly) implies that we may (explicitly) assert a formal relation as satisfied in M if, and only if, it is severally, and jointly, satisfied by the elements in the ontology of M even if there are elements of this ontology that are not interpretations of any mathematical objects in PA.

Now, a constructive view of Gödel’s reasoning is that it actually establishes the invalidity of such a broad, implicit (hence ambiguous) assumption; thus, we can argue that we cannot unrestrictedly assert [R(x)] as jointly satisfied by all x in the standard interpretation M of PA, although we can assert that [R(x)] is satisfied (severally) by any given x in M.

The significance of this distinction is seen in Corollary 1.1 to Meta-lemma 1 of Anand [An02b]; the totality of values for which [R(x)] is satisfied in M may not be constructively definable as a formal mathematical object. In other words, the classical assumption that such values define a “set” in an Axiomatic Set Theory such as ZFC may introduce an inconsistency. Thus, we cannot make any constructive, or meaningful, assertion about the totality of values that satisfy [R(x)] in M.

More precisely, Corollary 1.1 asserts that every recursive number-theoretic relation may not well-define a (recursively enumerable[5]) sub-set of the natural numbers consistently in any Axiomatic Set Theory[6] that is a consistent extension of PA.

The above becomes clearer if we define a mathematical object and a set precisely as follows:

Definition (i): A primitive mathematical object is any symbol for an individual constant, predicate letter, or a function letter, which is defined as a primitive symbol of a formal mathematical language.

Definition (ii): A formal mathematical object is any symbol for an individual constant, predicate letter, or a function letter that is either a primitive mathematical object, or that can be introduced through definition into a formal mathematical language without inviting inconsistency.

Definition (iii): A mathematical object is any symbol that is either a primitive mathematical object, or a formal mathematical object.

Definition (iv): A set is the range of any function whose function letter is a mathematical object.

We can then argue, as a consequence of the theorem cited above, that expressions such as “(Ax)F(x)”, and “(Ex)F(x)”, in an interpretation M of a formal theory P, may be taken to mean[7]F(x) is true for all x in M”, and “F(x) is true for some x in M”, respectively, if, and only if, the predicate letter “F” is a formal mathematical object in P.

In the absence of a proof that “F” is such a mathematical object, the expressions “(Ax)F(x)” and “(Ex)F(x)” can only be taken to mean that “F(x) is true for any given x in M”, and “It is not true that F(x) is false for any given x in M”, indicating that the predicate “F(x)” is well-defined, and decidable, for any given value of x, but that there may not be any uniformly effective method for such decidability.

2. What exactly does this mean, and why is the distinction important?

What exactly does this mean, and why is the distinction important?

Taking the latter part of the question first, the distinction is important because we do not, then, need to accept absolute limits on our ability to adequately formalise our intuitive mathematical concepts.

Now, a central issue in the development of any significant Artificial Intelligence is that of finding effective methods of duplicating the cognitive and expressive processes of the human mind. This issue is being increasingly brought into sharper focus by the rapid advances in the experimental, behavioral, and computer sciences[8]. Penrose’s “The Emperor’s New Mind” and “Shadows of the Mind” highlight what is striking about the attempts, and struggles, of current work in these areas to express their observations adequately - necessarily in a predictable way - within the standard interpretations of formal propositions as offered by classical theory. 

So, the question arises: Are formal classical theories essentially unable to adequately express the extent and range of human cognition, or does the problem lie in the way formal theories are classically interpreted at the moment? The former addresses the question of whether there are absolute limits on our capacity to express human cognition unambiguously; the latter, whether there are only temporal limits - not necessarily absolute - to the capacity of classical interpretations to communicate unambiguously that which we intended to capture within our formal expression.

 Now, my thesis is that we may comfortably reject the first, by recognising that we can, indeed, constructively reformulate Tarski’s definitions, of the “satisfiability” and “truth” of formal relations and propositions, respectively, under a given interpretation, less ambiguously.

3. A constructive definition of Tarskian truth

So, we return to the first part of the earlier question: what exactly does this mean?

Well, it means that we can, for instance, replace the strong[9], classical, implicit interpretation of Tarski’s non-constructive definition, which is essentially the assertion:

(i) The string [F(x)] of a formal system P is satisfied under an interpretation M of P if, and only if, the interpreted predicate F(x) is satisfied jointly, and severally, by the elements in the ontology of M;

by the weaker, explicit assertion:

(ii) The string [F(x)] of a formal system P is satisfied under an interpretation M of P if, and only if, the interpreted predicate F(x) is satisfied either jointly, or severally, by the elements in the ontology of M;

We can, further, eliminate any implicit commitment to a Platonic ontology by making these definitions constructive - in the sense of being effectively verifiable:

(iii) The string [F(x)] of a formal system P is individually satisfied under an interpretation M of P if, and only if, given any value k in M, there is an individually effective method (which may depend on the value k) to determine that the interpreted proposition F(k) is satisfied in M;

(iv) The string [F(x)] of a formal system P is uniformly satisfied under an interpretation M of P if, and only if, there is a uniformly effective method (necessarily independent of x) such that, given any value k in M, it can determine that the interpreted proposition F(k) is satisfied in M.

(v) The string [F(x)] of a formal system P is satisfied under an interpretation M of P if, and only if, it is either uniformly satisfied in M, or it is individually satisfied in M.

Clearly, if [F(x)] is uniformly satisfied in M, then it is, obviously, individually satisfied in M. However, does the converse hold? More to the point, could Gödel’s undecidable proposition, [(Ax)R(x)], be an instance of a formula [R(x)] that is individually satisfied in M (since Gödel shows that [R(k)] is provable in P for any numeral [k]), but not uniformly satisfied in M?

An interesting consequence of an affirmative answer to this question would be that the interpreted arithmetical predicate R(x) - which is instantiationally equivalent to a primitive recursive relation - becomes Turing-undecidable! Prima facie, this would appear to conflict with the classical postulation that a number-theoretic function is Turing-computable if, and only if, it is partial recursive[10]. However, the conflict may be illusory: the proof of equivalence seems to presume that there is a uniformly effective method (algorithm) for computing the partial recursive function[11]. This proof would be invalid if we held that Gödel has shown there are total[12] arithmetical functions, and relations, that may not be computable, or decidable, respectively, by any uniform method.

(This may, indeed, have been the interpretation that prompted Turing to assert the essential equivalence between Gödel’s definition of an undecidable, but true, arithmetical proposition, and his own definition of a number-theoretic Turing-uncomputable Halting function.)

4. Effective computability and Church’s Thesis

A key question, of course, is: why change?

One reason is that of verifiability: we are now able to define effective computability constructively, i.e. in a verifiable manner, by answering the questions:

 (vi) When may we constructively assume that, given any sequence s of an interpretation M of P, there is an individually effective method to determine that s satisfies a given P-formula in M?

 (vii) When may we constructively assume that there is a uniformly effective method such that, given any sequence s of an interpretation M, s satisfies a given P-formula in M?

If the domain D of M can be assumed representable in P, then (vi) can be answered constructively; we simply reformulate the classical Church Thesis as follows:

(viii) Individual Church Thesis: If, for a given relation R(x), and any value a in some interpretation M of P, there is an individually effective method such that it will determine whether R(a) holds in M or not, then every element of the domain D of M is the interpretation of some term of P, and there is some P-formula [R'(x)] such that:

 R(a) holds in M if, and only if, [R'(a)] is P-provable.

In other words, the Individual Church Thesis postulates that the domain of a relation R that is effectively decidable individually in an interpretation M of some formal system P can only consist of mathematical objects, even if R is not, itself, a mathematical object.

However, (vii) can be answered constructively for any interpretation M of P, if we postulate:

(ix) Uniform Church Thesis: If, in some interpretation M of P, there is a uniformly effective method such that, for a given relation R(x), and any value a in M, it will determine whether R(a) holds in M or not, then R(x) is the interpretation in M of a P-formula [R(x)], and:

 R(a) holds in M if, and only if, [R(a)] is P-provable.

Thus, the Universal Church Thesis postulates, firstly, that the domain of a relation R that is effectively decidable uniformly in an interpretation M of a formal system P can only consist of mathematical objects; and, secondly, that R, too, is necessarily a mathematical object.

Some interesting consequences of the above are that:

(x) The Uniform Church Thesis implies that a formula [R] is P-provable if, and only if, [R] is uniformly true in some interpretation M of P.

(xi) The Uniform Church Thesis implies that if a number-theoretic relation R(x) is uniformly satisfied in some interpretation M of P, then the predicate letter “R” is a formal mathematical object in P (i.e. it can be introduced through definition into P without inviting inconsistency).

(xii) The Uniform Church Thesis implies that, if a P-formula [R] is uniformly true in some interpretation M of P, then [R] is uniformly true in every model of P.

(xiii) The Uniform Church Thesis implies that if a formula [R] is not P-provable, but [R] is classically true under the standard interpretation, then [R] is individually true, but not uniformly true, in the standard model of P.

(xiv) The Uniform Church Thesis implies that Gödel’s undecidable sentence GUS is individually true, but not uniformly true, in the standard model of P.[13]

By defining effective computability, both individually and uniformly, along similar lines, we can give a constructive definition of uncomputable number-theoretic functions:

(xv) A number-theoretic function F(x1, ..., xn) in the standard interpretation M of P is uncomputable if, and only if, it is effectively computable individually, but not effectively computable uniformly.

This, last, removes the mysticism behind the fact that we can define a total number-theoretic Halting function that is, paradoxically, Turing-uncomputable.

5. The Uniform Church Thesis and the classical Church-Turing Theses

The significance, of defining the truth of a formula of P under interpretation explicitly in terms of individual, and uniform, effective methods, and of expressing Church’s Thesis constructively, is seen if we note that any computer can be designed to recognise a “looping” situation; it simply records every instantaneous tape description at the execution of each machine instruction, and compares the current instantaneous tape description with the record.

Now, we could instruct such a machine to assign arbitrary values to those undefined instances of the Halting predicate whose occurrences cause the machine to loop. Prima facie, what we appear to have here is an individually effective decision method that is dependent entirely on the particular Halting function that is being computed, and cannot be predicted.

Is such a machine a Turing machine? The classical answer to this question is not obvious if we do not appeal to the Church-Turing Thesis.

However:

(xvi) If we assume a Uniform Church Thesis, then every partial recursive number-theoretic function F(x1, ..., xn) has a unique constructive extension as a total function.

(xvii) If we assume a Uniform Church Thesis, then not every effectively computable function is classically Turing computable (so Turing’s Thesis does not, then, hold).

(xviii) If we assume a Uniform Church Thesis, then not every (partially) recursive function is classically Turing-computable.[14]

(xix) If we assume a Uniform Church Thesis, then the class P of polynomial-time languages in the P versus NP problem may not define a formal mathematical object.

Appendix 1:

Constructivity and classical Quantum Theory

In Anand [An02c], we show how the introduction of constructive definitions of classical mathematical concepts may permit formal systems of Peano Arithmetic to model some of the more paradoxical concepts of Quantum Mechanics. For instance, as a consequence of §4(xiv), consider the following argument:

(a) Gödel has proved in his 1931 paper that there is an arithmetic formula [R(x)] such that, for any given k, [R(k)] is provable.

(b) Hence, for any given k, there is always some effective method for evaluating the arithmetic expression R(k).

(cGödel has also proved in the above paper that [(Ax)R(x)] is not provable.

(d) Thesis: There is no uniform effective method (algorithm/Turing machine) that can evaluate the arithmetic expression R(x) for any given x.

(e) Thus, R(n) is individually computable, but not uniformly computable.

(fTheorem (provable by induction): For any given k, we can always find some effective method (algorithm/Turing machine) T(k) that can compute R(n) for all n<k, i.e. T(k) terminates for all n<k, but it "loops" on input k. (Note: All methods that evaluate R(n) for all n<k cannot be non-terminating on input k; this would imply that R(k) is undefined, which would contradict (b).)

(g) Quantum interpretation: The process of finding T(k+1) can be corresponded, firstly, to the act of finding a suitable method of measuring the value R(k) precisely, and, secondly, to the collapse of the wave function at k as a result of the measurement; we then have the new "state" T(k'), which can evaluate the value of R(n) for all n<k', where k<k', but not beyond!

(h) If, now, we have some law that determines the state T(k') from the state T(k) and the interaction at k, we have a deterministic interaction that is, nevertheless, absolutely unpredictable, where we may then define free will as absolute unpredictability. (We note that, if k' > k+1, we have a language that admits inter-actions that can leave the state T(k') unchanged.)

Now we note that a counter-thesis to (d) would be:

(i) Counter-Thesis: There is some uniform effective method (algorithm/Turing machine) that can evaluate the arithmetic expression R(x) for any given x.

It follows from Gödel’s reasoning in [Go31a] that both (d) and (i) are effectively unverifiable, since they cannot be proved formally. We thus have two standard models of Peano Arithmetic - classical and constructive - that are mutually inconsistent. If we assume that both are consistent, the above argument indicates the interpretation that implies (d) may be the more suitable language for expressing concepts of classical Quantum Theory.

References

[An02a]  Anand, B. S. 2002. Reviewing Gödel’s and Rosser’s meta-reasoning of “undecidability”. (Web essay)

 

<Web page: http://alixcomsi.com/Constructivity_consider.htm>

[An02b]  Anand, B. S. 2002. Some consequences of a recursive number-theoretic relation that is not the standard interpretation of any of its formal representations. (Web essay)

 

<Web page: http://alixcomsi.com/CTG_06_Consequences.htm>

[An02c]  Anand, B. S. 2002. Is a deterministic universe logically consistent with a probabilistic Quantum Theory? (Web essay)

 

<Web page: http://alixcomsi.com/CTG_08_Quantum_consistency1.htm>

[Br93]     Bringsjord, S. 1993. The Narrational Case Against Church's Thesis. Easter APA meetings, Atlanta.

 

<Web-page: http://www.rpi.edu/~brings/SELPAP/CT/ct/ct.html>

[Go31a]  Gödel, Kurt. 1931. On formally undecidable propositions of Principia Mathematica and related systems I. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York.

[Go31b]  Gödel, Kurt. 1931. On formally undecidable propositions of Principia Mathematica and related systems I.

 

<Web version: http://home.ddc.net/ygg/etext/godel/index.htm>

[Ha47]    Hardy, G.H. 1947, 9th ed. Pure Mathematics. Cambridge, New York

[Ho00]    Hodges, A. 2000. Uncomputability in the work of Alan Turing and Roger Penrose. (Unpublished lecture)

 

<Web page: http://www.turing.org.uk/philosophy/lecture1.html>

[Ka59]    Kalmár, L. 1959. An Argument Against the Plausibility of Church's Thesis. In Heyting, A. (ed.) Constructivity in Mathematics. North-Holland, Amsterdam.

[Kl36]     Kleene, S.C. 1936. General Recursive Functions of Natural Numbers. Math. Annalen 112.

[La51]     Landau, E.G.H. 1951. Foundations of Analysis. Chelsea Publishing Co., New York

[Me64]   Mendelson, Elliott. 1964. Introduction to Mathematical Logic. Van Norstrand, Princeton

[Me90]   Mendelson, E. 1990. Second Thoughts About Church's Thesis and Mathematical Proofs. Journal of Philosophy 87.5.

[Pe90]     Penrose, R. (1990, Vintage edition). The Emperor's New Mind: Concerning Computers, Minds and the Laws of Physics. Oxford University Press.

[Pe94]     Penrose, R. (1994). Shadows of the Mind: A Search for the Missing Science of Consciousness. Oxford University Press.

[Po01]    Podnieks, Karlis. 2001. Around Goedel's Theorem.

 

<e-textbook: http://www.ltn.lv/~podnieks/gt.html>

[RH01]   Ramachandran, V. S. and Hubbard, E. M. 2001. Synaesthesia - A Window Into Perception, Thought and Language. Journal of Consciousness Studies, 8, No. 12.

 

<Ramachandran’s Web page: http://psy.ucsd.edu/chip/ramapubs.html>

[Ru53]    Rudin, Walter. 1953. Principles of Mathematical Analysis. McGraw Hill, New York.

(Ti61)      Titchmarsh, E. C. 1961. The Theory of Functions. Oxford University Press.

[Tu36]     Turing, Alan. 1936. On computable numbers, with an application to the Entscheidungsproblem.

 

<Web page: http://www.abelard.org/turpap2/tp2-ie.asp - index>

 

(Acknowledgements: My thanks to Ms Shuchi Mehta for requesting a note on my perceived “loophole” in Gödel’s 1931 paper. This essay is an edited version of that note.)

 

(Updated: Wednesday 2nd June 2004 8:59:46 AM IST by re@alixcomsi.com)

 

Index           Top of page


[1] The author is an independent scholar.

 

[2] We use the synonymous terms “string” and “formula” interchangeably.

 

[3] At the end of his proof of Theorem VI in his 1931 paper [Go31a] on formally undecidable propositions, Gödel remarks: “One can easily convince oneself that the proof we have just given is constructive (for all the existential assertions occurring in the proof rest upon Theorem V which, as it is easy to see, is intuitionistically unobjectionable), ...”.

 

[4] We take Mendelson ([Me64], p49-52) as a standard exposition of Tarski’s definitions of the “satisfiability” and “truth” of formal strings under a given interpretation; and of the basic foundational concepts of classical mathematical theory in general.

 

[5] A recursively enumerable set is classically defined ([Me64], p250) as the range of some recursive number-theoretic function, and is implicitly assumed to be consistent with any Axiomatic Set Theory that is a model for P.

 

[6] Loosely speaking, we may not be able to give a set-theoretic definition, of Gödel’s primitive recursive function Sb(x v|Z(y)), such that {x | x=Sb(y 19|Z(y))} defines a set in any Axiomatic Set Theory with a Comprehension Axiom, or its equivalent, without introducing inconsistency.

 

Consequently, we may not be able to consistently assume that every recursive function formally defines a recursively enumerable set. It follows that we may be unable to define a recursive set as a recursively enumerable set whose complement is also recursively enumerable. In some cases, there may be no such complement.

 

It further follows that, if F(y) is an arithmetical function such that F(k) = Sb(k 19|Z(k)) for any given k, the assertion that the expression {x | x=F(y)} defines a formal set by the Comprehension Axiom may require additional qualification.

 

[7] We note that such interpreted symbolic expressions are simply abbreviations of semantically well-defined assertions of a language of communication in which we express our cognitive experiences.

 

[8] See, for instance ([RH01], footnote 18).

 

[9] As remarked earlier, such a strong assertion may also be invalid under a constructive interpretation of Gödel’s reasoning in Theorem VI of his 1931 paper.

 

[10] Cf. ([Me64], p233, Corollary 5.13 and p237, Corollary 5.15).

 

[11] See ([Me64], p226, Corollary 5.11).

 

[12] We define a number-theoretic function, or relation, as total if, and only if, it is individually computable, or individually decidable, respectively.

 

[13] An intriguing consequence of this argument is considered in Appendix 1.

 

[14] The classical proof that every (partially) recursive function is classically Turing-computable uses induction over (partial) recursive functions, thus assuming that every such function is a mathematical object; by Meta-lemma 1, such an assumption may be invalid.