**◄ ***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 19^{th} 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 20^{th} 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*(*x*_{1}, ..., *x _{n}*) 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*(*x*_{1}, ..., *x _{n}*) 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: [(A*x*)*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 [(A*x*)*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 [(A*x*)*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):

Thus, the Halting
problem is effectively solvable if we assume a *CCM Thesis*.

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?

[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>

[Ca01] Calude,
Cristian S., Calude, Elena, and Marcus, Solomon. 2001. *Passages of Proof*.
Workshop, Annual Conference of the Australasian Association of Philosophy (New
Zealand Division), Auckland.

<*PDF
file*: http://arXiv.org/abs/math.
HO/ 0305213>

[Da95] Davis, M. 1995. *Is
mathematical insight algorithmic?*
Behavioral and Brain Sciences, 13 (4), 659--60.

<*PDF
file*: http://citeseer.nj.nec.com/davis90is.html>

[Go31a] Gödel, Kurt.
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.

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

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

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

[Ho00] Hodges, A.
2000. *Uncomputability
in the work of Alan Turing and Roger Penrose.*

<*Unpublished lecture*: 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**.

[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.* Proceedings of the London
Mathematical Society, ser. 2. vol. 42 (1936-7), pp.230-265; corrections, Ibid,
vol 43 (1937) pp. 544-546.

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

[1]
The author is an independent scholar. E-mail: re@alixcomsi.com;
anandb@vsnl.com. Postal address: 32,
Agarwal House,

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

[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 (A*x*)*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*(*x*_{1},
..., *x _{n}*)
is a relation, then its characteristic function,

*C** _{n}*(

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