Some consequences of defining mathematical objects
constructively and mathematical truth effectively
A lay
perspective
Bhupinder
Singh Anand[1]
(A .pdf file of this essay before the current update is available at http://arXiv.org/abs/math.GM/0210078)
Standard expositions of classical first order
theory - rooted primarily in the works of Cantor, Gödel, Tarski, and Turing -
argue that the truth of some propositions of significant formal mathematical
languages, under any interpretation, is non-algorithmic, and essentially
unverifiable constructively. This, implicitly, admits non-constructive elements
into the domain of the interpretation. In this essay, we consider some
arguments for, and consequences of, an interpretation of classical foundational
concepts in which we define mathematical objects constructively, and
mathematical truth effectively.
Contents[2]
1. Introduction
A
formal definition of mathematical objects
An
alternative interpretation of Gödel’s Proof
The
ambiguity in Tarski’s definitions of satisfiability and truth
4. A
meta-theorem of recursive asymmetry
II. Some consequences of defining mathematical
objects constructively
1. Analysing Gödel’s
Theorem XI
Implicit
meta-theses underlying Gödel’s Theorem XI
Gödel’s Theorem XI as a conditional meta-assertion
2. Consistency
and Meta-thesis 3
3. Can
“consistency” be a formal convention?
4. Definitions
of new function and predicate letters
Instantiationally
and algorithmically computable functions
III. Some
consequences of defining mathematical truth effectively
1. Classical definitions
of “satisfiability” and “truth” are ambiguous
Classical definitions of “satisfiability” and “truth”
Expressing Church’s Thesis as an equivalence
2. Constructive definitions of classical
concepts
3. Self-terminating, converging and oscillating
Turing machines
Total
partial recursive functions
The
Arithmetical Provability Thesis and the classical Church-Turing Theses
Converging
NT-routines and Cauchy sequences
4. Turing’s computable and uncomputable numbers
6. Constructivity and classical Quantum
Mechanics
I. The
significance of defining mathematical objects constructively and mathematical
truth effectively
1. Introduction
We begin
our enquiry, by addressing the question: Are the concepts, “non-algorithmic”[3] and “non-constructive”[4], necessarily synonymous in classical[5] logic and mathematics?
We
consider, as a natural starting point, the classical interpretation of the
reasoning and conclusions in Gödel’s seminal 1931 paper [Go31a].
Gödel argues that, in a formal language[6] as basic as Peano Arithmetic[7] - which is considered as the foundation for all,
significant, formal, mathematical languages - there are undecidable[8] sentences[9] that can be recognised as intuitively true[10], under classical interpretation[11], but which are not formally provable[12] within the system.
Does
this imply that such recognition, in some cases, cannot be duplicated in any
artificially constructed and, more important, artificially controlled,
mechanism or organism whose design is based on classical logic?[13]
The
scientific, and philosophical, dimensions of an affirmative answer to the last
question have been broadly reviewed, and addressed, by
Penrose’s
argument is based on a strongly Platonist thesis that sensory perceptions simply
mirror aspects of a universe that exists, and will continue to exist,
independent of any observer ([Pe90], p123, p146)[14].
On this
view, individual consciousness would be a discovery of what there is (cf. [Pe90],
p124), and be independent of the language in which such discovery is expressed.
It follows that recognition of intuitive truth would be individually asserted -
and, implicitly, fallible - correlations between the unverifiable - and, ipso
facto, infallible - intuitive experiences of an individual consciousness, and
the formal expressions of a communicable language.
The
issue, then, is whether classical logic can adequately formalise intuitive
truth, to make it infallible, or whether such recognition is essentially
fallible[15].
Penrose
opts for the inadequacy, of classical logic, to completely capture a Platonic
mathematical reality that, he believes, manifests itself, first, in thought -
which originates in the mind consequent to sensory experience - and, second, in
its representation in a communicable language.
He
supports his view by highlighting the “ethereal” presence, and non-verifiable
properties, of various non-algorithmic ([Pe90], p168), and implicitly
non-constructive, mathematical concepts that are accepted in our formal
languages as essential to classical mathematics ([Pe90],
p123-8).
Although
Penrose’s arguments represent only one, and perhaps an arguably extreme, point
of view[16], they serve to emphasise that classical mathematics
may, yet, need to adequately legitimise the acceptance, into a theory, of
formally definable mathematical objects (cf. [Pe90], p147)[17], most obviously those that can be argued as being
essentially non-constructive.
Now, we
note that Penrose appears to base his thesis on, amongst others, a classical
consequence of Gödel’s reasoning and conclusions: we cannot express Tarskian
definitions[18] of the “satisfiability”, and “truth”, of formal
expressions under an interpretation algorithmically ([Pe90],
p159)[19].
He concludes
from this that, although we may follow a common, intuitive, process for
discovering common, mathematical, aspects of the universe, not all our
mathematically expressible discoveries are expressible by classical algorithms
([Pe90],
p533, p548).
However,
Penrose’s arguments also appear to imply further, albeit implicitly, that our
recognition of intuitive “arithmetical truth” - even when this is accepted as
being adequately formalised by the classical Tarskian definitions of the
“satisfiability” and “truth”, of formal expressions, under an interpretation -
is “absolutely” non-constructive (cf. [Pe90], p145-6).
Thus,
although Penrose does not seem to question the classical expression of Church’s
Thesis[20] ([Pe90], p64-65) as a strong identity -
which, essentially, postulates that every effectively computable function is
algorithmic - he seems to conclude from his arguments, concerning the
inadequacy of classical logic, that there may be non-algorithmic,
non-constructive, ways of acquiring mathematical insight and knowledge ([Pe90],
p538).
As is
evidenced in his discussion of Lucas’ Gödelian argument ([Pe90],
p539), Penrose does not appear to entertain the possibility, that there may be
non-algorithmic reasoning that could be intuitionistically accepted as
constructive; his arguments seem to, implicitly, treat the terms
“non-algorithmic” and “non-constructive” as synonymous[21].
1.2 A formal definition of mathematical objects
In this
essay, however, we argue that what Penrose, for instance, views as the
essentially, and absolutely non-constructive, aspects of mathematical concepts,
may simply be manifestations of a removable ambiguity in the classical
Tarskian definitions of the satisfiability, and truth, of the formulas of a
formal language under an interpretation.
We
argue that this leads to an alternative interpretation of the classical
consequences of Gödel’s seminal 1931 paper [Go31a], with implications for the
foundations of philosophy, logic, mathematics and computability.
We
start by noting that the introduction of classical, non-constructive, objects
into our mathematical ontology - particularly those introduced through
unrestricted definitions[22] - can be qualified by formally defining a set as the
range of a mathematical object that is, itself, a formal mathematical object:
Definition
1(i):
A primitive mathematical object, of a formal mathematical language, L,
is any symbol for an individual constant, predicate letter, or a function
letter (cf. [Me64],
p46; also p1,
p10), which is defined as a primitive symbol of L.
Definition
1(ii):
A formal mathematical object, of a formal mathematical language, L, is
any symbol for an individual constant, predicate letter, or a function letter
that is either a primitive mathematical object of L, or one that can be
introduced through definition (cf. [Me64], p82) into L without inviting
inconsistency[23].
Definition
1(iii):
A mathematical object, of a formal mathematical language, L, is any
symbol that is either a primitive, or a formal, mathematical object of L[24].
Definition
1(iv):
A set, in the domain of any interpretation, M, of a formal mathematical language,
L, is the interpretation of a mathematical object of L that is defined as the
range of a function in M that is, itself, an interpretation of a function
letter that is a mathematical object of L.
The
significance of these definitions is seen in Meta-theorem
1. We prove, there, the existence of an asymmetrical
recursive number-theoretic relation[25]. Such a relation is intuitively decidable constructively,
but cannot be introduced through definition as a formal mathematical object,
into any formal system of Peano Arithmetic, without inviting inconsistency;
nor, ipso facto, into any Axiomatic Set Theory in which the axioms of such
Arithmetic are theorems[26]. Hence, it would not be a formal mathematical object
of the Arithmetic, and the range, of its characteristic function[27], would also not be the interpretation of a formal
mathematical object that defines a (recursively enumerable[28]) set under interpretation!
This is
an astonishing result[29]! First, recursive number-theoretic functions, and
relations, are classically accepted as the basic building blocks for defining
constructive, and intuitionistically unobjectionable, mathematical concepts[30].
Second,
and in vivid contrast, the relative consistency, and independence, of the
Continuum Hypothesis seem to imply, prima facie, that we may also treat
Cantor’s non-constructive cardinal, aleph1, as a valid formal
mathematical object[31] of any Axiomatic Set Theory; thus, we may introduce
axiomatic definitions - and an individual constant symbol - for it into the
theory without inviting inconsistency!
1.3 An alternative interpretation of Gödel’s Proof
Now we
note that, in the proof of Theorem VI of his 1931 paper ([Go31a],
p24), Gödel argues that, in any consistent, formal, system P that formulates
Peano’s Arithmetic, we can construct a valid expression of the system, say [R(x)][32], such that [R(n)] is P-provable for any given numeral [n][33], but [(Ax)R(x)] is not
P-provable.
The
classical interpretation of this is that although [(Ax)R(x)] is not P-provable, it is true under its standard interpretation,
by Tarski’s definitions of satisfiability and truth ([Me64], p51).
We
argue, however, that, by implications that are implicit in Tarski’s
definitions, [R(n)] may be
viewed, alternatively, as an expression whose standard interpretation, R(n), can be effectively asserted as holding instantiationally[34] - and not necessarily algorithmically - for any given
natural number n, but R(x) cannot be effectively asserted as holding uniformly
- in the sense of algorithmically - for all natural numbers x collectively.
1.4 The
ambiguity in Tarski’s definitions of satisfiability and truth
Thus,
we deny the very basis for the above interpretation, of Penrose’s thesis, and
argue that classical interpretations, of Tarski’s definitions of satisfiability
and truth, contain an ambiguity: they implicitly imply the existence of an
ambiguous effective method[35], for deciding whether formal expressions, such as [R(x)], are satisfied under a given interpretation.
Specifically,
they fail to entertain the possibility that such a method may be
non-algorithmic[36]. In other words, for any given value n of its free variable, under a given interpretation,
there may always be a - possibly n-specific - non-algorithmic effective method, which can effectively
decide whether the interpretation, R(n), of a formal expression, such as [R(n)], holds instantiationally, even when there is
no n-independent
effective method that can effectively decide whether the expression [R(x)] is satisfied algorithmically, under a given
interpretation, when we substitute any numeral [n] for its free variable.
We
argue, further, that the above ambiguity is removable, by making the above
possibility explicit in the classical Tarskian
definitions of satisfiability and truth, and by weakening, and expressing, the Church and
Turing Theses as instantiational equivalences rather than as strong
identities.
Clearly,
every classically
Turing-computable number-theoretic function is effectively
computable instantiationally.
Consideration
of the converse leads naturally to the definition of self-terminating,
converging
and oscillating
neo-classical
Turing routines, and an argument that the Church and Turing Theses
may be false, when expressed as strong identities, since we can now define effectively
computable functions that are not classically Turing-computable.
We also
show that Turing’s “uncomputable” real numbers, and Cantor’s “uncountable”
real numbers, do not necessarily correspond to Cauchy sequences of rational
numbers; thus, they cannot be assumed to always define Dedekind real numbers.
In his
1931 paper [Go31a],
Gödel prefaces his Theorem V with the remark ([Go31a], p22):
“The fact which can be vaguely formulated as the
assertion that every recursive relation is definable within the system P (under
its intuitive interpretation), is rigorously expressed by the following
theorem, without reference to the intuitive meaning of the formulas of P.
Theorem V: For every recursive relation R(x1, ..., xn), there is an n-ary PREDICATE[37] r (with the
FREE VARIABLES u1 ... un) such that, for all n-tuples of numbers (x1, ..., xn), we have:
R(x1, ..., xn) => Bew[Sb(r (u1 ... un)|(Z(x1) ... Z(xn)))] (3)
~R(x1, ..., xn) => Bew[Neg Sb(r (u1 ... un)|(Z(x1) ... Z(xn)))] (4)”
In a
footnote, he adds that ([Go31a], footnote 38):
“The VARIABLES u1 ... un can be arbitrarily prescribed. There always exists,
e.g. some r with the FREE
VARIABLES 17, 19, 23, etc., for which (3) and (4) hold.”
He then
qualifies his proof with the remark ([Go31a], p23):
“We shall be content here to indicate the outline of
the proof of this theorem, since it offers no theoretical difficulties and is
fairly tedious.”
In
another footnote, he clarifies that ([Go31a], footnote 39):
“Theorem V depends of course upon the fact that, for a
recursive relation R, it is decidable on the basis of the axioms of the
system P whether or not R holds for any given n-tuple of numbers.”
Since Gödel
does not give a rigorous proof of the theorem, it is not clear whether his
remark - that the recursive relation R(x1, ..., xn) is “... definable within the system P (under its
intuitive interpretation) ...” - means that his reasoning is based on an implicit
assumption that R(x1, ..., xn) is syntactically isomorphic to the standard
interpretation of some PREDICATE r of P.
Such an
assumption would imply that a predicate letter for the n-ary relation “R”, along with suitable defining
axioms, could be introduced into P (cf. [Me64], p82) without inviting
inconsistency.
We
address this issue, and its possible direct, and indirect, consequences, in the
following sections.
In Meta-theorem
1, we consider the elementary, recursive, number-theoretic relation ~xB(Sb(y 19|Z(y))) (cf. [Go31a], p24, def. 8.1), and show that it
is not syntactically isomorphic to the standard interpretation of any[38] of its formal representations[39] in Gödel's system P[40].
In
other words we argue that, if we assume the primitive recursive relation ~xB(Sb(y 19|Z(y))) to be syntactically isomorphic to an abbreviation of
some formula of P, then we arrive at an inconsistency in P.
Intuitively,
this is unexceptionable, since, prima facie, the use of a representation
theorem (cf. [Me64],
Proposition 3.23, p131) in standard derivations (cf. [Me64],
Proposition 3.31, p143) of Gödel's Theorem VI (cf. [Go31a],
p24) appears to be both critical and necessary[41]. Meta-theorem 1 proves the necessity, and
confirms that every primitive recursive function cannot be defined in PA.
We consequently note, in Meta-lemma 1, that we cannot introduce a finite number of arbitrary recursive number-theoretic functions and relations, as function letters and predicate letters respectively, into a formal system of Arithmetic, such as P, without inviting inconsistency. Ipso facto, PA+PRA is inconsistent.
Since both PA and PRA are interpretable in ZF, we note in Corollary 1.1 that Meta-lemma 1 implies that ZF, too, is inconsistent.
We
further note, in Corollary 1.2 to this lemma, that not every
arithmetical relation well-defines a (recursively enumerable) sub-set of the
natural numbers in any Axiomatic Set Theory[42] in which the axioms of P are theorems.
In Corollary
1.3, we, then, note that not every, constructively well-defined,
number-theoretic function is a formal mathematical object of P (so it may not
define a mapping[43] in any Axiomatic Set Theory in which the axioms of P
are theorems).
In Meta-lemma 2,
we define formal equivalence and note that, even if a primitive recursive
relation, and the standard interpretation of its formal representation, are
always equivalent in their instantiations, they are not always formally
equivalent[44].
In §II-1,
§II-2
and §II-3,
we consider the immediate implications of Meta-theorem 1 for the concepts of
intuitive, and formal, consistency, which are based on classical
interpretations of Gödel’s reasoning.
In Meta-theorem
2, we consider, and analyse - independently of Meta-theorem
1 - a semantic argument to the effect that no P-formula asserts,
under the standard interpretation, that P is consistent.
In §II-4,
we note that Meta-theorem
1 implies, first, that every recursive relation is not strongly
representable in P; and, second, that, even if a recursive relation is instantiationally
equivalent to some arithmetical relation, such equivalence cannot always be
formulated within a formal system of Arithmetic such as P (or standard PA).
In §III,
we address a removable ambiguity in Tarski's classical definitions of
“satisfiability” and “truth”.
We then
consider how these definitions can be made constructive, and intuitionistically
unobjectionable, by expressing Church's Thesis as a weak, instantiational,
equivalence, rather than as a strong identity, and supplementing it with an,
intuitionistically unobjectionable, Arithmetical Provability Thesis.
In §III-2,
we introduce some constructive definitions of classical concepts, and offer a
constructive definition of uncomputable number-theoretic functions.
In §III-3,
we define a neo-classical Turing machine NT as a natural, and constructive,
extension of a classical Turing machine T.
We then
introduce definitions for self-terminating, converging
and oscillating
NT-routines, and show that the significance of explicitly defining the truth of
a formula of P under an interpretation in terms of terminating
routines, of expressing Church’s Thesis as an
equivalence, and of defining self-terminating computations of an NT
machine, is expressed by the following meta-lemma:
Meta-lemma 14: If we assume an Arithmetical
Provability Thesis, then every partial recursive number-theoretic
function F(x1, ..., xn) can be constructively extended as a total[45] function.
We
conclude that an Arithmetical Provability Thesis implies,
first, that the classical Halting problem is effectively solvable (Corollary
14.1); and, second, that the classical Church and Turing Theses are
false when expressed as strong identities
In §III-4,
Meta-lemma 17,
and in §III-5,
Meta-lemma 18
and Meta-lemma
19, we then show, respectively, that Turing's and Cantor's diagonal
constructions do not necessarily determine Cauchy sequences[46].
In §III-6,
we, finally, show how the introduction of constructive
definitions, of classical mathematical concepts, may permit formal systems, of
standard Peano Arithmetic, to model some of the more paradoxical concepts of
Quantum Mechanics.
Unless
specified otherwise, we generally follow the notation introduced by Mendelson
in his English translation of Gödel’s 1931 paper [Go31a];
however, for convenience of exposition, we refer to it as Gödel’s notation.
Three notable exceptions: we use the notation “(Ax)”, whose classical, standard, interpretation is “for
all x”, to denote
Gödel’s special symbol for Generalisation; the successor symbol is denoted by “S”,
instead of by “f”; and we use the symbol “¶” to denote the end of a
proof.
Following
Gödel (cf. [Go31a],
footnote 13), we use square brackets to indicate that the expression [(Ax)], including square brackets, only denotes the
uninterpreted string[47] named[48] within the brackets. Thus, [(Ax)] is not part of the formal system P, and would be
replaced by Gödel’s special symbolism for Generalisation wherever it occurs.
Following
Gödel’s definitions of well-formed formulas[49], we note that juxtaposing the string [(Ax)] and the formula[50] [F(x)] is the formula [(Ax)F(x)],
juxtaposing the symbol [~] and the formula [F] is the formula [~F],
and juxtaposing the symbol [v] between the formulas [F] and [G]
is the formula [FvG].
The
number-theoretic functions and relations in the following are defined
explicitly by Gödel [Go31a]. The formulas are defined implicitly by his
reasoning.
3. Definitions
We take
P to be Gödel’s formal system[51], and define ([Go31a], Theorem VI, p24-25):
(i) Q(x, y) as
Gödel’s recursive number-theoretical relation ~xB(Sb(y 19|Z(y)))[52].
(ii) [R(x, y)] as a
formula that represents Q(x, y) in the formal
system P.
(iii) q as the Gödel-number[53] of the formula [R(x, y)] of P.
(iv) p as the Gödel-number of the formula [(Ax)R(x, y)][54] of P.
(v) [p] as the numeral that represents the natural number p in P.
(vi) r as the Gödel-number of the formula [R(x, p)] of P.
(vii) 17Genr as the Gödel-number of the formula [(Ax)R(x, p)] of P.
(viii) Neg(17Genr)[55] as the Gödel-number of the formula [~(Ax)R(x, p)] of P.
(ix) R(x, y) as the
standard interpretation of the formula [R(x, y)] of P.
(x) Wid(P)
as the number-theoretic assertion (Ex)(Form(x) & ~Bew(x))[56].
(We note
that Wid(P) is defined by Gödel ([Go31a],
p36) as equivalent to the meta-assertion “P is consistent”.)
(xi) [Con(P)]
as the formula that represents Wid(P) in the formal system P.
(xii) w as the Gödel-number of the formula [Con(P)] of
P ([Go31a], p37]).
(xiii) Con(P)
as the standard interpretation of the formula [Con(P)] of P.
4. A meta-theorem of recursive asymmetry
Definition 4(i):
A recursive number-theoretic function or relation is asymmetrical in P
if it is not syntactically isomorphic to the standard interpretation of any of
its formal representations in P.
Meta-theorem 1[57]: There is a recursive number-theoretic relation that
is asymmetrical in P.
Proof: We
consider Gödel’s primitive recursive number-theoretic relation ~xB(Sb(y 19|Z(y))).
(a) We
assume that no recursive number-theoretic function or relation is asymmetrical
in Gödel’s system P. In other words, we assume that every recursive
number-theoretic function or relation is syntactically isomorphic to the
standard interpretation of at least one of its formal representations in P[58].
(b) There
is, thus, some P-formula [~xB(Sb(y 19|Z(y)))] whose
standard interpretation is syntactically isomorphic to the primitive recursive
number-theoretic relation ~xB(Sb(y 19|Z(y)))[59].
(c) Now,
in every model M[60] (cf. [Me64], p192-3) of P, we can also interpret[61]:
(i) the
integer 0 as the interpretation of the symbol “0”;
(ii) the
successor operation as the interpretation of the successor function “'”;
(iii) addition
and multiplication as the interpretations of “+” and “.”;
(iv) the
interpretation of the predicate letter = as the identity relation.
(d) Since
the numerals of P interpret as a sub-domain of every model M of P, the natural
numbers are, then, a sub-domain of every M.
(e) Further,
by the hypothesis (a), all of Gödel’s 45 primitive recursive functions
and relations ([Go31a],
p17-22) are also, then, mirrored in every model M of P, and the P-formula, [~xB(Sb(p 19|Z(p)))], always interprets as the M-relation ~xB(Sb(p 19|Z(p))), where [p] is the
numeral that represents the natural number p in P, and p is the Gödel-number of [(Ax)~xB(Sb(y 19|Z(y)))].
(f) Hence,
in every model M of P, the relation ~xB(Sb(p 19|Z(p))) holds in M if, and only if, x is a M-number that is not the Gödel-number of a proof
of [(Ax)~xB(Sb(p 19|Z(p)))] in P.
(g) Further,
since the Gödel-number of a proof of [(Ax)~xB(Sb(p 19|Z(p)))] in P
is necessarily a natural number, ~xB(Sb(p 19|Z(p))) holds in every model M of P if x is an M-number that is not a natural number.
(h) Now,
Gödel has shown (cf. [Go31a], Theorem VI) that ~xB(Sb(p 19|Z(p))) holds over the domain of the natural numbers.
(i) It
follows that ~xB(Sb(p 19|Z(p))) is satisfied
by all x in every model M
of P.
(j) Hence,
the P-formula [(Ax)~xB(Sb(p 19|Z(p)))] is true (cf. [Me64], p51) in every model M of P, and, by
Gödel’s Completeness Theorem ([Me64], Corollary 2.14, p68), [(Ax)~xB(Sb(p 19|Z(p)))] is
P-provable.
However,
since Gödel has shown that [(Ax)~xB(Sb(p 19|Z(p)))] is not
P-provable (cf. [Go31a],
Theorem VI), we conclude that assumption (a) does not hold. This proves
the theorem.
5. Two meta-lemmas
It now
follows that:
Meta-lemma 1:
We cannot introduce a finite number of arbitrary recursive number-theoretic
functions and relations, as function letters and predicate letters
respectively, into P without risking inconsistency.
Proof: Adding “BP”, and a finite number of other functions and relations in terms of which it is defined (cf. [Go31a], p17-22, def. 1-45)[62], as new function letters and predicate letters, respectively, to P, along with associated defining axioms (cf. [Me64], §9, p82), would yield a formal system P' in which, by the arguments of Meta-theorem 1, [~xBP(Sb(y 19|Z(y)))] is true in every model of P', and hence a P'-provable formula[63].
Since all the added functions and relations are primitive recursive, they are strongly represented in P ([Me64], Proposition 3.23, p134).
Every proof sequence
of P' can, thus, be converted into a proof sequence of P ([Me64],
Proposition 2.29, pp82-83). Ergo, [~xBP(Sb(p 19|Z(p)))], hence [(Ax)~xBP(Sb(p 19|Z(p)))], are both
P-provable - contradicting Gödel’s
Theorem VI (cf. [Go31a], p24). This proves the lemma.
Since, classically, both PA and PRA
are interpretable in ZF, we note that:
Corollary 1.1:
Meta-lemma 1 implies that ZF is inconsistent.
Corollary
1.2: There is a primitive recursive number-theoretic
relation such that the values for which it holds do not effectively well-define
a (recursively enumerable ([Me64],
p250)) sub-set of the set of natural numbers in any Axiomatic Set Theory Z (cf.
[Me64],
p192-4) that contains an Axiom of Separation[64], and in which the axioms of P are theorems.
Proof: Let f(x, y) be a recursive
number-theoretic relation, which is expressed in P by the formula [F(x, y)]. We
define the number-theoretic relation t(x) by:
t(x) <=> (Ey)f(x, y).
Since a number-theoretic relation is expressible in P
if, and only if, it is recursive ([Me64], Corollary 3.29, p142), and it can
be shown that t(x) is not
always recursive ([Me64],
Proposition 5.20(5), p251), it follows that t(x) is not always expressible in P.
Assuming that t(x) is not expressible in P, we note that the set T,
defined as {x | t(x)}, is, nevertheless, a well-defined sub-set, of the
set of natural numbers, which is definable in Z. This follows since:
(i) for
any given natural number k, the
standard, arithmetical, interpretation F(x, y) of the
P-formula [F(x, y)] is such that, by definition:
f(x, k) <=>
F(x, k);
(ii) the
set T', defined by {x | t'(x)}, is a well-defined set in Z, where:
t'(x) <=> (Ey)F(x, y);
(iii) by
the Axiom of Separation and (i), {x | t(x)} is a
sub-set of {x | t'(x)}.
It follows that we can add f as a new relation
letter to Z, without inviting inconsistency, where:
u is in {x | t(x)} if, and
only if, (Ey)f(u, y)).
Now, since the axioms of P are theorems of Z, it
further follows that we can also add the relation letter f to P, along
with suitable defining axioms, without inviting inconsistency. However, if we
take f(x, y) as the primitive recursive number-theoretic relation
~xB(Sb(y 19|Z(y))), it follows by Meta-lemma 1 that such addition would
introduce inconsistency into P.
We conclude that the values for which the recursive
number-theoretic relation ~xB(Sb(p 19|Z(p))) holds do
not effectively well-define a (recursively enumerable) sub-set of the set of
natural numbers in Z.
Corollary
1.3: Not every constructively well-defined
number-theoretic relation is a formal mathematical object of P.
It
further follows that, if we define:
Definition 5(i):
Two number-theoretic relations, say f(x) and g(x), are formally equivalent in P if, and only if, the equivalence “f(x) <=> g(x)” is the standard interpretation of some P-formula.
then:
Meta-lemma 2:
Even if a primitive recursive relation, and the standard interpretation of its
formal representation, are always equivalent in their instantiations, they are
not always formally equivalent.
Proof: Let f(x1, ..., xn) be any recursive number-theoretic relation, and F(x1, ..., xn) be the standard interpretation of one of its formal
representations in P.
We assume that the two relations are equivalent in
their instantiations, so that, for any given sequence <a1, ..., an> of natural numbers:
f(a1, ..., an) holds if, and only if, F(a1, ..., an) holds.
However, by Meta-lemma 1, it follows that [f(x1, ..., xn)] is not necessarily a P-formula. Hence, we cannot
conclude that:
[f(x1, ..., xn) <=> F(x1, ..., xn)] is a P-formula.[65]
II. Some consequences of defining
mathematical objects constructively
1. Analysing Gödel’s Theorem XI
Now we
note that Gödel’s number-theoretic relation Bew(x) is defined ([Go31a], p22) in terms of his recursive number-theoretical
relation xBy. The question thus arises:
If we assume that the number-theoretic sentence (Ex)(Form(x) & ~Bew(x)) ([Go31a], p36, footnote 63), abbreviated Wid(P),
defines the proposition “P is consistent” in a constructive and
intuitionistically unobjectionable way[66], then can we consistently assume further that Wid(P)
is syntactically isomorphic to the standard interpretation of some P-formula [Con(P)]?
We note
that the latter assumption is one of the implicit meta-theses that appear to
underlie Gödel’s proof of, and the conclusions he draws from, his Theorem XI ([Go31a], p36).
Clearly,
by Meta-theorem
1 and Meta-lemma
2, such an assumption may be invalid[67].
Thus,
there may be no P-formula, Con(P), whose standard interpretation is
syntactically isomorphic to the number-theoretic assertion (Ex)(Form(x) & ~Bew(x)) - which is defined by Gödel as equivalent to “P is consistent”.
1.1 Implicit
meta-theses underlying Gödel’s Theorem XI
The
question then arises: Is there any P-formula whose standard interpretation can
be defined equivalent to the proposition “P is consistent” in a constructive,
and intuitionistically unobjectionable, way?[68]
In Meta-theorem
2 we address this question by considering a semantic argument that
is based on the assumption that P formalises Dedekind’s Peano Arithmetic[69].
However, we do not appeal to the further thesis that P is
consistent if it has a model, since the consistency of the model may appeal to
set-theoretic reasoning that is non-constructive, and intuitionistically
objectionable, in view of Corollary 1.1 to Meta-lemma 1.
Instead, without assuming the consistency of P, we appeal to
the following four meta-theses, all of
which appear to be implicit in, or consequences of, Gödel’s reasoning in the
proof of his Theorem XI ([Go31a], p36):
Meta-thesis 1:
P is a faithful formalisation of Dedekind’s Peano Axioms.[70]
Meta-thesis 2: If a
sentence [F] is P-provable, then its standard interpretation F is
a true number-theoretic sentence.[71]
Meta-thesis
3: “P is consistent”, abbreviated Wid(P), can be
defined as some number-theoretic sentence in a constructive, and
intuitionistically unobjectionable, way.
Meta-thesis
4: Wid(P) is equivalent to the standard
interpretation, Con(P), of some P-formula [Con(P)].
We now
argue that:
Meta-theorem 2: If we assume that Meta-theses
1-3 are true, then no P-formula can assert P as consistent under the
standard interpretation.
Proof: We assume that Meta-theses
1-4 are true, so that there is some formula [Con(P)] of the
formal system P such that, under the standard interpretation:
Con(P) holds
if, and only if, Wid(P) holds.
We take
this as equivalent, by Meta-thesis 3, to the
assertion:
[Con(P)] is a P-formula that asserts, under the
standard interpretation, that P is consistent.
Now:
(i) By
the classical definition of consistency, [Con(P)] is P-provable if P is
inconsistent - since every formula of an inconsistent P is a consequence of the
Axioms by the Rules of Inference of P[72].
(ii) Further,
if [Con(P)] were P-provable then, by Meta-thesis 2, we would conclude, under the
standard interpretation, that:
Con(P) is a
true number-theoretic sentence.
We would further conclude, by Meta-thesis
3 and Meta-thesis 4, the
meta-assertion:
P is a consistent formal system.
However, this would be an invalid meta-conclusion, since
P may be inconsistent.
(iii) It
follows that we cannot conclude from the P-provability of [Con(P)] that
P is consistent[73]. Hence we cannot have any formula [Con(P)]
such that, under the standard interpretation:
If Con(P) is a true number-theoretic sentence,
then Wid(P) is a true number-theoretic sentence.
(iv) We
conclude that, if Meta-thesis 1-3 are assumed true, then Meta-thesis
4 is false, and there is no P-formula [Con(P)] such that,
under the standard interpretation:
Con(P) is a
true number-theoretic sentence if, and only if, P is a consistent formal
system.
The
question, now, arises: How does Meta-theorem 2 affect Gödel’s
Theorem XI ([Go31a], p36)?
1.3 Gödel’s Proof of Theorem XI
Now,
classically, Gödel’s Theorem XI is interpreted as equivalent to the following
meta-proposition.
Gödel’s
Theorem XI: The consistency of P is not provable in P if P is
consistent.
Proof: Gödel argues
that:
(i) If
P is assumed consistent, then the following number-theoretic assertions follow
from his Theorems V, VI and his definition of Wid(P).
Wid(P) =>
~Bew(17Genr)
Wid(P) =>
(Ax)~xB(17Genr)
17Genr = Sb(p 19|Z(p)))
Wid(P) =>
(Ax)~xB(Sb(p 19|Z(p)))
Q(x, y) <=>
~xB(Sb(y 19|Z(y)))
(x)Q(x, y) <=>
(Ax)~xB(Sb(y 19|Z(y)))
Wid(P) =>
(Ax)Q(x, p)
(ii) Assuming
that [(Ax)R(x, p)] asserts its
own provability, Gödel concludes from the above that the instantiation:
wImp(17Genr),
of the recursive number-theoretic relation xImpy, is a true number-theoretic assertion under the standard
interpretation.
(iii) From
this, he concludes that:
[Con(P) => (Ax)R(x, p)] is P-provable.
(iv) Now,
in his Theorem VI, Gödel argues that, if P is assumed consistent, then [(Ax)R(x, p)] is not
P-provable. He thus concludes that, if P is assumed consistent, then [Con(P)]
too is not P-provable.
(v) Implicitly
assuming that Meta-thesis 4 is true, and so, under the
standard interpretation:
Con(P) is a
true number-theoretic sentence if, and only if, Wid(P) is a true
number-theoretic sentence,
Gödel further concludes that (iv) is equivalent
to asserting that the classical notion of the consistency of P is not provable
in P.
1.4 Gödel’s Theorem XI as a conditional
meta-assertion
However,
since Gödel’s Theorem XI implicitly assumes Meta-theses
1-4, it should be treated, more appropriately, as the conditional
meta-assertion:
If, assuming Meta-theses
1-4[74], there is a P-formula [Con(P)] whose standard
interpretation is equivalent to the assertion “P is consistent”, then [Con(P)]
is not P-provable if P is consistent.
Hence Meta-theorem
2 implies that Gödel’s Theorem XI is a vacuous
meta-assertion.
(a) What
we have essentially argued above is that, for his Theorem XI to hold, Gödel
needs to, first, meta-establish both (i) and (ii):
(i) P
is a consistent formal system
==>[75] “(Ex)(Form(x) & ~Bew(x))” is a true[76] number-theoretic assertion
==> “Con(P)” is a true number-theoretic
assertion
(ii) “Con(P)”
is a true number-theoretic assertion
==> “(Ex)(Form(x) & ~Bew(x))” is a true number-theoretic assertion
==> P is a consistent formal system
Now what Gödel actually meta-argues is (iii)
and (iv):
(iii) P
is a consistent formal system
==> “(Ex)(Form(x) & ~Bew(x))” is a true number-theoretic assertion ... (by
definition)
==> [Con(P)] is not P-provable.
(iv) “(Ex)(Form(x) & ~Bew(x))” is a true number-theoretic assertion
==> P is a consistent formal system ... (by
definition)
From this he implicitly concludes, in Theorem XI,
that:
(v) “P
is consistent” is equivalent to [Con(P)] under the standard
interpretation, and that [Con(P)] is not P-provable.
However, since he does not meta-establish that:
(vi) P is
a consistent formal system
<==> “Con(P)” is a true number-theoretic
assertion
his conclusion in Theorem XI can only be that:
(vii) If
“P is consistent” is equivalent to [Con(P)] under the standard
interpretation, then [Con(P)] is not P-provable.
(b) In Meta-theorem
2 above, we argue, as below, that (a)(vii) holds
vacuously:
(i) Assuming
that P is a faithful formalisation of Dedekind’s Peano Axioms, the axioms of P
are true under the standard interpretation by the classical definitions of
“satisfiability” and “truth” for predicate logic (cf. [Me64],
p50), and the rules of inference preserve truth. Thus, every provable formula
of P is also true under the standard interpretation. It follows that:
[Con(P)] is P-provable ==> “Con(P)”
is a true number-theoretic assertion.
(ii) Now
we have that:
P is an inconsistent formal system ==> [Con(P)]
is P-provable
(iii) If
we, then, assume that:
“Con(P)” is a true number-theoretic assertion
==> P is a consistent formal system
it would follow from (i) that:
[Con(P)] is P-provable ==> P is a consistent
formal system.
(iv) This
is clearly false, since, by (i) and (ii), we may have that:
[Con(P)] is P-provable & P is an
inconsistent formal system[77].
(v) We
conclude that, assuming P is a faithful formalisation of Dedekind’s Peano
Axioms, there is no number-theoretic assertion “Con(P)” such that:
“Con(P)” is a true number-theoretic assertion
==> P is a consistent formal system.
2. Consistency and Meta-thesis 3
Prima
facie, it may seem reasonable to accept Gödel’s assertion - that “P is
consistent” can be defined as equivalent to the number-theoretic sentence (Ex)(Form(x) & ~Bew(x)) - and to assume that this definition is equivalent to the
classical meta-definition of consistency, such as that expressed in Mendelson ([Me64], p57,
Corollary 1.15).
However,
the number-theoretic assertion (Ex)(Form(x) & ~Bew(x)) can be treated as equivalent to the meta-assertion
“P is consistent”, only if we understand it non-constructively to mean:
There is some natural number n for which we can assert that n is the Gödel -number of some formula [F] of P
that is not P-provable.
Now,
since “(Ex)” is only a
shorthand notation for “~(Ax)~” ([Go31a],
p11), the assertion “(Ex)(Form(x) & ~Bew(x))” should actually be read as “~(Ax)~(Form(x) & ~Bew(x))”.
As we
argue in §III,
we can interpret the above constructively, either as the meta-assertion:
(i) It
is not true that, for any given natural number n, there is always a constructive, and
intuitionistically unobjectionable, effective method, which may be dependent on
n, to determine that it is not true that n is the Gödel-number of some formula [F] of P
that is not P-provable.
or, as
the meta-assertion:
(ii) It
is not true that there is an algorithm, necessarily independent of n, to determine that, for any given natural number n, it is not true that n is the Gödel-number of some formula [F] of P
that is not P-provable.
We note
that, although (i) obviously implies (ii), the converse need not
be true. Thus, we cannot assume that the two meta-assertions are necessarily
equivalent.
So
Gödel’s assumption that the number-theoretic sentence (Ex)(Form(x) & ~Bew(x)) is a precise, and intuitionistically unobjectionable, definition
of “P is consistent” is not unambiguous; it can, conceivably, lead to anomalous
consequences.[78]
We note
that a similar ambiguity may exist in the interpretation of the consequences of
Gödel's construction of the recursive relation Q(x, p)[79]; thus, although we can effectively assert that “Q(n, p) holds
instantiationally for any given natural number n”, we cannot, prima facie, assume that this is
equivalent to the non-constructive, infinite, compound, sentence “Q(x, p) holds
algorithmically for all natural numbers x”.
The
distinction between the two assertions is better expressed in terms of
classical, program-terminating, Turing routines[80].
Thus,
given any n, it follows -
from Gödel’s reasoning that [R(n, p)][81] is P-provable - that there is always some effective
method that will terminate in a finite, even if indeterminate, number of steps t(n) if, and only if, R(n, p) holds.
However,
since [(Ax)R(x, p)] is not
P-provable, there may not be any Turing machine such that, given any n, it will halt in a determinate number of steps t(n)[82] if, and only if, R(n, p) holds[83].
In
other words, there may be no classical, program-terminating, Turing routine for
computing the function t(x); in Turing's terminology, t(x) may be Turing-uncomputable, even though t(n) is effectively computable instantiationally for any
given n.[84]
3. Can consistency be a formal convention?
Meta-theorem
2 and §II-2
raise the question: Can we arbitrarily postulate that a formal sentence, under
an interpretation, asserts the consistency of the system?
If so,
the formula expressing such consistency may be in the nature of an impermanent
convention that has intuitive significance only for a transient panel of
mathematical logicians.
That
the issue is not trivial is indicated by Mendelson’s remarks ([Me64],
p148):
“Let Con(S) be the wf: (x1)( x2)( x3)( x4)~(Pf(x1, x3) & Pf(x2, x4) & Ng(x3, x4)).
Intuitively, according to the standard interpretation, Con(S) asserts
that there is no proof in S of any wf and its negation ... .”[85]
Mendelson
then goes on to remark ([Me64],
p149), for a first order theory K that possesses the individual constants of S:
“... the way in which Con(K) is constructed
also adds an element of ambiguity. This ambiguity is dangerous, because ...
there is a reasonable way of defining Con(S) so that Con(S) is
S-provable.”
Mendelson
finally outlines Feferman's formulation of “... a wf expressing the consistency
of K”.
However,
intuitively, this formula no longer even appears related to Mendelson’s
classical, and intuitionistically unobjectionable, notion of consistency ([Me64], p57,
Corollary 1.15).
Without
attempting to address the issue further, we simply note that:
If
these definitions cannot be intuitively interpreted as representing the
classical expression of consistency, then is there a constructive, and
intuitionistically unobjectionable, logical basis by which a formal postulation
can be meaningfully adopted as an effective definition to replace the classical
expression of consistency?[86]
4. Definitions of new function and predicate
letters
Meta-theorem
1 highlights a non-constructive issue underlying Gödel’s reasoning
in his Theorem V.
It
addresses the question: Can every recursive number-theoretic function or
relation be introduced effectively as a formal
mathematical object into P?
The
classical argument is expressed by Mendelson ([Me64], p82, §9):
“In mathematics, once we have proved, for any y1, ..., yn, the existence of a unique object u having the property A(u, y1, ..., yn), we often introduce a new function f(y1, ..., yn) such that A(f(y1, ..., yn), y1, ..., yn) holds for all y1, ..., yn. ... It is generally acknowledged that such
definitions, though convenient, add nothing really new to the theory.”
More
precisely, he argues, in his Proposition
2.29 ([Me64],
p82), that, classically, abbreviations for strongly representable ([Me64],
p118) number-theoretic functions may be introduced as function letters into P,
since they can always be eliminated as follows:
Let K be a first-order theory with equality. Assume
that [(E!u)A(u, y1, ..., yn)][87] is K-provable. Let K' be the first-order theory with
equality obtained by adding to K a new function letter [F] of n arguments, and the proper axiom [A(F(y1, ..., yn), y1, ..., yn)], as well as all instances of the axioms of K
involving [F]. Then:
(i) If
K' is assumed consistent[88], every formula [B] of K' is provably
equivalent to a formula [B'] of K' that does not contain [F].
(ii) If
K' is assumed consistent[89], [B'] is K-provable if, and only if, [B']
is K'-provable.
However,
assuming that every recursive number-theoretic function can be strongly
represented in P[90], Meta-theorem 1 implies that such classical
definitions, as envisaged in Mendelson’s Proposition 2.29, may introduce
inconsistency into a consistent P. Hence K' cannot, then, be assumed
consistent.
We thus
have:
Meta-lemma 3:
If every strongly representable number-theoretic function can be introduced as
a new function letter into P, without affecting the consistency of P, then
every recursive function is not strongly representable in P.
4.2
Non-constructive definitions
Mendelson’s
remarks can be taken as reflecting an implicit, and non-constructive, classical
belief, which his Proposition 2.29 apparently attempts to
formalise explicitly.
This is
that, if we can represent every instantiation of a recursive function
individually in K, it is sufficient to well-define the function as a formal,
mathematical entity in K.
However,
as noted in §II-2,
in order to address this issue in a constructive, and intuitionistically
unobjectionable way, classical arguments may need to explicitly address the
distinction between:
(i) constructing, for any given natural number n, a decision-routine, which may be dependent on n, that terminates in a finite, even if indeterminate,
number of steps on a given condition, and,
(ii) constructing an algorithm that will
terminate in a determinate number of steps on a given condition for any given
natural number n.
4.3 Instantiationally and algorithmically
computable functions
To
highlight the distinction, we assume that [(E!y)R(y, x1, ..., xn)] is P-provable. The classical, non-constructive,
conclusion drawn from this is that:
(i) There
is a unique b in the domain of
the interpretation M of P such that, given any sequence <a1, ...,
an>
in the domain of M, R(b, a1, ...,
an)
holds in M, where R(y, x1, ...,
xn) is
the interpretation of [R(y, x1, ..., xn)] in M.
We may thus define a total function F(x1, ...,
xn) in M
such that, given any sequence <b, a1, ...,
an>
in M:
R(b, a1, ...,
an)
<=> (F(a1, ..., an) = b)
holds in M.
Thus, (i)
assures us, classically, that:
(ii) For
each given sequence <a1, ..., an> in the domain of M, there is some effective
method, which may depend on <a1, ...,
an>,
that will compute a unique b as the
value of F(a1, ..., an) in M in a finite, possibly indeterminate, number of
steps t(a1, ..., an).
However,
the P-provability of [(E!x)R(x, y1, ..., yn)], by itself, does not assure us that there is an
algorithm such that, given any sequence <a1, ...,
an>
in the domain of M, it will compute a unique b, in the domain of M, as the value of F(a1, ...,
an) in a
determinate number of steps t(a1, ...,
an).
In
other words, some sequence <a1, ...,
an> may
require an input-sequence-specific effective method in order to compute F(a1, ...,
an).
Hence,
in the absence of an algorithm, F(x1, ...,
xn) may
be defined as instantiationally, but not algorithmically, computable in M.
(There
is also no assurance of an algorithm that, for any given sequence <a1, ...,
an>,
will compute t(a1, ..., an) in M.)
In view
of the above, a reasonable interpretation of Gödel’s outline of the proof of
Theorem V ([Go31a],
p22) indicates that, it, too, may implicitly rely on non-constructive reasoning
in order to assert the formal existence of a unique formal mathematical object
corresponding to any recursive number-theoretic function or relation.
Classically,
such an assertion would imply that every recursive number-theoretic relation
can either be expressed constructively, and in an intuitionistically
unobjectionable manner, in terms of only symbols that are the interpretations
of the primitive symbols of P, or introduced as a formal
mathematical object into P without inviting inconsistency.
Gödel’s
remarks, both whilst outlining a proof of Theorem V[91], and those at the end of his Theorem VII, indicate that
this may have been his belief at the time.
Such a
belief would imply that the expression “~xB(Sb(y 19|Z(y)))”
can be treated as an abbreviation of one of its representations in P, without affecting
the consistency of P. Meta-theorem 1 implies that any such belief
could be false.
We note
that Gödel’s Theorem VII ([Go31a], p29) asserts that, for any given
set of natural number values of its free variables, every recursive
number-theoretic relation, say F(x), is equivalent to a corresponding instantiation of an
arithmetical[92] relation G(x) (i.e. a relation that uses only “+” and “*” as
primitive arithmetic symbols).
From
this, Gödel apparently concludes that the two relations must also be formally
equivalent. He remarks that ([Go31a], p31):
“According to Theorem VII, for every problem of the
form (x)F(x) (F recursive), there is an equivalent
arithmetical problem, and since the whole proof of Theorem VII can be
formulated (for each particular F) within the system P. this equivalence
is provable in P.”
However, Meta-theorem 1 implies that such a premise may be false. We cannot add Gödel’s first 45 definitions to P - by adding suitable function and predicate letters, and treating their definitions as axioms[93] - without risking inconsistency.
Moreover, in such case, we cannot assume that “the whole proof of Theorem VII could be formulated (for each particular F) within the system P”. It follows that, where Gödel’s reasoning in his Theorems VIII to XI appeals implicitly to the above premise, it might invite inconsistency.
4.6
Standard PA
We also
note that every arithmetical relation is syntactically isomorphic to the
standard interpretation of one of its representations in a formal system of
Arithmetic such as standard PA[94].
Further,
from Meta-Lemma
1 and Meta-lemma
2, we have that:
Meta-lemma 4: Even if a primitive recursive relation is
classically equivalent to some arithmetical relation, in the sense that they
may be always equivalent in their instantiations, such classical equivalence
cannot always be formulated within a formal system of Arithmetic such as
standard PA.
It
follows that Gödel’s Theorems V to XI cannot, therefore, be assumed proven, in
the sense that he intended by his reasoning in [Go31a],
in a formal system of Arithmetic such as standard PA.
III. Some consequences of defining
mathematical truth effectively
1. Classical
definitions of “satisfiability” and “truth” are ambiguous
We next
note that Tarski’s classical definitions, of “satisfiability” and “truth” ([Me64],
p50-52), do not explicitly address the distinction between “instantiationally[95] decidable” relations, and “algorithmically[96] decidable” relations[97].
Thus,
whereas an algorithmically decidable relation is always instantiationally
decidable, Gödel’s recursive number-theoretic relation Q(x, y) may
correspond to an instance where, under a constructive expression of Church's Thesis,
the converse does not hold.
1.1 Classical definitions of
“satisfiability” and “truth”
We note
that the existence of a method to effectively determine that the assertions
involved in the following definitions hold in an interpretation M of the formal
system P, is implicit in Tarski’s classical definitions of the satisfiability
and truth of the well-formed formulas of a formal language under a given
interpretation ([Me64],
p50-51).
In
order to highlight that these definitions must be verifiable by some effective
method, we therefore introduce this condition explicitly as below, and consider
some consequences.
Definition
1(i):
If [R(x1, ..., xn)] is an atomic formula[98] of P, and R(x1, ...,
xn) is
the corresponding relation of the interpretation, then the sequence[99] <a1, ...,
an>
of M satisfies [R(x1, ...,
xn)] classically,
under the interpretation M, if, and only if, there is an effective method to
determine that R(a1, ..., an) holds[100] in M, where a1, ...,
an are
elements in the domain D of M[101].
Definition
1(ii):
If [R] is a formula of P, a sequence s of M satisfies
[~R] classically, under the interpretation M, if, and only if,
there is an effective method to determine that s does not satisfy [R] classically.
Definition
1(iii):
If [R] and [S] are formulas of P, a sequence s of M satisfies
[R=>S] classically, under the interpretation M, if,
and only if, there is an effective method to determine that either s does not satisfy [R] classically, or s satisfies [S] classically.
Definition
1(iv):
If [R] is a formula of P, a sequence s of M satisfies
[(Axi)R]
classically, under the interpretation M, if, and only if, there is an
effective method to determine that every sequence of M, which differs
from s in at most the i’th component, satisfies [R] classically.
We note
that the explicit introduction of effective methods highlights an ambiguity[102] that is implicit in Tarski’s classical definitions.
Thus,
Definition 1(iv) can be understood to mean either of[103]:
Definition
1(iv)(a): If [R] is a formula of P, a sequence s of M satisfies
[(Axi)R]
instantiationally, under the interpretation M, if, and only if, given
any sequence s' of M, which
differs from s in at most the i’th component, there is an effective method, which may depend
on s', to determine that s' satisfies [R] classically.
Definition
1(iv)(b):
If [R] is a formula of P, a
sequence s of M satisfies [(Axi)R] algorithmically, under the
interpretation M, if, and only if, there is an algorithm to determine that,
given any sequence s' of M,
which differs from s in at most
the i’th component, s' satisfies [R] classically.
We
note, here, that:
Meta-lemma
5: 1(iv)(b) ==> 1(iv)(a)
==> 1(iv)[104]
Proof:
Clearly, if there is an algorithm to determine that, given any sequence s' of M, which differs from s in at most the i’th component, s' satisfies
[R] classically, then, trivially, given any sequence s' of M, which differs from s in at most the i’th component, the algorithm determines that s' satisfies [R] classically.
Hence, if 1(iv)(b) holds, then 1(iv)(a)
holds trivially. Since 1(iv) holds if, and only if, either 1(iv)(a)
or 1(iv)(b) holds, the meta-lemma follows.
Definition
1(v):
A formula [R] of P is classically true, for the interpretation M,
if, and only if, there is an effective method to determine that every
sequence of M satisfies [R] classically.
As in
1(iv) above, 1(v) can be taken to mean either of:
Definition
1(v)(a): A formula [R] of P is instantiationally
true, for the interpretation M, if, and only if, given any sequence s of M, there is an effective method, which may depend
on s, to determine
that s satisfies [R]
classically.
Definition
1(v)(b): A formula [R] of P is algorithmically true,
for the interpretation M, if, and only if, there is an algorithm to
determine that, given any sequence s of M, s satisfies
[R] classically.
We
again have:
Meta-lemma
6: 1(v)(b) ==> 1(v)(a)
==> 1(v)
Proof: As in
the previous meta-lemma, if 1(v)(b) holds, then 1(v)(a)
holds trivially. Since 1(v) holds if, and only if, either 1(v)(a)
or 1(v)(b) holds, the meta-lemma follows.
Definition
1(vi):
A formula [R] of P is classically false, for the interpretation
M, if, and only if, there is an effective method to determine that no
sequence of M satisfies [R] classically.
Here,
too, 1(vi) can be taken to mean either of:
Definition
1(vi)(a): A formula [R] of P is instantiationally
false, for the interpretation M, if, and only if, given any sequence s of M, there is an effective method, which may depend
on s, to
determine that s does not satisfy
[R] classically.
Definition
1(vi)(b): A formula [R] of P is algorithmically
false, for the interpretation M, if, and only if, there is an algorithm to
determine that, given any sequence s of M, s does not
satisfy [R] classically.
We also
have:
Meta-lemma
7: 1(vi)(b) ==> 1(vi)(a)
==> 1(vi)
Proof: As
previously, if 1(vi)(b) holds, then 1(vi)(a) holds
trivially. Since 1(vi) holds if, and only if, either 1(vi)(a)
or 1(vi)(b) holds, the meta-lemma follows.
1.2 A constructive expression of Church’s Thesis
Now we
note, first, that definitions 1(iv)(a), 1(v)(a) and
1(vi)(a) are meta-assertions that appeal to the decidability of
an infinity of individual assertions in M, between elements of D that are not
necessarily representable in P as formal mathematical objects.
In the
absence of an effective method for deciding whether an assertion holds individually
in M or not, the definitions are, essentially, non-constructive.
We
note, next, that definitions 1(iv)(b), 1(v)(b) and
1(vi)(b) are also meta-assertions that appeal to the decidability
of infinitely compound assertions in M, between elements of D that are not
necessarily representable in P as formal mathematical objects.
In the
absence of an effective method for deciding whether an infinitely compound
assertion is satisfied uniformly in M or not, these definitions,
too, are, essentially, non-constructive.
We note
also that, if the domain of M is representable in P, then definitions 1(i)
to 1(iii) can be treated as finitely decidable truths.
These
definitions are, then, constructive, and intuitionistically unobjectionable.
The constructiveness of definitions 1(iv) to 1(vi), however,
cannot be assumed even in such a case.
The
question arises:
(*) When may we
constructively assume that, given a relation R in an interpretation M of a
(**) When may we constructively assume that, given a
relation R in an interpretation M of
a
We note
that (*) can be answered constructively if we reformulate the classical Church
Thesis[105] as a weak instantiational, equivalence, instead of as
a strong identity:
Instantiational
Church Thesis: If, for a given relation R(x1, ...,
xn) in
some interpretation M of a Peano Arithmetic, PA, and any sequence <a1, ...,
an>
in M, there is an effective method such that it will
determine whether R(a1, ..., an) holds in M or not, then every element of the domain
D of M is the interpretation of some term of PA, and there is some PA-formula [R'(x1, ..., xn)] such that:
R(a1, ...,
an)
holds in M if, and only if, [R'(a1, ..., an)] is PA-provable.
In
other words, the Instantiational Church Thesis postulates that, if a relation R
is effectively decidable instantiationally (which may be non-algorithmically)
in an interpretation M of a Peano Arithmetic, PA, then R is expressible
in PA, and its domain necessarily consists of only formal
mathematical objects of PA, even if the predicate letter R is
not, itself, the interpretation of a formal
mathematical object of PA.
Moreover,
(**) can be answered constructively if we supplement the weakened Church Thesis
with the postulate:
Arithmetical
Provability Thesis: If, in some interpretation M of a
[R(x)] is PA-provable.
Thus,
the Arithmetical Provability Thesis postulates that, if a total arithmetical
relation R is effectively decidable algorithmically as always true in an
interpretation M of a Peano Arithmetic PA, then the algorithm can be converted
into a proof sequence for [R(x)] in PA.
It
follows from definition 1(v)(b) that:
Meta-lemma 8:
The Arithmetical
Provability Thesis implies that a formula [R] is PA-provable
if, and only if, [R] is algorithmically true in some interpretation
M of PA.
Corollary
8.1: The Arithmetical
Provability Thesis implies that, if there is an algorithm such that
the number-theoretic relation R is satisfied by any sequence s in some interpretation M of a
We also
have the further meta-lemma:
Meta-lemma 9:
The Arithmetical
Provability Thesis implies that, if a PA-formula [R] is algorithmically
true in some interpretation M of PA, then [R] is algorithmically
true in every model of PA.
Corollary
9.1: The Arithmetical Provability Thesis implies
that if a formula [R] is not PA-provable, but [R] is classically
true under the standard interpretation, then [R] is instantiationally
true, but not algorithmically true, in the standard model
of PA.
Corollary
9.2: The Arithmetical Provability Thesis implies
that Gödel’s undecidable sentence ([Go31a], p26) is instantiationally
true, but not algorithmically true in the standard model
of PA.
2. Constructive
definitions of classical concepts
As
suggested by the weakened expression of Church’s Thesis, a more stringent
condition of constructivity would be to postulate that assertions in an
interpretation M of PA are verifiable individually only over elements in the
domain D of M that are representable in PA as formal mathematical objects.
We thus
have the following constructive definitions[106], which correspond to various classical concepts that
involve effective methods that hold instantiationally, but not necessarily
algorithmically.
Definition
2(i):
A relation R(x1, ..., xn) of M is effectively expressible in PA if, and
only if, there is a PA-formula [R'(x1, ..., xn)], with n free variables, such that, for any sequence of numerals <[b], [a1], ..., [an]> of PA, there is an
effective method, which may depend on <b, a1, ..., an>, for determining that:
(i) if R(a1, ...,
an)
holds in M, then [R'(a1, ..., an)] is PA-provable;
(ii) if R(a1, ...,
an) does
not hold in M, then [~R'(a1, ..., an)] is PA-provable,
where <b, a1, ...,
an>
is the interpretation of <[b], [a1], ..., [an]> in M.
We note
that, for any given sequence of numerals <[b], [a1], ..., [an]> of PA, in the absence of an
effective method for determining (i) and (ii), the
concept of “effective expressibility” is, essentially, non-constructive.
Definition
2(ii):
A function F(x1, ..., xn) of M is effectively representable in PA if, and
only if, there is a PA-formula [R(y, x1, ..., xn)], with the free variables [(y, x1, ..., xn)], such that, for any sequence of numerals <[b], [a1], ..., [an]> of PA:
(i) there
is an effective method, which may depend on <b, a1, ...,
an>,
for determining that if (F(a1, ...,
an) = b) holds in M, then [R(b, a1, ..., an)] is PA-provable;
(ii) [(E!y)R(y, a1, ..., an)] is PA-provable,
where <b, a1, ...,
an>
is the interpretation of <[b], [a1], ..., [an]> in M.
We again
note that, for any given sequence of numerals <[b], [a1], ..., [an]> of PA, in the absence of an effective method for
determining (i), the concept of “effective representability” is,
essentially, non-constructive.
Definition
2(iii):
A function F(x1, ..., xn) of M is strongly representable effectively in
a formal system P if, and only if, there is a P-formula [R(y, x1, ..., xn)], with the free variables [(y, x1, ..., xn)], such that:
(i) for
any sequence of numerals <[b], [a1], ..., [an]> of P, there is an effective method, which may
depend on <b, a1, ...,
an>,
for determining that if (F(a1, ...,
an) = b) holds in M, then [R(b, a1, ..., an)] is P-provable;
(ii) [(E!y)R(y, x1, ..., xn)] is P-provable,
where <b, a1, ...,
an>
is the interpretation of <[b], [a1], ..., [an]> in M.
We note
that, here also, for any given sequence of numerals <[b], [a1], ..., [an]> of P, in the absence of an effective method for
determining (i), the concept of “effectively strong representability”
is, essentially, non-constructive.
Definition
2(iv):
A relation R(x1, ..., xn) in M is effectively definable in a formal
system P if, and only if, [R(x1, ..., xn)] is a P-formula such that, for any sequence of
numerals <[a1], ..., [an]> of P, there is an effective method, which may depend
on <a1, ..., an>, for determining that:
(i) if R(a1, ...,
an)
holds in M, then [R(a1, ..., an)] is P-provable;
(ii) if R(a1, ...,
an) does
not hold in M, then [~R(a1, ..., an)] is P-provable,
where <a1, ...,
an>
is the interpretation of <[a1], ..., [an]> in M.
Meta-lemma 10:
If a relation R of M is effectively definable in P, then it is
syntactically isomorphic to the interpretation of one of its representations in
P. (Although the converse holds if M is the standard model, it need not be true
for every model.)
We note
that, for any given sequence of numerals <[b], [a1], ..., [an]> of P, in the absence of an effective method for
determining (i) and (ii), the concept of “effective definability”
is also, essentially, non-constructive.
Definition
2(v): A
number-theoretic function F(x1, ...,
xn) is effectively
computable instantiationally in an interpretation M of a
Definition
2(vi):
A number-theoretic function F(x1, ...,
xn) is effectively
computable algorithmically in an interpretation M of a
Meta-lemma 11:
If a number-theoretic function F(x1, ...,
xn) is
effectively computable algorithmically in an interpretation M of a Peano
Arithmetic PA, then it is effectively computable instantiationally in
M.
Proof: The
lemma is trivially true, by definition.
Definition
2(vii): A number-theoretic function F(x1, ..., xn) in the standard interpretation M of a
Definition 2(viii): A number-theoretic function F(x1, ...,
xn) is
an omega-function in an interpretation M of a Peano Arithmetic PA if,
and only if, there is a PA-formula [R(y, x1, ..., xn)], with the free variables [(y, x1, ..., xn)], such that:
(i) for
any sequence of numerals <[b], [a1], ..., [an]> of PA, there is an effective method, which may
depend on <b, a1, ...,
an>,
for determining that, if (F(a1, ...,
an) = b) holds in M, then [R(b, a1, ...,
an)] is
PA-provable, where <b, a1, ...,
an>
is the interpretation of <[b], [a1], ..., [an]> in M;
(ii) for
any sequence of numerals <[b], [a1], ..., [an]> of PA, there is an effective method, which may
depend on <b, a1, ...,
an>,
for determining that [(E!y)(R(b, a1, ...,
an))] is
PA-provable;
(iii) [(E!y)(R(y, x1, ...,
xn))] is
not PA-provable,
where <b, a1, ...,
an>
is the interpretation of <[b], [a1], ..., [an]> in M.
We thus
have:
Meta-lemma 12:
An omega-function F(x1, ...,
xn) in
an interpretation M of a
3.
Self-terminating, converging and oscillating Turing machines
We note
that classical Turing machines ([Me64], p229) are constructive, in the
sense of §III-2,
to the extent that:
Meta-lemma 13:
If a total function F(x1, ...,
xn) is
classically Turing-computable[107] in the standard interpretation M of a
Proof: Since
the domain of M is representable in PA, a number-theoretic function is
representable (cf. [Me64],
p118) in PA if, and only if, it is effectively
representable in PA (cf. §III-Def. 2(ii)).
Now, if a total number-theoretic function F(x1, ...,
xn) is
classically Turing-computable in the standard interpretation M of PA, then it
is recursive ([Me64],
p233, Corollary 5.13).
Since every recursive function is representable in PA
([Me64],
p131, Proposition 3.23), it follows by §III-Def.
2(v) that F(x1, ...,
xn) is
effectively computable instantiationally in M.
We next
define a neo-classical Turing machine NT as a natural, and essentially
constructive, extension of a classical Turing machine T.
We
introduce the concept of a neo-classical, self-terminating, Turing routine, and
note some significant consequences of the difference between such routines and
classical, program-terminating[109], Turing routines. We begin by recalling Mendelson’s
description ([Me64],
p229) of the operations of T:
(a) There
is a two-way, potentially infinite[110], tape divided up into squares. There is a finite set
of tape symbols S0,
S1, ..., Sn called the alphabet
of the machine; at every moment, each square of the tape is occupied by at most
one symbol. The machine has a finite set of internal states {q0, q1, ..., qm}. At any given moment, the machine is in exactly one
of these states. Finally, there is a reading head which, at any given time,
stands over some square of the tape. The machine does not act continuously, but
only at discrete moments of time. If, at any moment t, the reading head is scanning a square containing a
symbol[111] Si, and the machine is in the internal state qj, then the action of the machine is determined, and it
will do one of four things:
(i) it
may erase the symbol Si and print a new symbol Sk;
(ii) it
may move left one square;
(iii) it
may move right one square;
(iv) it
may stop. In cases (i)-(iii), the machine goes into a new
internal state qr, and
is ready to act again at time t+1.
(b) The
actions (a)(i) to (a)(iii) can be represented by quadruples:
(i) qjSiSkqr;
(ii) qjSiLqr;
(iii) qjSiRqr,
where the first two symbols stand for the present
internal state and scanned symbol, the third symbol represents the action of
the machine, and the fourth symbol gives the internal state of the machine
after the action has been performed.
(c) If a
tape is put into a Turing machine and the reading head is placed on a certain
square, and if the machine is started off in one of its internal states, then
the machine begins to operate on the tape: printing and erasing symbols and
moving from one square to an adjacent one. If the machine ever stops, the
resulting tape is said to be the output
of the machine applied top the given tape.
(d) We
can associate with any Turing machine T the following algorithm B in the
alphabet A of T. Take any word P of the alphabet A and print it from
left to right in the squares of an empty tape. Place this tape in the machine
with the reading head scanning the left-most square. Start the machine in the
internal state q0. If the machine ever stops, the word of A appearing
on the tape is the value of the algorithm B. B is called a Turing algorithm.
(e) A classical Turing machine T is
then defined precisely as a finite set of quadruples of the three kinds (b)(i)
to (b)(iii), where no two quadruples have the same first two
symbols.
(f) An instantaneous tape description
of a Turing machine T is a word such that:
(i) all
symbols in the word but one are tape symbols Sm;
(ii) the
only symbol which is not a tape symbol is an internal state qs;
(iii) qs is not the last symbol of the word.[112]
(g) We
say that T moves one
instantaneous tape description alpha into another one beta[113] if, and only if:
(i) either,
alpha is of the form PqjSiQ, beta
is of the form PqrSkQ, and qjSiSkqr is one of the quadruples of T;
(ii) or,
alpha is of the form PSsqjSiQ, beta
is PqrSsSiQ, and qjSiLqr is one of the quadruples of T;
(iii) or,
alpha is of the form qjSiQ, beta
is qrS0SiQ, and qjSiLqr is one of the quadruples of T;
(iv) or, alpha
is of the form PqjSiSkQ, beta
is PSiqrSkQ, and qjSiRqr is one of the quadruples of T;
(v) or, alpha
is of the form PqjSi, beta is PSiqrSo, and qjSiRqr is one of the quadruples of T.[114]
(h) We
say that T stops[115] classically
at an instantaneous tape description alpha if, and only if, there is no
instantaneous tape description beta into which T can move alpha.
(j) A classical computation of
a Turing machine T is a finite sequence of instantaneous tape descriptions alpha0,
alpha1, ..., alpham (m >= 0)
such that:
(i) the
internal state occuring in alpha0 is q0;
(ii) for
0 =< i < m, alpha(i+1)
follows alphai;
(iii) there
is no instantaneous tape description alpha(m+1) into
which T can move alpham;
(iv) and T stops at alpham.
(k) The algorithm BT,C
in any alphabet C containing the alphabet A of T is defined as follows:
For any words P, Q in C, BT,C(P)
= Q if, and only if, there is a classical computation of T which begins
with the instantaneous tape description q0P and ends with an instantaneous tape description of
the form R1qjR2, where Q = R1R2.
(l) An
algorithm U in an alphabet D is called classically Turing-computable
if, and only if, there is a Turing machine T with alphabet A and an alphabet C
containing A+D[116] such that BT,C and U are
fully equivalent relative to D.
(m) Given
a partial number-theoretic function F(x1, ...,
xn), we
say that a Turing machine T (whose alphabet A includes {1, *}) computes F
if, and only if, for any natural numbers k1, k2, ... kn, and any word Q, BT,A(k1* k2* ... * kn) = Q if, and only if, Q is R1F(x1, ...,
xn)R2,
where both R1 and R2 are certain, possibly
empty, words consisting only of S0’s.[117]
3.2
Neo-classical Turing machines
We now define a broader class of neo-classical Turing
machines NT as follows:
(a) A
neo-classical Turing machine NT is a classical Turing machine T that also stops
if an instantaneous tape description repeats itself.[118]
(b) A self-terminating
computation of an NT machine is a finite sequence of instantaneous tape
descriptions alpha0, alpha1, ..., alpham (m >= 0) such
that:
(i) the
internal state occuring in alpha0 is q0;
(ii) for
0 =< i < m, alpha(i+1)
follows alphai;
(iii) alpham is a repetition of alphai for some 0 =< i < m;
(iv) NT
stops at alpham.[119]
(c) We call
classical Turing-computations as program-terminating NT-routines,
and neo-classical Turing-computations as terminating NT-routines.
(d) The instantaneous
tape output of an NT machine is the word obtained by deleting the symbol for
the internal state of the machine from the instantaneous tape description.
(e) The number of
tape symbols in an instantaneous tape output of an NT machine is called the output
length of the instantaneous tape description.
(f) For all 0
=< i =< m, the finite integer i is defined as the configuration number of an instantaneous
tape output corresponding to the instantaneous tape description alphai of an NT machine.
(g) The terminal
tape output of an NT machine is the word obtained by deleting the symbol for
the internal state of the machine from the final instantaneous tape description
of a terminating NT-routine.
(h) An NT-routine
is non-terminating if, and only if, it is not a terminating NT-routine.
(j) A
non-terminating NT-routine is a converging NT-routine if, and
only if, there is a positive integer n0 such
that, given any natural number n > n0, there is a minimum configuration number nmin such that, for any given configuration number m > nmin, the instantaneous tape description is of the form PqjSiQ where P
is a word in the alphabet A of NT that contains more than n tape symbols.
(k) We call a
non-terminating NT-routine an oscillating NT-routine if, and only
if, it is not a converging NT-routine.
3.3 Total
partial recursive functions
The
significance, of explicitly defining the truth of a formula of P under
interpretation in terms of effective methods, of weakening
Church’s Thesis and supplementing it with an Arithmetical
Provability Thesis, and of defining self-terminating
computations of an NT machine, is expressed by the following
meta-lemmas.
Meta-lemma
14: If we
assume an Arithmetical Provability Thesis, then every
partial recursive[120] number-theoretic function F(x1, ...,
xn) can
be constructively extended as a total function.
Proof: We
assume that F is obtained from the recursive function G by means
of the unrestricted μ-operator, so that F(x1, ...,
xn) = μy(G(x1, ...,
xn, y) = 0).
If [H(x1, ...,
xn, y)] expresses ~(G(x1, ...,
xn, y) = 0) in a
(We note that, if we define the truth of a formula of
PA, under an interpretation M, explicitly in terms of effective methods that
are appropriate to M[121], a formula such as [(Ax)F(x)] does not interpret as a compound number-theoretic assertion
about the range of values of M for which [F(x)] is satisfied in M, but as a meta-assertion that,
for any given a of M, there is an
effective method that is appropriate to M, which may depend on a, and which can determine that F(a) holds in M.)
We now consider the argument:
(a) Let Q1
be the meta-assertion that [H(a1, ...,
an, y)] is not classically
true in M. Hence there is no algorithm in M that, for any given y in M, will determine that y satisfies [H(a1, ...,
an, y)] classically.
Since G(a1, ...,
an, y) is recursive, it follows that there is some finite k such that any neo-classical Turing machine NT1(y) that computes G(a1, ...,
an, y) will halt and return the value 0 for y = k.
(b) Next,
let Q2 be the meta-assertion that [H(a1, ...,
an, y)] is classically true in the standard
interpretation M of P, but that there is no algorithm in M that, for any given y in M, will determine that y satisfies [H(a1, ...,
an, y)] classically.
Since G(a1, ...,
an, y) is recursive, it follows that there is some finite k such that any neo-classical Turing machine NT2(y) that computes the arithmetical function H(a1, ...,
an, y) will halt, and return the symbol for
self-termination, for y = k.
(c) Finally,
let Q3 be the meta-assertion that [H(a1, ...,
an, y)] is classically true in the standard
interpretation M of PA, and that there is an algorithm in M such that, for any
given y in M, it will
determine that y satisfies [H(a1, ...,
an, y)] classically. We then have that that [H(a1, ...,
an, y)] is algorithmically true in the standard
interpretation M of P
If we assume an Arithmetical
Provability Thesis, then, by Meta-lemma 8, it follows that [H(a1, ...,
an, y)] is PA-provable. Let h be the Gödel-number of [H(a1, ...,
an, y)].
We consider, then, Gödel’s recursive number-theoretic
relation xBy, which holds in M if, and only if, x is the Gödel-number of a proof sequence in PA for the
PA-formula whose Gödel-number is y.
It follows that there is some finite k such that any neo-classical Turing machine NT3(y), which computes the characteristic function[122] of xBh, will halt and return the value 0 for x = k[123].
Since Q1, Q2, and Q3
are mutually exclusive and exhaustive[124], it follows that, when run simultaneously[125] over the sequence 1, 2, 3, ... of values for y, one of the parallel trio {NT1(y) // NT2(y) // NT3(y)} of neo-Turing machines will always halt for some
finite value of y.
If NT1(y) halts at y = k, and returns the value
0, we define F'(a1, ..., an) = F(a1, ...,
an).
If NT2(y) halts and returns the symbol for self-termination,
or if NT3(y) halts, we
define F'(a1, ..., an) = 0.
Hence, under the given hypothesis, there is always a
constructive extension of every partial recursive function F(x1, ...,
xn) as a
total function F'(x1, ..., xn).
Since
every Turing-computable function F is partial recursive, and, if F
is total, then F is recursive ([Me64], Corollary 5.13, p233), it follows
from Meta-lemma 14 that:
Corollary
14.1: The classical Halting problem is effectively
solvable if we assume an Arithmetical Provability Thesis.
3.4 The Arithmetical Provability Thesis and the
classical Church-Turing Theses
We now
consider the significance of constructively defining instantiational
and algorithmic effective methods for the two classical theses:
Classical Turing Thesis: Every effectively computable function is classically
Turing computable ([Me64], p237).
We note
that, classically, the two theses are accepted as equivalent since the Turing
machine approach to effective computability is equivalent ([Me64],
p237) to that by means of normal algorithms ([Me64], p209), or by recursive functions.
Now, we
can express the Turing Thesis alternatively in terms of instantiational and
algorithmic effective methods:
Alternate Turing Thesis: A function is classically
Turing computable if, and only if, it is computable[126] either by an instantiational
effective method, or by an algorithmic
effective method.
We also
note that the classical Turing Thesis - that every effectively computable
function is classically Turing computable ([Me64],
p237) - implies the:
Secondary
Turing Thesis: If a number-theoretic function F(x1, ...,
xn) is effectively
computable instantiationally in the standard interpretation M of a
However,
if some, classically-defined, partial recursive function can be constructively
computed as a total function, in the sense that it is effectively
computable instantiationally in the standard interpretation M of PA,
as in the argument in Meta-lemma 14, then it follows that the
classical Turing Thesis may be false, since:
Corollary
14.2: If we assume an Arithmetical
Provability Thesis, then not every effectively computable function
can be assumed as classically Turing computable.[127]
Proof: Meta-lemma 14
gives an effective method, corresponding to a constructive Turing “oracle”[128], for determining whether a classical Turing machine
will halt or not. Hence, by the classical Halting argument, it does not define
a classical Turing machine.
Since
the Instantiational
Church Thesis implies the classical Church’s Thesis, it further
follows that:
Corollary
14.3: If we assume an Arithmetical
Provability Thesis, then not every (partially) recursive function is
classically Turing-computable.
3.5 Converging NT-routines and Cauchy sequences
We next
note that:
Meta-lemma
15: If the alphabet A of NT consists of only the
numerals “0” and “1”, then every converging NT-routine defines a Cauchy
sequence[129] of rational numbers.
Proof: If B
is a converging
NT-routine, then there is a positive integer n0 such that,
given any positive integer n > n0, there
is a minimum configuration number nmin of output length n such that:
(i) the
instantaneous
tape description whose configuration number is nmin+1 is of the form Pn+1qjSiQ, where Pn+1 is a
binary string of length (n+1);
(ii) the
instantaneous
tape description whose configuration number is k > nmin+1 is of the form Pn+1PmqjSiQ where Pm is either the null string, or a binary string of
finite, non-zero, length.
We thus have the Cauchy sequence {P'0,
P'1, ..., P'n, ...}, where P'n is obtained by prefacing a decimal point to the start
of the string Pn, and
is thus the binary form of a rational number between 0 and 1.
Corollary 15.1: If
the alphabet
A of an NT
machine consists of only the numerals “0” and “1”, a Cauchy sequence
such as {P'0, P'1, ..., P'n, ...} may not be constructible if the instantaneous
tape outputs of an NT machine define an oscillating,
non-terminating, NT-routine.[130]
Meta-lemma
16: Every number-theoretic function that is effectively
computable instantiationally in the standard interpretation M of P
defines a Cauchy sequence.
Proof: If a
function F(x1, ..., xn) of M is effectively
computable instantiationally in M, then it is effectively
representable in P. Hence there is a P-formula [R(y, x1, ..., xn)], with the free variables [(y, x1, ..., xn)], such that, for any sequence of numerals <[b], [a1], ..., [an]> of P, [(E!y)R(y, a1, ..., an)] is P-provable.
The denumerable sequences <[b], [a1], ..., [an]> of P can be put into a 1-1 correspondence with
the natural numbers. We thus have:
k <=> <Sk>
for any given natural number k, where <Sk> is a sequence of numerals <[s1], ..., [sn+1]> of
P.
If we define the number-theoretic function rk such that rk = 0 if, and only if, [R(s1, s2, ..., sn+1)] is
P-provable, and rk
= 1 otherwise, we obtain the Cauchy sequence:
(0. r1), (0. r1 r2), (0. r1 r2 r3), ...,
(0. r1 r2 r3 ... rk), ...
Corollary 16.1:
By Meta-lemma
11, it follows that every function that is effectively
computable algorithmically in M defines a Cauchy sequence.
Definition 3(i): We define the sequence:
(0. r1), (0. r1 r2), (0. r1 r2 r3), ...,
(0. r1 r2 r3 ... rk), ...
as the characteristic
Cauchy sequence of the function F(x1, ...,
xn)
under the 1-1 correspondence k <=> <Sk>.
3.6 The P
versus NP problem[131]
We now
consider an argument that, by Corollary 1.2 to Meta-lemma 1,
the definition[132] of the class P of polynomial-time languages in the P
versus NP problem may not define a formal
mathematical object of a formal first order predicate calculus.
Definition 3(ii):
Let A be a finite alphabet (that is, a finite non-empty set) with at least two
elements, and let A* be the set of finite strings over A. The language L(T),
accepted[133] by the classical Turing machine whose description
number is T[134], is defined by:
L(T) = {w is in A* | T accepts w}.
We denote by tT(w) the number of
steps in the computation of T on input w. For any given natural number n, we define the worst case run time of T as:
TT(n) = max{tT(w)
| w is in An},
where An is the set of all strings over A of length n. We say that T runs in polynomial time if there
exists a k such that, for
all n, TT(n) =< nk + k. We then
define the class P of languages by:
P = {L | L = L(T) for some Turing machine T which runs
in polynomial time}.
Is P a formal
mathematical object of any formal, first order, predicate calculus
such as, say, PA?
Assuming
that TT(n) is
well-defined[135], we can define a number-theoretic relation F(T,
k, n) that
holds if, and only if, TT(n) =< nk + k.
Clearly,
if the alphabet A is of length l, there are a maximum of ln possible strings of length n. Hence, for a given T, TT(n) is effectively computable individually in the
standard interpretation M of PA.
It
follows that, for a given T and k, and any given natural number n, there is always an effective method, which may depend
on n, to determine
whether the number-theoretic relation F(T, k, n) holds.
However,
there may not be any algorithm to determine whether, for any given T and k, F(T, k, n) holds for any
given natural number n.
In
other words, in the absence of a specific proof, we cannot conclude that F(T,
k, n) is effectively
definable in the standard interpretation of any standard,
first-order, predicate calculus such as PA; nor, in view of Meta-lemma 10,
that F(T, k, n) necessarily defines a formal
mathematical object.
Prima
facie, there are also no grounds for concluding that the language L(T) defines
a formal
mathematical object of PA; ipso facto, we cannot conclude, without
specific proof, that the class, P, of languages defined by:
P = {L | (ET)(L = L(T) & (Ek)(An)F(T,
k, n))},
is a formal
mathematical object in any formal, first-order, predicate calculus
such as PA.
4. Turing’s
computable and uncomputable numbers
In his
seminal 1936 paper [Tu36],
Turing did not explicitly define computable (real) numbers, but chose to
variously describe their properties in terms of Turing machines as below.
However, as we note in Corollary 17.1, Turing’s assumption that
every “circle-free” machine necessarily defines a Dedekind[136] real number is invalid.
(a) The
“computable” numbers may be described briefly as the real numbers whose
expressions as a decimal are calculable by finite means. ... A number is
computable if its decimal can be written down by a machine.
(b) If
an a-machine prints two kinds of symbols, of which the
first kind (called figures) consists entirely of 0 and 1 (the others being
called symbols of the second kind), then the machine will be called a computing
machine.
If the machine is supplied with a blank tape and set
in motion, starting from the correct initial m-configuration, the subsequence of the symbols printed
by it which are of the first kind will be called the sequence computed
by the machine.
The real number whose expression as a binary decimal
is obtained by prefacing this sequence by a decimal point is called the number computed by
the machine.
(c) If
a computing machine never writes down more than a finite number of symbols of
the first kind it will be called circular. Otherwise it is said to be circle-free. ... A machine will be circular if it reaches a
configuration from which there is no possible move, or if it goes on moving,
and possibly printing symbols of the second kind, but cannot print any more
symbols of the first kind.
(d) A
sequence is said to be computable if it can be computed by a circle-free
machine. A number is computable if it differs by an integer from the number
computed by a circle-free machine.
(e) A
computable sequence O is determined
by a description (number) of a machine which computes O.
(f) To
each computable sequence there corresponds at least one description number,
while to no description number does there correspond more than one computable sequence.
The computable sequences and numbers are therefore enumerable. A number which
is a description number of a circle-free machine will be called a satisfactory
number.
(g) The
expression “there is a general process for determining …” has been used throughout
this section as equivalent to “there is a machine which will determine …”. This
usage can be justified if and only if we can justify our definition of
“computable”. For each of these “general process” problems can be expressed as
a problem concerning a general process for determining whether a given integer n has a property G(n) [e.g.
G(n) might mean “n is satisfactory” or “ n is the Gödel representation of a provable formula”],
and this is equivalent to computing a number whose n-th figure is 1 if G(n) is true and 0 if it is false.
(h) The
computable numbers do not include all (in the ordinary sense) definable
numbers. Let P be a sequence whose n-th figure is 1 or 0 according as n is or is not satisfactory. It is an immediate consequence
of the theorem of §8 that P is not computable.
Meta-lemma 17:
Turing’s sequence P in the above definition does not necessarily
determine a Cauchy sequence.
Proof: By
Turing’s argument in §8 of his 1936 paper [Tu36], P is not effectively
computable algorithmically in the standard interpretation M of any
formal system of Arithmetic. Hence, either P is effectively
computable instantiationally in M such that some sub-sequence Pn of P is self-terminating
or, by the Corollary 15.1 to Meta-lemma 15,
the sequence P may define an oscillating NT-routine.
Corollary 17.1:
Turing’s argument in §8 of his 1936 paper [Tu36] does not establish the existence of a
(classically uncomputable) Dedekind real number[137].
(j) It
is (so far as we know at present) possible that any assigned number of figures
of P can be calculated, but not by a uniform process. When sufficiently
many figures of P have been calculated, an essentially new method is
necessary in order to obtain more figures.
(In
other words, P may be effectively computable instantiationally,
but not effectively computable algorithmically, in any standard
interpretation of a formal system of Arithmetic.)
A
similar argument applies to Cantor’s diagonal construction of an uncountable
set of real numbers. Cantor’s classical argument[138] only establishes that there is no algorithm for
determining a 1-1 correspondence between the natural numbers and the real
numbers between 0 and 1.
However,
there still may be an instantiational effective method for
determining a 1-1 correspondence between the natural numbers and the real
numbers between 0 and 1.
In this
case, any algorithm that computes the sequence whose n-th digit is 1 if the n-th digit in the binary expression of the real number
corresponding to n is not 1,
and 0 otherwise, may include a self-terminating computation of an NT
machine, or it may correspond to an oscillating NT-routine. In such a case, the
routine would not define a Dedekind real number.
We thus
have:
Meta-lemma 18:
We cannot conclude that the Dedekind real numbers are uncountable by Cantor’s
diagonal argument.
Moreover,
if we accept the classical definition of a number as real if, and only if, it
is the limit of a Cauchy sequence[139] of rational numbers[140], and that of a sequence of rationals as a function
whose domain is the integers, and whose range is the rationals (i.e., the
function defining the sequence is a mapping from the integers into the
rationals), then Cantor’s diagonal argument simply shows that some real numbers
are generated by classically uncomputable functions that are
not effectively
computable algorithmically.
However,
since, constructively, the function must be effectively
computable instantiationally, and there can only be denumerable effectively
computable functions[141], it follows that:
Meta-lemma 19: Under constructive extensions of Tarski’s
definitions of the satisfiability and truth of the propositions of a
formal mathematical language, P, under an interpretation, and a weakened Church’s
Thesis, the real numbers are denumerable (hence Cantor’s Theorem[142] does not hold).
6. Constructivity
and classical Quantum Mechanics
The
introduction of constructive definitions of classical mathematical concepts may
permit formal systems of standard Peano Arithmetic to model some of the more
paradoxical concepts of Quantum Mechanics. For instance, consider the following
argument:
(a) Gödel has proved in his 1931 paper [Go31a]
that there is a formula [R(x)] such that, for any given natural number k, [R(k)] is provable in any formal system of Arithmetic such as standard
PA.
(b)
Hence, for any given k,
there is always some effective
method for evaluating the arithmetic expression R(k) in the standard interpretation M of PA.
(c) Gödel has also proved in the above paper that [(Ax)R(x)] is not PA-provable.
(d)
Thesis: There is no algorithm that can evaluate the
arithmetic expression R(n) for any given n in M. (We note that (d) is a consequence of Corollary
9.2)
(e)
Thus, R(n) is instantiationally computable, but not
algorithmically computable.
(f) Theorem (provable by induction): For any given k, we can always define, using Gödel’s
Beta-functions, some algorithm 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.
This follows since, clearly, 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, first, to the act of finding a suitable method of
measuring the value R(k) precisely, and, second, 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 algorithm 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.
[Cook] Cook, S. The
P versus NP Problem. Official description provided for the Clay Mathematical
Institute,
<http://www.claymath.org/millennium/P_vs_NP/Official_Problem_Description.pdf>
[Ch95] Chalmers, D.
1995. Minds, Machines, And Mathematics, para 2.5, Psyche, Vol. 2(9), June 1995.
<Web page: http://psyche.cs.monash.edu.au/v2/psyche-2-09-chalmers.html>
[Da90]
<
[Go31a] Gödel, Kurt.
1931. On formally undecidable propositions of Principia Mathematica and
related
[Go31b] Gödel, Kurt.
1931. On formally undecidable propositions of Principia Mathematica and
related
<Web page: http://home.ddc.net/ygg/etext/godel/index.htm>
[Go47] Gödel, Kurt. 1947. What is Cantor's
continuum problem? Amer. Math. Monthly 54 (1947), 515-525; errata 55, 151;
Revised and expanded version, in Philosophy of Mathematics: Selected Readings,
P. Benacerraf and H. Putnam, eds., pp. 258-273, Prentice-Hall, Englewood
Cliffs, 1964; Reprinted in Kurt Gödel, Collected Works, Vol. II. Publications
1938-1974, S. Feferman, et al., eds., pp. 176-187 (original), pp. 254-270
(revised), Oxford University Press, New York, 1990.
[Go51] Gödel, Kurt.
1951. Some basic theorems on the foundations of mathematics and their
implications. Gibbs lecture. In Kurt Gödel, Collected Works III, pp.
304-323. 1995. Unpublished Essays and Lectures. S. Feferman et al (ed.).
[Ha47] Hardy, G.H.
1947, 9th ed. Pure Mathematics.
[HA00] Hodges, A.
2000. Uncomputability in the work of Alan Turing and Roger Penrose. Talk
given for Interface 5,
<Web page: http://www.turing.org.uk/philosophy/lecture1.html>
[La51] Landau,
E.G.H. 1951. Foundations of Analysis. Chelsea Publishing Co.,
[Me64] Mendelson,
Elliott. 1964. Introduction to Mathematical Logic. Van Norstrand,
[Pe90] Penrose,
R. (1990, Vintage edition). The Emperor's New Mind: Concerning Computers, Minds
and the Laws of Physics.
[Pe94] Penrose,
R. (1994). Shadows of the Mind: A Search for the Missing Science of
Consciousness.
[Po01] Podnieks,
Karlis. 2001. What is Mathematics: Goedel's Theorem and Around.
<e-textbook: http://www.ltn.lv/~podnieks/gt.html>
[Ru53] Rudin,
Walter. 1953. Principles of Mathematical Analysis.
[Ti61] Titchmarsh, E. C. 1961. The Theory of Functions.
[Tu36] Turing, Alan. 1936. On computable numbers, with an application
to the Entscheidungsproblem.
<Web page: http://www.abelard.org/turpap2/tp2-ie.asp
- index>
(Created:
