Is the Halting probability a Dedekind real number?

Bhupinder Singh Anand[1]

(A .pdf  file of this essay before the current update is available at http://arXiv.org/abs/math/0306023 and at http://www.mathpreprints.com/math/Preprint/anandb/20030521/1)

In a historical overview, Cristian S. Calude, Elena Calude, and Solomon Marcus identify eight stages in the development of the concept of a mathematical proof in support of an ambitious conjecture: we can express classical mathematical concepts adequately only in a mathematical language in which both truth and provability are essentially unverifiable. In this essay we show, first, that the concepts underlying their thesis can, however, be interpreted constructively; and, second, that an implicit thesis in the authors’ arguments implies that the Halting problem is solvable, but that, despite this, the probability of a given Turing machine halting on a random input cannot be assumed to define a Dedekind real number.

1.  Introduction

In an arXived paper ([Ca01], v2), “Passages of Proof”, Cristian S. Calude, Elena Calude, and Solomon Marcus conjecture that:

Reason and experiment are two ways to acquire knowledge. For a long time mathematical proofs required only reason; this might be no longer true.

As the basis for their belief, they identify eight stages in the development of the concept of a mathematical proof:

(a)  The first period was that of pre-Greek mathematics, for instance the Babylonian one, dominated by observation, intuition and experience.

(b)  The second period was started by Greeks such as Pythagoras and is characterised by the discovery of deductive mathematics, based on theorems.

(c)  ... with Galilei, Descartes, Newton and Leibniz, the mathematical language became more and more a mixed language, characterized by a balance between its natural and artificial components. ... This was the third step in the development of mathematical proofs.

(d)  The fourth step is associated with the so-called epsilon rigour, so important in mathematical analysis; it occurred in the XIXth century and it is associated with names such as A. Cauchy and K. Weierstrass.

(e)  The fifth period begun with the end of the 19th century, when Aristotle’s logic, underlining mathematical proofs for two thousands years, entered a crisis with the challenge of the principle of non-contradiction.

(f)  The sixth period begins with Godel’s incompleteness theorem (1931), for many meaning the unavoidable failure of any attempt to formalise the whole mathematics.

(g)  The seventh period belongs to the second half of the 20th century, when algorithmic proofs become acceptable only when their complexities were not too high.

(h)  With the eighth stage, proofs are no longer exclusively based on logic and deduction, but also empirical and experimental factors.

1.1  What is proof?

The authors then ask, rhetorically, ([Ca01], v2):

What is a mathematical proof ? At a first glance the answer seems obvious: a proof is a series of logical steps based on some axioms and deduction rules which reaches a desired conclusion. Every step in a proof can be checked for correctness by examining it to ensure that it is logically sound. In David Hilbert’s words: “The rules should be so clear, that if somebody gives you what they claim is a proof, there is a mechanical procedure that will check whether the proof is correct or not, whether it obeys the rules or not.”

They note, however, that:

In 1976, Kenneth Appel and Wolfgang Haken proved the 4CT (Four Colour Theorem) ... No human being could ever actually read the entire proof to check its correctness ... “The real question is this: If no human being can ever hope to check a proof, is it really a proof ?”

The authors’ perception of the relation between truth and provability is reflected in their comments:

... Godel’s incompleteness theorem (GIT) which says that every formal system which is (1) finitely specified, (2) rich enough to include the arithmetic, and (3) consistent, is incomplete[2]. That is, there exists an arithmetical statement which (A) can be expressed in the formal system, (B) is true, but (C) is unprovable within the formal system. ... But what does it mean to be a “true arithmetical statement”? It is a statement about non-negative integers which cannot be invalidated by finding any combination of non-negative integers that contradicts it. ... a true arithmetical statement is a “primordial mathematical reality”. ... The essence of GIT is to distinguish between truth and provability. A closer analogy in real life is the distinction between truths and judicial decisions, between what is true and what can be proved in court. How large is the set of true and unprovable statements? If we fix a formal system satisfying all three conditions in GIT, then the set of true and unprovable statements is topologically “large” (constructively, a set of second Baire category, and in some cases even “larger”).

Prima facie, under the standard interpretations of classical[3] mathematical theory, which the authors seem to implicitly assume ([Ca01], v2), the above remarks can be taken to imply that the authors accept mathematical truth as being unverifiable effectively. It follows that there could, then, be any number of (equally reasonable) ways of responding to their question:

... what does it mean to be a “true arithmetical statement”?

However, in their attempt to offer an ambitious interpretation of classical theory, the authors do not address the question:

Can such latitude in the perception of fundamental meta-mathematical concepts such as truth and provability reflect a basic ambiguity in our definitions of foundational mathematical concepts?

On the contrary, the authors seem to be comfortable with the, implicitly Platonic, suggestion that classical concepts of mathematical proof, and even truth, might actually lie beyond the ambit of direct intuitive cognition! They conclude that ([Ca01], v2):

If we accept the above assumptions about the biological and physical nature of proofs, then there is little ‘intrinsic’ difference between traditional and ‘unconventional’ types of proofs as i) first and foremost, we have not access to truth, ii) correctness is not absolute, but nearly certain as mathematics advances by making mistakes and correcting and re–correcting them ..., iii) non–deterministic and probabilistic proofs do not allow mistakes in the applications of rules, they are just indirect forms of checking ... which correspond to various degrees of rigour, iv) the explanatory component, the understanding ‘generated’ by proofs, while extremely important from a cognitive point of view, is subjective and has no bearing on formal correctness.

