A foundational argument for defining Effective Computability formally, and weakening the Church and Turing Theses – II
(Notations, non-standard concepts, and definitions used commonly in these investigations are detailed in this post.)
The Logical Issue
In the previous posts we addressed first the computational issue, and second the philosophical issue—concerning the informal concept of `effective computability’—that seemed implicit in Selmer Bringsjord’s narrational case against Church’s Thesis .
We now address the logical issue that leads to a formal definability of this concept which—arguably—captures our intuitive notion of the concept more fully.
We note that in this paper on undecidable arithmetical propositions we have shown how it follows from Theorem VII of Gödel’s seminal 1931 paper that every recursive function is representable in the first-order Peano Arithmetic PA by a formula which is algorithmically verifiable, but not algorithmically computable, if we assume (Aristotle’s particularisation) that the negation of a universally quantified formula of the first-order predicate calculus is always indicative of the existence of a counter-example under the standard interpretation of PA.
(i) The concept of algorithmic verifiability is well-defined under the standard interpretation of PA over the structure of the natural numbers; and
(ii) The concept of algorithmic computability too is well-defined under the algorithmic interpretation of PA over the structure of the natural numbers; and
We shall argue in this post that the standard postulation of the Church-Turing Thesis—which postulates that the intuitive concept of `effective computability’ is completely captured by the formal notion of `algorithmic computability’—does not hold if we formally define a number-theoretic formula as effectively computable if, and only if, it is algorithmically verifiable; and it therefore needs to be replaced by a weaker postulation of the Thesis as an instantiational equivalence.
Weakening the Church and Turing Theses
We begin by noting that the following theses are classically equivalent :
In this paper we shall argue that, from a foundational perspective, the principle of Occam’s razor suggests the Theses should be postulated minimally as the following equivalences:
Weak Church’s Thesis: A number-theoretic function (or relation, treated as a Boolean function) is effectively computable if, and only if, it is instantiationally equivalent to a recursive function (or relation, treated as a Boolean function).
Weak Turing’s Thesis: A number-theoretic function (or relation, treated as a Boolean function) is effectively computable if, and only if, it is instantiationally equivalent to a Turing-computable function (or relation, treated as a Boolean function).
The need for explicitly distinguishing between `instantiational’ and `uniform’ methods
Why Church’s Thesis?
It is significant that both Kurt Gödel (initially) and Alonzo Church (subsequently—possibly under the influence of Gödel’s disquietitude) enunciated Church’s formulation of `effective computability’ as a Thesis because Gödel was instinctively uncomfortable with accepting it as a definition that minimally captures the essence of `intuitive effective computability’ .
Kurt Gödel’s reservations
Gödel’s reservations seem vindicated if we accept that a number-theoretic function can be effectively computable instantiationally (in the sense of being algorithmically verifiable as defined in the Birmingham paper, reproduced in this post), but not by a uniform method (in the sense of being algorithmically computable as defined in the Birmingham paper, reproduced in this post).
The significance of the fact (considered in the Birmingham paper, reproduced in this post) that `truth’ too can be effectively decidable both instantiationally and by a uniform method under the standard interpretation of PA is reflected in Gödel’s famous 1951 Gibbs lecture, where he remarks:
“I wish to point out that one may conjecture the truth of a universal proposition (for example, that I shall be able to verify a certain property for any integer given to me) and at the same time conjecture that no general proof for this fact exists. It is easy to imagine situations in which both these conjectures would be very well founded. For the first half of it, this would, for example, be the case if the proposition in question were some equation of two number-theoretical functions which could be verified up to very great numbers .” 
Alan Turing’s perspective
Such a possibility is also implicit in Turing’s remarks :
“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 that P is not computable. 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.”
Boolos, Burgess and Jeffrey’s query
The need for placing such a distinction on a formal basis has also been expressed explicitly on occasion .
Thus, Boolos, Burgess and Jeffrey  define a diagonal halting function, , any value of which can be decided effectively, although there is no single algorithm that can effectively compute .
Now, the straightforward way of expressing this phenomenon should be to say that there are well-defined number-theoretic functions that are effectively computable instantiationally but not uniformly. Yet, following Church and Turing, such functions are labeled as uncomputable !
However, as Boolos, Burgess and Jeffrey note quizically:
“According to Turing’s Thesis, since is not Turing-computable, cannot be effectively computable. Why not? After all, although no Turing machine computes the function , we were able to compute at least its first few values, For since, as we have noted, the empty function we have . And it may seem that we can actually compute for any positive integer —if we don’t run out of time.” 
Why should Chaitin’s constant be labelled `uncomputable’?
The reluctance to treat a function such as —or the function that computes the digit in the decimal expression of a Chaitin constant —as computable, on the grounds that the `time’ needed to compute it increases monotonically with , is curious ; the same applies to any total Turing-computable function !
Moreover, such a reluctance to treat instantiationally computable functions such as as not `effectively computable’ is difficult to reconcile with a conventional wisdom that holds the standard interpretation of the first order Peano Arithmetic PA as defining an intuitively sound model of PA.
Reason: We have shown in the Birmingham paper (reproduced in this post) that ‘satisfaction’ and ‘truth’ under the standard interpretation of PA is definable constructively in terms of algorithmic verifiability (instantiational computability).
Distinguishing between algorithmic verifiability and algorithmic computability
We now show in Theorem 1 that if Aristotle’s particularisation is presumed valid over the structure of the natural numbers—as is the case under the standard interpretation of the first-order Peano Arithmetic PA—then it follows from the instantiational nature of the (constructively defined ) Gödel -function that a primitive recursive relation can be instantiationally equivalent to an arithmetical relation, where the former is algorithmically computable over , whilst the latter is algorithmically verifiable (i.e., instantiationally computable) but not algorithmically computable over .
Significance of Gödel’s -function
We note first that in Theorem VII of his seminal 1931 paper on formally undecidable arithmetical propositions Gödel showed that, given a total number-theoretic function and any natural number , we can construct a primitive recursive function and natural numbers such that for all .
In this paper we shall essentially answer the following question affirmatively:
Query 3: Does Gödel’s Theorem VII admit construction of an arithmetical function such that:
(a) for any given natural number , there is an algorithm that can verify for all (hence may be said to be algorithmically verifiable if is recursive);
(b) there is no algorithm that can verify for all (so may be said to be algorithmically uncomputable)?
Defining effective computability
(i) Algorithmically verifiable;
(ii) Algorithmically computable.
under an interpretation.
We shall thus propose the definition:
Effective computability: A number-theoretic formula is effectively computable if, and only if, it is algorithmically verifiable.
Intuitionistically unobjectionable: We note first that since every finite set of integers is recursive, every well-defined number-theoretical formula is algorithmically verifiable, and so the above definition is intuitionistically unobjectionable; and second that the existence of an arithmetic formula that is algorithmically verifiable but not algorithmically computable (Theorem 1) supports Gödel’s reservations on Alonzo Church’s original intention to label his Thesis as a definition .
The concept is well-defined, since we have shown in the Birmingham paper (reproduced in this post) that the algorithmically verifiable and the algorithmically computable PA formulas are well-defined under the standard interpretation of PA and that:
(a) The PA-formulas are decidable as satisfied / unsatisfied or true / false under the standard interpretation of PA if, and only if, they are algorithmically verifiable;
(b) The algorithmically computable PA-formulas are a proper subset of the algorithmically verifiable PA-formulas;
(c) The PA-axioms are algorithmically computable as satisfied / true under the standard interpretation of PA;
(d) Generalisation and Modus Ponens preserve algorithmically computable truth under the standard interpretation of PA;
(e) The provable PA-formulas are precisely the ones that are algorithmically computable as satisfied / true under the standard interpretation of PA.
Gödel’s Theorem VII and algorithmically verifiable, but not algorithmically computable, arithmetical propositions
In his seminal 1931 paper on formally undecidable arithmetical propositions, Gödel defined a curious primitive recursive function—Gödel’s -function—as :
where denotes the remainder obtained on dividing by .
Gödel showed that the above function has the remarkable property that:
Lemma 1: For any given denumerable sequence of natural numbers, say , and any given natural number , we can construct natural numbers such that:
(iii) for .
Proof: This is a standard result .
Now we have the standard definition :
Definition 2: A number-theoretic function is said to be representable in PA if, and only if, there is a PA formula with the free variables , such that, for any given natural numbers :
(i) if then PA proves: ;
(ii) PA proves: .
The function is said to be strongly representable in PA if we further have that:
(iii) PA proves:
Interpretation of `‘: The symbol `‘ denotes `uniqueness’ under an interpretation which assumes that Aristotle’s particularisation holds in the domain of the interpretation.
Formally, however, the PA formula:
is merely a short-hand notation for the PA formula:
We then have:
Lemma 2 is strongly represented in PA by , which is defined as follows:
Proof: This is a standard result .
Gödel further showed (also under the tacit, but critical, presumption of Aristotle’s particularisation  that:
Lemma 3: If is a recursive function defined by:
where and are recursive functions of lower rank  that are represented in PA by well-formed formulas and ,
then is represented in PA by the following well-formed formula, denoted by :
Proof: This is a standard result .
What does “ is provable” assert under the standard interpretation of PA?
Now, if the PA formula represents in PA the recursive function denoted by then by definition, for any given numerals , the formula is provable in PA; and true under the standard interpretation of PA.
We thus have that:
Lemma 4: “ is true under the standard interpretation of PA” is the assertion that:
Given any natural numbers , we can construct natural numbers —all functions of —such that:
(b) for all , ;
where , and are any recursive functions that are formally represented in PA by and respectively such that:
(ii) for all
(iii) and are recursive functions that are assumed to be of lower rank than .
Proof: For any given natural numbers and , if interprets as a well-defined arithmetical relation under the standard interpretation of PA, then we can define a deterministic Turing machine that can `construct’ the sequences:
and give evidence to verify the assertion. 
We now see that:
Theorem 1: Under the standard interpretation of PA is algorithmically verifiable, but not algorithmically computable, as always true over .
Proof: It follows from Lemma 4 that:
(1) is PA-provable for any given numerals . Hence is true under the standard interpretation of PA. It then follows from the definition of in Lemma 3 that, for any given natural numbers , we can construct some pair of natural numbers —where are functions of the given natural numbers and —such that:
(a) for ;
(b) holds in .
Since is primitive recursive, defines a deterministic Turing machine that can `construct’ the denumerable sequence for any given natural numbers and such that:
(c) for .
We can thus define a deterministic Turing machine that will give evidence that the PA formula is true under the standard interpretation of PA.
Hence is algorithmically verifiable over under the standard interpretation of PA.
(2) Now, the pair of natural numbers are defined such that:
(a) for ;
(b) holds in ;
where is defined in Lemma 3 as !, and:
(d) is the `number’ of terms in the sequence .
Since is not definable for a denumerable sequence we cannot define a denumerable sequence such that:
(e) for all .
We cannot thus define a deterministic Turing machine that will give evidence that the PA formula interprets as true under the standard interpretation of PA for any given sequence of numerals .
Hence is not algorithmically computable over under the standard interpretation of PA.
The theorem follows.
Corollary 1: If the standard interpretation of PA is sound, then the classical Church and Turing theses are false.
The above theorem now suggests the following definition:
Definition 2: (Effective computability) A number-theoretic function is effectively computable if, and only if, it is algorithmically verifiable.
Such a definition of effective computability now allows the classical Church and Turing theses to be expressed as the weak equivalences in —rather than as identities—without any apparent loss of generality.
BBJ03 George S. Boolos, John P. Burgess, Richard C. Jeffrey. 2003. Computability and Logic (4th ed). Cambridge University Press, Cambridge.
Bri93 Selmer Bringsjord. 1993. The Narrational Case Against Church’s Thesis. Easter APA meetings, Atlanta.
Ch36 Alonzo Church. 1936. An unsolvable problem of elementary number theory. In M. Davis (ed.). 1965. The Undecidable Raven Press, New York. Reprinted from the Am. J. Math., Vol. 58, pp.345-363.
Ct75 Gregory J. Chaitin. 1975. A Theory of Program Size Formally Identical to Information Theory. J. Assoc. Comput. Mach. 22 (1975), pp. 329-340.
Go31 Kurt Gödel. 1931. On formally undecidable propositions of Principia Mathematica and related systems I. Translated by Elliott Mendelson. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York.
Go51 Kurt Gödel. 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. Solomon Feferman et al (ed.). Oxford University Press, New York.
Ka59 Laszlo Kalmár. 1959. An Argument Against the Plausibility of Church’s Thesis. In Heyting, A. (ed.) Constructivity in Mathematics. North-Holland, Amsterdam.
Kl36 Stephen Cole Kleene. 1936. General Recursive Functions of Natural Numbers. Math. Annalen vol. 112 (1936) pp.727-766.
Me64 Elliott Mendelson. 1964. Introduction to Mathematical Logic. Van Norstrand, Princeton.
Me90 Elliott Mendelson. 1990. Second Thoughts About Church’s Thesis and Mathematical Proofs. Journal of Philosophy 87.5.
Pa71 Rohit Parikh. 1971. Existence and Feasibility in Arithmetic. The Journal of Symbolic Logic, Vol.36, No. 3 (Sep., 1971), pp. 494-508.
Si97 Wilfried Sieg. 1997. Step by recursive step: Church’s analysis of effective calculability Bulletin of Symbolic Logic, Volume 3, Number 2.
Sm07 Peter Smith. 2007. Church’s Thesis after 70 Years. A commentary and critical review of Church’s Thesis After 70 Years. In Meinong Studies Vol 1 (Ontos Mathematical Logic 1), 2006 (2013), Eds. Adam Olszewski, Jan Wolenski, Robert Janusz. Ontos Verlag (Walter de Gruyter), Frankfurt, Germany.
Tu36 Alan Turing. 1936. On computable numbers, with an application to the Entscheidungsproblem In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York. Reprinted from the Proceedings of the London Mathematical Society, ser. 2. vol. 42 (1936-7), pp.230-265; corrections, Ibid, vol 43 (1937) pp. 544-546.
An07 Bhupinder Singh Anand. 2007. Why we shouldn’t fault Lucas and Penrose for continuing to believe in the Gödelian argument against computationalism – II. In The Reasoner, Vol(1)7 p2-3.
An12 … 2012. Evidence-Based Interpretations of PA. In Proceedings of the Symposium on Computational Philosophy at the AISB/IACAP World Congress 2012-Alan Turing 2012, 2-6 July 2012, University of Birmingham, Birmingham, UK.
Return to 1: cf. Me64, p.237.
Return to 2: Church’s (original) Thesis: The effectively computable number-theoretic functions are the algorithmically computable number-theoretic functions Ch36.
Return to 11: cf. Me64, p.227.
Return to 4: After describing what he meant by “computable” numbers in the opening sentence of his 1936 paper on Computable Numbers Tu36, Turing immediately expressed this thesis—albeit informally—as: “… the computable numbers include all numbers which could naturally be regarded as computable”.
Return to 5: cf. BBJ03, p.33.
Return to 6: See Si97.
Return to 7: Go51.
Return to 8: Parikh’s paper Pa71 can also be viewed as an attempt to investigate the consequences of expressing the essence of Gödel’s remarks formally.
Return to 9: Tu36, , p.139.
Return to 10: Parikh’s distinction between `decidability’ and `feasibility’ in Pa71 also appears to echo the need for such a distinction.
Return to 11: BBJ03, p. 37.
Return to 12: The issue here seems to be that, when using language to express the abstract objects of our individual, and common, mental `concept spaces’, we use the word `exists’ loosely in three senses, without making explicit distinctions between them (see An07).
Return to 13: BBJ03, p.37.
Return to 14: Chaitin’s Halting Probability is given by , where the summation is over all self-delimiting programs that halt, and is the size in bits of the halting program ; see Ct75.
Return to 15: The incongruity of this is addressed by Parikh in Pa71.
Return to 16: The only difference being that, in the latter case, we know there is a common `program’ of constant length that will compute for any given natural number ; in the former, we know we may need distinctly different programs for computing for different values of , where the length of the program will, sometime, reference .
Return to 17: By Kurt Gödel; see Go31, Theorem VII.
Return to 18: Analagous distinctions in analysis: The distinction between algorithmically computable, and algorithmically verifiable but not algorithmically computable, number-theoretic functions seeks to reflect in arithmetic the essence of uniform methods (formally detailed in the Birmingham paper (reproduced in this post) and in its main consequence—the Provability Theorem for PA—as detailed in this post), classically characterised by the distinctions in analysis between: (a) uniformly continuous, and point-wise continuous but not uniformly continuous, functions over an interval; (b) uniformly convergent, and point-wise convergent but not uniformly convergent, series.
A limitation of set theory and a possible barrier to computation: We note, further, that the above distinction cannot be reflected within a language—such as the set theory ZF—which identifies `equality’ with `equivalence’. Since functions are defined extensionally as mappings, such a language cannot recognise that a set which represents a primitive recursive function may be equivalent to, but computationally different from, a set that represents an arithmetical function; where the former function is algorithmically computable over , whilst the latter is algorithmically verifiable but not algorithmically computable over .
Return to 20: cf. Go31, p.31, Lemma 1; Me64, p.131, Proposition 3.21.
Return to 21: cf. Go31, p.31, Lemma 1; Me64, p.131, Proposition 3.22.
Return to 22: Me64, p.118.
Return to 23: cf. Me64, p.131, proposition 3.21.
Return to 24: The implicit assumption being that the negation of a universally quantified formula of the first-order predicate calculus is indicative of “the existence of a counter-example”—Go31, p.32.
Return to 25: cf. Me64, p.132; Go31, p.30(2).
Return to 26: cf. Go31, p.31(2); Me64}, p.132.
Return to 27: A critical philosophical issue that we do not address here is whether the PA formula can be considered to interpret under a sound interpretation of PA as a well-defined predicate, since the denumerable sequences and is not equal to if is not equal to —are represented by denumerable, distinctly different, functions respectively. There are thus denumerable pairs for which yields the sequence .