◄ Index                                                                        

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]

I.     The significance of defining mathematical objects constructively and mathematical truth effectively

Preamble

A formal definition of mathematical objects

An alternative interpretation of Gödel’s Proof

The ambiguity in Tarski’s definitions of satisfiability and truth

Overview

2.  Notation

3.  Definitions

4.  A meta-theorem of recursive asymmetry

5.  Two meta-lemmas

II.   Some consequences of defining mathematical objects constructively

1.  Analysing Gödel’s Theorem XI

Implicit meta-theses underlying Gödel’s Theorem XI

A negative meta-theorem

Gödel’s Proof of Theorem XI

Gödel’s Theorem XI as a conditional meta-assertion

Analytic summary

2.  Consistency and Meta-thesis 3

3.  Can “consistency” be a formal convention?

4.  Definitions of new function and predicate letters

The classical argument

Non-constructive definitions

Instantiationally and algorithmically computable functions

Gödel’s Theorem V

Gödel’s Theorem VII

Standard PA

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

Classical Turing machines

Neo-classical Turing machines

Total partial recursive functions

The Arithmetical Provability Thesis and the classical Church-Turing Theses

Converging NT-routines and Cauchy sequences

The P versus NP problem

4.  Turing’s computable and uncomputable numbers

5.  Cantor’s diagonal argument

6.  Constructivity and classical Quantum Mechanics

I.  The significance of defining mathematical objects constructively and mathematical truth effectively

1.  Introduction

1.1  Preamble

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 Roger Penrose in [Pe90] and [Pe94].

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, aleph₁, 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.

1.5  Overview

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(x₁, ..., x_n), there is an n-ary PREDICATE[37] r (with the FREE VARIABLES u₁ ... u_n) such that, for all n-tuples of numbers (x_1, ..., x_n), we have:

R(x₁, ..., x_n) => Bew[Sb(r (u₁ ... u_n)|(Z(x₁) ... Z(x_n)))]                         (3)

~R(x₁, ..., x_n) => Bew[Neg Sb(r (u₁ ... u_n)|(Z(x₁) ... Z(x_n)))]               (4)”

In a footnote, he adds that ([Go31a], footnote 38):

“The VARIABLES u₁ ... u_n 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(x₁, ..., x_n) is “... definable within the system P (under its intuitive interpretation) ...” - means that his reasoning is based on an implicit assumption that R(x₁, ..., x_n) 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(x₁, ..., x_n) 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.

2.  Notation

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 “B_P”, 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, [~xB_P(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, [~xB_P(Sb(p 19|Z(p)))], hence [(Ax)~xB_P(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(x₁,  ..., x_n) be any recursive number-theoretic relation, and F(x₁,  ..., x_n) 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 <a₁,  ..., a_n> of natural numbers:

f(a₁,  ..., a_n) holds if, and only if, F(a₁,  ..., a_n) holds.

However, by Meta-lemma 1, it follows that [f(x₁,  ..., x_n)] is not necessarily a P-formula. Hence, we cannot conclude that:

[f(x₁,  ..., x_n) <=> F(x₁,  ..., x_n)] 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)].

1.2  A negative meta-theorem

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.

1.5  Analytical summary

(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: (x₁)( x₂)( x₃)( x₄)~(Pf(x₁, x₃) & Pf(x₂, x₄) & Ng(x₃, x₄)). 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?

4.1  The classical argument

The classical argument is expressed by Mendelson ([Me64], p82, §9):

“In mathematics, once we have proved, for any y₁, ..., y_n, the existence of a unique object u having the property A(u, y₁, ..., y_n), we often introduce a new function f(y₁, ..., y_n) such that A(f(y₁, ..., y_n), y₁, ..., y_n) holds for all y₁, ..., y_n. ... 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, y₁, ..., y_n)][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(y₁, ..., y_n), y₁, ..., y_n)], 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, x₁, ..., x_n)] 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 <a₁, ..., a_n> in the domain of M, R(b, a₁, ..., a_n) holds in M, where R(y, x₁, ..., x_n) is the interpretation of [R(y, x₁, ..., x_n)] in M.

We may thus define a total function F(x₁, ..., x_n) in M such that, given any sequence <b, a₁, ..., a_n> in M:

R(b, a₁, ..., a_n) <=> (F(a₁, ..., a_n) = b)

holds in M.

Thus, (i) assures us, classically, that:

(ii)     For each given sequence <a₁, ..., a_n> in the domain of M, there is some effective method, which may depend on <a₁, ..., a_n>, that will compute a unique b as the value of F(a₁, ..., a_n) in M in a finite, possibly indeterminate, number of steps t(a₁, ..., a_n).

However, the P-provability of [(E!x)R(x, y₁, ..., y_n)], by itself, does not assure us that there is an algorithm such that, given any sequence <a₁, ..., a_n> in the domain of M, it will compute a unique b, in the domain of M, as the value of F(a₁, ..., a_n) in a determinate number of steps t(a₁, ..., a_n).

In other words, some sequence <a₁, ..., a_n> may require an input-sequence-specific effective method in order to compute F(a₁, ..., a_n).

Hence, in the absence of an algorithm, F(x₁, ..., x_n) may be defined as instantiationally, but not algorithmically, computable in M.

(There is also no assurance of an algorithm that, for any given sequence <a₁, ..., a_n>, will compute t(a₁, ..., a_n) in M.)

4.4  Gödel’s Theorem V

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.

4.5  Gödel’s Theorem VII

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(x₁, ..., x_n)] is an atomic formula[98] of P, and R(x₁, ..., x_n) is the corresponding relation of the interpretation, then the sequence[99] <a₁, ..., a_n> of M satisfies [R(x₁, ..., x_n)] classically, under the interpretation M, if, and only if, there is an effective method to determine that R(a₁, ..., a_n) holds[100] in M, where a₁, ..., a_n 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 [(Ax_i)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 [(Ax_i)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 [(Ax_i)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 Peano Arithmetic, PA, and an effective method that determines whether or not a given sequence, s, of M, satisfies the relation R in M, the relation R is expressible in PA?

(**) When may we constructively assume that, given a relation R in an interpretation M of a Peano Arithmetic, PA, and an effective method that determines whether or not a given sequence, s, of M, satisfies the relation R in M, the relation R is provable in PA?

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(x₁, ..., x_n) in some interpretation M of a Peano Arithmetic, PA, and any sequence <a₁, ..., a_n> in M, there is an effective method such that it will determine whether R(a₁, ..., a_n) 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'(x₁, ..., x_n)] such that:

R(a₁, ..., a_n) holds in M if, and only if, [R'(a₁, ..., a_n)] 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 Peano Arithmetic, PA, there is an effective method such that, for a given, total, arithmetical relation R(x), and any element k in M, it will always determine that R(k) holds in M, then:

[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 Peano Arithmetic, PA, then the predicate letter “R” is a formal mathematical object of PA.

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(x₁, ..., x_n) of M is effectively expressible in PA if, and only if, there is a PA-formula [R'(x₁, ..., x_n)], with n free variables, such that, for any sequence of numerals <[b], [a₁], ..., [a_n]> of PA, there is an effective method, which may depend on <b, a₁, ..., a_n>, for determining that:

(i)    if R(a₁, ..., a_n) holds in M, then [R'(a₁, ..., a_n)] is PA-provable;

(ii)   if R(a₁, ..., a_n) does not hold in M, then [~R'(a₁, ..., a_n)] is PA-provable,

where <b, a₁, ..., a_n> is the interpretation of <[b], [a₁], ..., [a_n]> in M.

We note that, for any given sequence of numerals <[b], [a₁], ..., [a_n]> 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(x₁, ..., x_n) of M is effectively representable in PA if, and only if, there is a PA-formula [R(y, x₁, ..., x_n)], with the free variables [(y, x₁, ..., x_n)], such that, for any sequence of numerals <[b], [a₁], ..., [a_n]> of PA:

(i)    there is an effective method, which may depend on <b, a₁, ..., a_n>, for determining that if (F(a₁, ..., a_n) = b) holds in M, then [R(b, a₁, ..., a_n)] is PA-provable;

(ii)   [(E!y)R(y, a₁, ..., a_n)] is PA-provable,

where <b, a₁, ..., a_n> is the interpretation of <[b], [a₁], ..., [a_n]> in M.

We again note that, for any given sequence of numerals <[b], [a₁], ..., [a_n]> 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(x₁, ..., x_n) of M is strongly representable effectively in a formal system P if, and only if, there is a P-formula [R(y, x₁, ..., x_n)], with the free variables [(y, x₁, ..., x_n)], such that:

(i)    for any sequence of numerals <[b], [a₁], ..., [a_n]> of P, there is an effective method, which may depend on <b, a₁, ..., a_n>, for determining that if (F(a₁, ..., a_n) = b) holds in M, then [R(b, a₁, ..., a_n)] is P-provable;

(ii)   [(E!y)R(y, x₁, ..., x_n)] is P-provable,

where <b, a₁, ..., a_n> is the interpretation of <[b], [a₁], ..., [a_n]> in M.

We note that, here also, for any given sequence of numerals <[b], [a₁], ..., [a_n]> 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(x₁, ..., x_n) in M is effectively definable in a formal system P if, and only if, [R(x₁, ..., x_n)] is a P-formula such that, for any sequence of numerals <[a₁], ..., [a_n]> of P, there is an effective method, which may depend on <a₁, ..., a_n>, for determining that:

(i)    if R(a₁, ..., a_n) holds in M, then [R(a₁, ..., a_n)] is P-provable;

(ii)   if R(a₁, ..., a_n) does not hold in M, then [~R(a₁, ..., a_n)] is P-provable,

where <a₁, ..., a_n> is the interpretation of <[a₁], ..., [a_n]> 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], [a₁], ..., [a_n]> 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(x₁, ..., x_n) is effectively computable instantiationally in an interpretation M of a Peano Arithmetic, PA, if, and only if, it is effectively representable in PA.

Definition 2(vi): A number-theoretic function F(x₁, ..., x_n) is effectively computable algorithmically in an interpretation M of a Peano Arithmetic, PA, if, and only if, it is both effectively representable and effectively definable in PA.

Meta-lemma 11: If a number-theoretic function F(x₁, ..., x_n) 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. 

We can now define:

Definition 2(vii): A number-theoretic function F(x₁, ..., x_n) in the standard interpretation M of a Peano Arithmetic, PA, is effectively computable if, and only if, it is effectively computable instantiationally.

Definition 2(viii): A number-theoretic function F(x₁, ..., x_n) is an omega-function in an interpretation M of a Peano Arithmetic PA if, and only if, there is a PA-formula [R(y, x₁, ..., x_n)], with the free variables [(y, x₁, ..., x_n)], such that:

(i)    for any sequence of numerals <[b], [a₁], ..., [a_n]> of PA, there is an effective method, which may depend on <b, a₁, ..., a_n>, for determining that, if (F(a₁, ..., a_n) = b) holds in M, then [R(b, a₁, ..., a_n)] is PA-provable, where <b, a₁, ..., a_n> is the interpretation of <[b], [a₁], ..., [a_n]> in M;

(ii)   for any sequence of numerals <[b], [a₁], ..., [a_n]> of PA, there is an effective method, which may depend on <b, a₁, ..., a_n>, for determining that [(E!y)(R(b, a₁, ..., a_n))] is PA-provable;

(iii)  [(E!y)(R(y, x₁, ..., x_n))] is not PA-provable,

where <b, a₁, ..., a_n> is the interpretation of <[b], [a₁], ..., [a_n]> in M.

We thus have:

Meta-lemma 12: An omega-function F(x₁, ..., x_n) in an interpretation M of a Peano Arithmetic, PA, is effectively computable instantiationally, but not effectively computable algorithmically.

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(x₁, ..., x_n) is classically Turing-computable[107] in the standard interpretation M of a Peano Arithmetic, PA, then it is effectively computable instantiationally in M.[108]

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(x₁, ..., x_n) 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(x₁, ..., x_n) 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:

3.1  Classical Turing machines

(a)   There is a two-way, potentially infinite[110], tape divided up into squares. There is a finite set of tape symbols S₀, S₁, ..., S_n 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 {q₀, q₁, ..., q_m}. 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] S_i, and the machine is in the internal state q_j, then the action of the machine is determined, and it will do one of four things:

(i)    it may erase the symbol S_i and print a new symbol S_k;

(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 q_r, and is ready to act again at time t+1.

(b)   The actions (a)(i) to (a)(iii) can be represented by quadruples:

(i)    q_jS_iS_kq_r;

(ii)   q_jS_iLq_r;

(iii)  q_jS_iRq_r,

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 q₀. 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 S_m;

(ii)   the only symbol which is not a tape symbol is an internal state q_s;

(iii)  q_s 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 Pq_jS_iQ, beta is of the form Pq_rS_kQ, and q_jS_iS_kq_r is one of the quadruples of T;

(ii)   or, alpha is of the form PS_sq_jS_iQ, beta is Pq_rS_sS_iQ, and q_jS_iLq_r is one of the quadruples of T;

(iii)  or, alpha is of the form q_jS_iQ, beta is q_rS₀S_iQ, and q_jS_iLq_r is one of the quadruples of T;

(iv)  or, alpha is of the form Pq_jS_iS_kQ, beta is PS_iq_rS_kQ, and q_jS_iRq_r is one of the quadruples of T;

(v)   or, alpha is of the form Pq_jS_i, beta is PS_iq_rS_o, and q_jS_iRq_r 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 alpha₀, alpha₁, ..., alpha_m (m >= 0) such that:

(i)    the internal state occuring in alpha₀ is q₀;

(ii)   for 0 =< i < m, alpha_(i+1) follows alpha_i;

(iii)  there is no instantaneous tape description alpha_(m+1) into which T can move alpha_m;

(iv) and T stops at alpha_m.

(k)   The algorithm B_T,C in any alphabet C containing the alphabet A of T is defined as follows:

For any words P, Q in C, B_T,C(P) = Q if, and only if, there is a classical computation of T which begins with the  instantaneous tape description q₀P and ends with an instantaneous tape description of the form R₁q_jR₂, where Q = R₁R₂.

(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 B_T,C and U are fully equivalent relative to D.

(m)  Given a partial number-theoretic function F(x₁, ..., x_n), we say that a Turing machine T (whose alphabet A includes {1, *}) computes F if, and only if, for any natural numbers k₁, k₂, ... k_n, and any word Q, B_T,A(k₁* k₂* ... * k_n) = Q if, and only if, Q is R₁F(x₁, ..., x_n)R₂, where both R₁ and R₂ are certain, possibly empty, words consisting only of S₀’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 alpha₀, alpha₁, ..., alpha_m (m >= 0) such that:

(i)    the internal state occuring in alpha₀ is q₀;

(ii)   for 0 =< i < m, alpha_(i+1) follows alpha_i;

(iii)  alpha_m is a repetition of alpha_i for some 0 =< i < m;

(iv)  NT stops at alpha_m.[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 alpha_i 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 n₀ such that, given any natural number n > n₀, there is a minimum configuration number n_min such that, for any given configuration number m > n_min, the instantaneous tape description is of the form Pq_jS_iQ 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(x₁, ..., x_n) 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(x₁, ..., x_n) = μy(G(x₁, ..., x_n, y) = 0).

If [H(x₁, ..., x_n, y)] expresses ~(G(x₁, ..., x_n, y) = 0) in a Peano Arithmetic, PA, we consider the PA-provability, and truth in the standard interpretation M of PA, of the formula [H(a₁, ..., a_n, y)] for a given sequence of numerals <[a₁], ..., [a_n]> of PA.

(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 Q₁ be the meta-assertion that [H(a₁, ..., a_n, 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(a₁, ..., a_n, y)] classically.

Since G(a₁, ..., a_n, y) is recursive, it follows that there is some finite k such that any neo-classical Turing machine NT₁(y) that computes G(a₁, ..., a_n, y) will halt and return the value 0 for y = k.

(b)   Next, let Q₂ be the meta-assertion that [H(a₁, ..., a_n, 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(a₁, ..., a_n, y)] classically.

Since G(a₁, ..., a_n, y) is recursive, it follows that there is some finite k such that any neo-classical Turing machine NT₂(y) that computes the arithmetical function H(a₁, ..., a_n, y) will halt, and return the symbol for self-termination, for y = k.