... more research will be performed in large computational environments where we might or might not be able to determine what the system has done or why ... The blend of logical and empirical-experimental arguments are here to stay and develop. ... There are many reasons which support this prediction. They range from economical ones (powerful computers will be more and more accessible to more and more people), social ones (sceptical oldsters are replaced naturally by youngsters born with the new technology, results and success inspire emulation) to pure mathematical (new challenging problems, wider perspective) and philosophical ones (note that incompleteness is based on the analysis of the computer’s behaviour).

2.  Interpreting classical mathematical theory

2.1  Standard interpretations of foundational concepts may be ambiguous

Now, we note that, as is implicit in Mendelson’s [Me90] following remarks (italicised parenthetical qualifications added), standard interpretations of classical foundational concepts can, indeed, be argued as being either ambiguous, or non-constructive, or both:

Here is the main conclusion I wish to draw: it is completely unwarranted to say that CT (Church’s Thesis) is unprovable just because it states an equivalence between a vague, imprecise notion (effectively computable function) and a precise mathematical notion (partial-recursive function). ... The concepts and assumptions that support the notion of partial-recursive function are, in an essential way, no less vague and imprecise (non-constructive, and intuitionistically objectionable) than the notion of effectively computable function; the former are just more familiar and are part of a respectable theory with connections to other parts of logic and mathematics. (The notion of effectively computable function could have been incorporated into an axiomatic presentation of classical mathematics, but the acceptance of CT made this unnecessary.) ... Functions are defined in terms of sets, but the concept of set is no clearer (not more non-constructive, and intuitionistically objectionable) than that of function and a foundation of mathematics can be based on a theory using function as primitive notion instead of set. Tarski's definition of truth is formulated in set-theoretic terms, but the notion of set is no clearer (not more non-constructive, and intuitionistically objectionable), than that of truth. The model-theoretic definition of logical validity is based ultimately on set theory, the foundations of which are no clearer (not more non-constructive, and intuitionistically objectionable) than our intuitive (non-constructive, and intuitionistically objectionable) understanding of logical validity. ... The notion of Turing-computable function is no clearer (not more non-constructive, and intuitionistically objectionable) than, nor more mathematically useful (foundationally speaking) than, the notion of an effectively computable function.

The questions thus arise: Could the thesis conjectured in ([Ca01], v2) also be founded on ambiguities that are rooted in the standard interpretations of classical foundational concepts such as “mathematical object”, “effective computability”, “truth of a formula under an interpretation”, “set”, “Church’s Thesis” etc.; ambiguities that may, moreover, encourage non-constructive, Platonic, interpretations by default? How would such a thesis fare if we could make these concepts unambiguous, and constructive, in an intuitionistically unobjectionable way?

2.2  Can classical concepts be defined constructively?

Now, prima facie, we can, indeed, define these concepts constructively in terms of a small number of primitive, formally undefined but intuitively unobjectionable, mathematical terms as below:

(i) Primitive mathematical object: 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.[4]

(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.

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

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

[1] The author is an independent scholar. E-mail: re@alixcomsi.com; anandb@vsnl.com. Postal address: 32, Agarwal House, D Road, Churchgate, Mumbai - 400 020, INDIA. Tel: +91 (22) 2281 3353. Fax: +91 (22) 2209 5091.

[2] We note that this is an instance of the standard interpretation of Gödel’s seminal 1931 paper [Go31a] that may be arguably definitive; if we apply the standard Deduction Theorem of first order logic to Gödel’s meta-proof of his Theorem VI in the cited paper, then we can, reasonably, argue that his formal system P is omega-inconsistent. Theorem VI would, in such case, hold vacuously, and the incompleteness of P would not, then, be a consequence.

[3] For the purposes of this essay, we take the expositions by Hardy [Ha47], Landau [La51], Mendelson [Me64], Rudin [Ru53] and Titchmarsh [Ti61] as representative, in the areas that they cover, of classical mathematical reasoning and conclusions.

[4] We note that, as remarked by Mendelson [Me90], the terms “function” and “function letter” - and, presumably, “individual constant”, “predicate”, and “predicate letter” - can be taken as undefined, primitive foundational concepts.

[5] We note that classical definitions of the effective computability of a function (cf. [Me64], p207) do not distinguish between the two cases.

[6] We use square brackets to distinguish between the uninterpreted string [F] of a formal system, and the symbolic expression “F” that corresponds to it under a given interpretation that unambiguously assigns formal, or intuitive, meanings to each individual symbol of the expression “F”.

[7] Under a constructive interpretation of formal Peano Arithmetic, Gödel’s undecidable proposition may, thus, be instantiationally, but not algorithmically, true under the standard interpretation.

[8] We note that, classically, Tarski’s definition of the truth of a formal proposition under an interpretation (cf. [Me64], p49-52) does not distinguish between the two cases.

[9] Standard first order Peano Arithmetic such as Mendelson’s formal system S ([Me64], p102).

[10] We note that, by reasoning that lies outside the immediate scope of this essay, introduction of an equivalent statement of this thesis, as an independent Quantum Halting Hypothesis, allows us to model a deterministic universe that is essentially unpredictable.

[11] We note that the classical Church Thesis is the assertion: “A number-theoretic function is effectively computable if, and only if, it is recursive” (cf. [Me64], p227).

[12] For “relation R(x)”, read “proposition (Ax)R(x)”.

[13] This is actually an implicit meta-lemma in Theorem VI of Gödel’s seminal 1931 paper [Go31a].

[14] This, too, is an implicit meta-lemma in Theorem VI of Gödel’s seminal 1931 paper [Go31a].

[15] For “meta-theorem”, read “meta-lemma” in this section.

[16] “If R(x1, ..., xn) is a relation, then its characteristic function, Cn(x1, ..., xn), is defined as follows:

Cn(x1, ..., xn) = 0 if R(x1, ..., xn) is true, and Cn(x1, ..., xn) = 1 if R(x1, ..., xn) is false.” ([Me64], p119).

[17] We assume that such a machine can be effectively meta-programmed to proceed to the next instantaneous tape description whenever it encounters a loop.

[18] They correspond to the instances where a classical Turing machine that computes the recursive function G(a, y) will halt for some y, loop for some y, or not halt for any y, respectively.

[19] This concept is essentially that of parallel computing, where the action of one machine can influence the action of another unpredictably, without human intervention. Since classical Turing machines are necessarily sequential, such a procedure cannot be defined as a classical Turing machine. Hodges remarks [HA00] that the possibility of parallel machines being essentially different from his Logical Computing Machines does not (arguably) appear to have been considered by Turing:

“... Another source may lie in Turing's definition of an ‘oracle-machine’ which is a Turing machine allowed at certain points to ‘consult the oracle’. Such a machine is not purely mechanical: it is like the ‘choice-machine’ defined in (Turing 1936-7) which at certain points allows for human choices to be made. Turing used the word ‘machine’ for entities which are only partially mechanical in operation, reserving the term ‘automatic machine’ for those which are purely mechanical. Copeland appears to imagine that when Turing describes the oracle-machine definition as giving a ‘new type of machine’, he is defining a new type of automatic machine. On the contrary, Turing is defining something only partially mechanical.

To take this point further, it is worth noting that the expression ‘purely mechanical process’ enters into Turing's definitive statement of the Church-Turing thesis, which comes as an opening section to (Turing 1939), and that Turing goes on: ‘understanding by a purely mechanical process one which could be carried out by a machine’. In the subsequent discussion the word ‘machine’ is used to mean ‘Turing machine’. There is no evidence that Turing had any concept of a purely mechanical ‘machine’ of any kind other than encapsulated by the Turing machine definition.”

[20] We define a prefix-free Halting program as a digital string that does not start with a string, smaller than itself, that is, itself, a Halting program.

[21] The significance of this may need to be viewed, however, in the light of earlier remarks in footnote 1.

[22] Chaitin defines Omega, for a given Universal Turing machine U, as:

Omega = SUM 2-|p| over all prefix-free, binary, strings p on which U halts, where |p| is the length of the string p.

However, when compared to the classical definition of probability considered earlier, and the value of Omega if we eliminate the prefix-free stipulation, it is not clear in which sense this sum can be termed as a probability that U will halt when its binary, prefix-free input is chosen randomly, e.g., by flipping a coin.

[23] This theorem would, then, hold vacuously; it would, then, follow that, constructively, ZFC may not be arithmetically sound, in the sense that it may not be a model for standard PA.

[24] This result may also need to be viewed against the arguments of the previous section; if the Halting probability is not a set-theoretically defined Dedekind real number, then it is not clear what arithmetical interpretation, or significance, is to be given to a routine that calculates “finitely many bits of Omega” or one that “can give a bound on the number of bits of Omega which ZFC can determine”.

[25] Standard interpretations of classical mathematical theory ignore the possibility of such a distinction between Cantorian real numbers and Dedekind real numbers.

[26] Since every step of a formal proof sequence is either an axiom, or an immediate consequence of any two preceding elements of the sequence, each step can be effectively verified mechanistically by identifying the concerned axiom, or two preceding elements of the sequence. So long as each step is verified as logically sound, such a procedure need not be time bound, nor limited to the conceptual ability of any one individual to grasp, or even verify, the correctness of the entire proof.