◄ Index 
◄
Main essay
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
1.1 What is proof?
2. Interpreting classical mathematical theory
2.1 Standard
interpretations of foundational concepts may be ambiguous
2.2 Can classical
concepts be defined constructively?
2.3 Standard
interpretations may admit ambiguity
2.4 Reducing
Tarskian truth and satisfiability to provability
2.5 Some
consequences of a constructive interpretation
2.6 Defining
formal, constructive and Platonic concepts
3. Mathematical
proof and non-algorithmic effective methods
3.1 Non-algorithmic
effective methods: Gödel oracles
3.2 Defining
Tarskian truth verifiably
4.1 CCM’s
Thesis and the Halting problem
4.2 An
effective solution of the Halting problem
4.3 Is
the Halting probability a Dedekind real number?
4.4 Standard
interpretations of the significance of the Halting probability
5. Are mechanistic proofs of mathematical problems
logically sound?
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,
(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) Formal mathematical object: 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) Mathematical object: A mathematical object is any symbol that is either a
primitive mathematical object, or a formal mathematical object.
(iv) Set: A set is the range of any function whose function letter is a mathematical object.
(v)
Instantiational
computability: A
number-theoretic function F(x) is instantiationally computable if, and only if, given any
natural number k, there is always
an effective method (which may depend on the value k) to compute F(k).
(vi)
Algorithmic
computability: A
number-theoretic function F(x) is algorithmically computable if, and only if, there is an
effective method (necessarily independent of x) such that,
given any natural number k, it can
compute F(k).
(vii)
Effective computability: A number-theoretic function is effectively
computable if, and only if, it is either instantiationally computable, or it is
algorithmically computable.[5]
(viii)
Instantiational
truth: A string [F(x)][6] of a
formal system P is instantiationally true under an interpretation M of P if,
and only if, given any value k in M, there is an effective method (which may depend on the value k) to determine that the interpreted proposition F(k) is satisfied in M.[7]
(ix)
Algorithmic
truth: A string [F(x)] of a formal system P is algorithmically true under
an interpretation M of P if, and only if, there is an 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.
(x)
Effective
truth: A string [F(x)] of a formal system P is effectively true under an
interpretation M of P if, and only if, it is either instantiationally true in
M, or it is algorithmically true in M.[8]
(xi)
Instantiational
Church Thesis: If, for a given
relation R(x), and any
element k in some
interpretation M of a formal system P, there is an effective method such that
it will determine whether R(k) 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(k) holds in M if, and only if, [R'(k)]
is P-provable.
(xii) Algorithmic
Church Thesis: If, in some
interpretation M of a formal system P, there is an effective method such that,
for a given relation R(x), and any element k in M, it will determine whether R(k) holds in M or not, then R(x) is the interpretation in M of a P-formula [R(x)], and:
R(k) holds in M if, and only if, [R(k)] is P-provable.
2.3 Standard interpretations may admit ambiguity
2.4 Reducing Tarskian truth and satisfiability to provability
2.5 Some consequences of a constructive interpretation
(i)
The Algorithmic Church Thesis
implies that a formula [R] is P-provable if, and only if, [R] is
algorithmically true in some interpretation M of P.
(ii) The Algorithmic Church Thesis implies that if a
number-theoretic relation R(x) is algorithmically 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).
(iii) The Algorithmic Church Thesis implies that, if a
P-formula [R] is algorithmically true in some interpretation M of P,
then [R] is algorithmically true in every model of P.
(iv) The Algorithmic Church Thesis implies that if a
formula [R] is not P-provable, but [R] is classically true under
the standard interpretation, then [R] is instantiationally true, but not
algorithmically true, in the standard model of P.
(v)
The Algorithmic Church Thesis
implies that Gödel’s undecidable sentence GUS is instantiationally true,
but not algorithmically true, in the standard model of P.
(vi)
A number-theoretic function F(x1, ..., xn) in the standard interpretation M of P is uncomputable
if, and only if, it is effectively computable instantiationally, but not
effectively computable algorithmically.
(vii) If we assume an Algorithmic Church Thesis, then every
partial recursive number-theoretic function F(x1, ..., xn) has a unique constructive extension as a total
function.
(viii) If we assume an Algorithmic
Church Thesis, then the classical Halting problem is effectively
solvable.
(ix)
If we assume an Algorithmic Church
Thesis, then not every effectively computable function is classically Turing
computable (so Turing’s Thesis does not, then, hold).
(x)
If we assume an Algorithmic Church
Thesis, then the class P of polynomial-time languages in the P versus NP problem
may not define a formal mathematical object.
(xi)
Church’s Theorem: The Individual
Church Thesis implies that a number-theoretic function is effectively
computable if, and only if, it is recursive[11].
2.6 Defining formal, constructive and Platonic concepts
(ii) number-theoretic and relations that are
always algorithmically computable / verifiable;
3. Mathematical proof and
non-algorithmic effective methods
Mathematics is a language where proof is the yardstick for
unambiguous expression and communication.
3.1 Non-algorithmic
effective methods: Gödel oracles
(ii)
PA does not prove: [(Ax)R(x)].[14]
In other words, we
may replace the classical Turing Thesis:
(iii)
A number-theoretic predicate F(x), viewed as a Boolean function, is effectively
computable if, and only if, it is classically Turing-computable,
with, for instance,
an Arithmetic Provability Thesis:
(iv)
A PA-string [(Ax)F(x)] is provable if, and only if, in it's standard interpretation M,
the predicate F(x), viewed
as a Boolean function, is classically Turing-computable as true for every
input.
3.2 Defining
Tarskian truth verifiably
(i)
The PA-string [(Ax)F(x)] is true under an interpretation M if, and only if, F(x) is satisfied by every element s of M (i.e. F(s) holds in M).
Now, the three
significant points to note here are that Tarski implicitly assumes:
(ii)
there is some language, accessible
to us, in which F(s) is
expressible for any s of M;
(iii) this is a
language in which we can verify that F(s) holds for any s of M;
(iv)
there is some effective method to
verify that F(s) holds for
any element of M.
Hence, if we
seriously intend to make our mathematical language precise and unambiguous,
then:
(v)
we should introduce these
assumptions explicitly as premises in Tarski's definitions;
(vi) we should specify what we mean by an effective method
that can verify that F(s) holds for any element s of M.
(vii) any
effective method must be an instantiationally effective method;
(viii) we
can only verify that F(s) holds in M by an effective method if every s in M is the interpretation of some symbol [s] of PA.
4.1 CCM’s Thesis and the Halting problem
CCM
Thesis: For arithmetical functions and relations,
Turing-computability is equivalent to PA-provability.
is implicit in the
following remarks ([Ca01],
v2):
4.2 An
effective solution of the Halting problem
We reproduce this argument
below.
Theorem 1: The CCM
Thesis implies that the Halting problem is effectively solvable.
Proof: Given a
Turing machine that computes a number-theoretic function F(x), we note that, by ([Me64],
p233, Corollary 5.13), F(x) is partial recursive. We may thus assume that such an F is
obtained from a recursive function G by means of the unrestricted μ-operator;
in other words, that (cf. [Me64],
p214):