**Preamble**

I find a frustrating equivocity^{[*]} in standard literature between the intent behind the definitions of the classes and as explained informally in terms of ‘verifiability’ and ‘decidability’, and the formal definitions of these two classes.

I call it the Separation Problem.

My understanding of the intent commonly expressed in standard literature is that:

**Verifiability:** A number-theoretical formula is verifiable under an interpretation (and should by intent be defined in ) if, and only if, for any given natural number , there is a deterministic algorithm which can provide objective evidence for deciding the value of each formula in the finite sequence .

**Decidability:** A number theoretical formula is decidable under an interpretation (and should by intent be defined in ) if, and only if, there is a deterministic algorithm that can provide objective evidence for deciding the value of each formula in the denumerable sequence .

In other words, for me ‘decidability’ should imply the existence of a deterministic algorithm that can decide the truth/falsity of each proposition in a well-defined denumerable sequence of propositions; whereas ‘verifiability’ need not imply the existence of a deterministic algorithm that can decide the truth/falsity of each proposition in a well-defined denumerable sequence of propositions.

For reasons and in ways that I cannot quite grasp as yet, it seems to me that standard definitions of the two classes and only muddy the issue by associating the two concepts with terms such as ‘quickly’, ‘polynomial-time’ and ‘non-deterministic’; and by requiring introduction of some corresponding measure/s of computational complexity.

In other words, standard definitions of the two classes assert that:

**Verifiability (standard):** A number-theoretical formula is verifiable under an interpretation (and is defined in ) if, and only if, for any given natural number , there is a deterministic polynomial-time algorithm which can provide objective evidence for deciding the value of each formula in the finite sequence .

**Decidability (standard):** A number theoretical formula is decidable under an interpretation (and is defined in ) if, and only if, there is a deterministic polynomial-time algorithm that can provide objective evidence for deciding the value of each formula in the denumerable sequence

The following argument attempts to view the consequence for the problem if we separate the two classes and essentially as intended in the first case above.

The justification for this perspective is the formal distinction between the two concepts of ‘algorithmic verifiability’ and ‘algorithmic computability’ introduced in the Birmingham paper.

The significance that such a distinction may have for the first-order Peano Arithmetic in particular—and for the foundations of mathematics, logic and computability in general—has already been suggested in this post.

**Abstract**

In this investigation we now consider the consequences of separating the classes and logically from a similar—finitary arithmetical rather than computational—perspective.

This perspective too is based on explicitly highlighting that the assignment of satisfaction and truth values to number-theoretic formulas under an interpretation can be constructively defined in two distinctly different ways:

(a) in terms of algorithmic verifiability, and

(b) in terms of algorithmic computability.

From this perspective it can be seen that standard definitions of the classes and implicitly assume without proof that:

**Cook’s Thesis:** If a propositional formula is algorithmically verifiable in polynomial time, then it is algorithmically computable.

This imples that the differentiation between the two classes is only quantitative, and can therefore be adequately expressed in terms of computational complexity.

However, we argue that there are classically defined arithmetic formulas which are algorithmically verifiable but not algorithmically computable; and so the differentiation between the classes and can also be defined qualitatively, and need not be expressed only in terms of computational complexity.

Specifically, we show how Gödel’s -function uniquely corresponds some real numbers to algorithmically verifiable arithmetical formulas that are not algorithmically computable.^{[**]}

**Introduction**

“The computability precursors of the classes and are the classes of decidable and c.e. (computably enumerable) languages, respectively. We say that a language is c.e. i.e. (or semi-decidable) iff for some Turing machine . We say that is decidable iff for some Turing machine which satisfies the condition that halts on all input strings . …

Thus the problem Satisfiability is: Given a propositional formula , determine whether is satisfiable. To show that this is in we define the polynomial-time checking relation , which holds iff codes a propositional formula and codes a truth assignment to the variables of which makes true.”

… Stephen Cook, *The P versus NP Problem*, 2000, Clay Mathematical Institute, Providence, USA.

In this investigation we shall argue that standard interpretations—such as the above^{[1]}—of the formal definitions of the classes and leave room for ambiguity.

Specifically, such interpretations fail to explicitly highlight that the assignment of satisfaction and truth values to number-theoretic formulas under an interpretation can be constructively defined in two distinctly different ways^{[1a]}:

(a) in terms of algorithmic verifiability (Definition 1 below);

It immediately follows from this definition that a number-theoretical formula is algorithmically verifiable under an interpretation (and should therefore be defined in ) if, and only if, we can define a checking relation ^{[2]}—where codes a propositional formula and codes a truth assignment to the variables of —such that, for any given natural number values , there is a deterministic algorithm which will finitarily decide whether or not holds over the domain of the natural numbers.

(b) in terms of algorithmic computability (Definition 2 below).

It immediately follows from this definition that a number-theoretical formula is algorithmically computable under an interpretation (and should therefore be defined in ) if, and only if, we can define a checking relation ^{[3]}—where codes a propositional formula and codes a truth assignment to the variables of —such that there is a deterministic algorithm which, for any given natural number values , will finitarily decide whether or not holds over the domain of the natural numbers.

In other words, standard interpretations of the classes and implicitly assume without proof that:

**Cook’s Thesis:** If a propositional formula is algorithmically verifiable in polynomial-time, then it is algorithmically computable.

It would follow from such a perspective that the differentiation between the classes and is only quantitative, and can therefore be adequately expressed in terms of computational complexity.

However, we shall argue that—since the two concepts are well-defined^{[3a]}—there are classically defined arithmetic formulas which are algorithmically verifiable but not algorithmically computable; and so the differentiation between the classes and is also qualitative, and cannot be adequately expressed in terms of only computational complexity.

**The Separation Problem**

Accordingly, in this investigation we shall ignore both Cook’s Thesis and polynomial-time computations, and address instead the following non-standard (NS) formulation of the Separation Problem in arithmetic:

**Non-standard :** Is there an arithmetical formula that is algorithmically verifiable but not algorithmically computable?

We shall first show how Gödel’s -function uniquely corresponds each classically defined real number to an algorithmically verifiable arithmetical formula.

Since classical theory admits the existence of real numbers that are not algorithmically computable^{[4]}, we shall conclude that classical theory must also admit the existence of arithmetical formulas that are algorithmically verifiable but not algorithmically computable.

**Algorithmically verifiable and algorithmically computable formulas**

**Definition 1:** A number-theoretical formula is algorithmically verifiable under an interpretation if, and only if, for any given natural number , there is a deterministic algorithm which can provide objective evidence^{[5]} for deciding the value of each formula in the finite sequence .

The concept is well-defined in the sense that, first, every atomic number-theoretical formula is algorithmically verifiable as above^{[6]}; further, by Tarski’s definitions^{[7]}, the algorithmic verifiability of the formulas of a formal language which contain logical constants can be inductively defined under an interpretation in terms of the algorithmic verifiability of the interpretations of the atomic formulas of the language.

In particular^{[8]}, the formulas of the first order Peano Arithmetic PA are constructively decidable under the standard interpretation of PA over the domain of the natural numbers if, and only if, they are algorithmically verifiable under the interpretation.^{[9]}

**Definition 2:** A number theoretical formula is algorithmically computable under an interpretation if, and only if, there is a deterministic algorithm that can provide objective evidence for deciding the value of each formula in the denumerable sequence .

This concept too is well-defined in the sense that, first, every atomic number-theoretical formula is algorithmically computable as above^{[10]}; further, by Tarski’s definitions, the algorithmic computability of the formulas of a formal language which contain logical constants can also be inductively defined under an interpretation in terms of the algorithmic computability of the interpretations of the atomic formulas of the language.

In particular^{[11]}, the PA-formulas are constructively decidable under an algorithmic interpretation of PA over if, and only if, they are algorithmically computable under the interpretation.^{[12]}

We note that:

**Lemma 1:** There are algorithmically verifiable number theoretical formulas which are not algorithmically computable.

*Proof:* Let denote the digit in the decimal expression of a putatively given real number in the interval .

By the definition of the real number as the limit of the Cauchy sequence of rationals , it follows that is an algorithmically verifiable number-theoretic function.

Since the set of algorithmically computable reals is countable^{[13]}, Cantor’s diagonal argument^{[14]} shows that there are real numbers that are not algorithmically computable.

The Lemma follows.

We note that algorithmic computability implies the existence of a deterministic algorithm that can decide the truth/falsity of each proposition in a well-defined denumerable sequence of propositions, whereas algorithmic verifiability does not imply the existence of a deterministic algorithm that can decide the truth/falsity of each proposition in a well-defined denumerable sequence of propositions.^{[15]}

**Gödel’s -function**

We note next that Gödel’s -function is the primitive recursive number-theoretic function defined by^{[16]}:

**Definition 3:** , where denotes the remainder obtained on dividing by .

We also note that:

**Lemma 2:** For any non-terminating sequence of values , we can construct natural numbers such that:

(i) ;

(ii) !;

(iii) for .

*Proof:* This is a standard result^{[17]}.

Now we have the standard definition^{[18]}:

**Definition 4:** A number-theoretic function is said to be representable in the first order Peano Arithmetic PA if, and only if, there is a PA formula ^{[19]} 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:

We also have that:

**Lemma 3:** is strongly represented in PA by , which is defined as follows:

.

*Proof:* This is a standard result^{[20]}.

**An arithmetical perspective on the Separation Problem**

We finally argue that:

**Theorem 1:** There is an arithmetical formula that is algorithmically verifiable but not algorithmically computable under any sound interpretation of PA.

*Proof:* Let be the denumerable sequence defined by the denumerable sequence of digits in the decimal expansion of a putatively given real number in the interval .

By Lemma 2, for any given natural number , there are natural numbers such that, for any :

.

By Lemma 3, is strongly represented in PA by such that, for any :

If then PA proves .

We now define the arithmetical formula for any by:

if, and only if, PA proves .

Hence every putatively given real number in the interval uniquely corresponds to an algorithmically verifiable arithmetical formula since:

For any , the primitive recursivity of yields a deterministic algorithm AL that can provide objective evidence for deciding the unique value of each formula in the finite sequence by evidencing the truth under a sound interpretation of PA for:

…

.

The correspondence is unique because, if and are two different putatively given reals in the interval , then there is always some for which:

.

Hence the corresponding arithmetical formulas and are such that:

for all .

for all .

.

By Lemma 1, there is an algorithmically uncomputable real number such that the corresponding PA formula is also algorithmically uncomputable, but algorithmically verifiable, under a sound interpretation of PA.

The theorem follows.

**An arithmetical perspective on the problem**

We conclude that if we were to unambiguously define the classes and as in Section 1(a) and Section 1(b) respectively, then it would follow that:

**Corollary 1:**

**References**

**Kl52** Stephen Cole Kleene. 1952. *Introduction to Metamathematics.* North Holland Publishing Company, Amsterdam.

**Me64** Elliott Mendelson. 1964. *Introduction to Mathematical Logic.* Van Norstrand. pp.145-146.

**Mo12** Cristopher Moore. 2012. *P vs. NP, Phase Transitions, and Incomputability in the Wild.* Presentation given on 18th June 2012 at the Turing Centenary Workshop on *The Incomputable* at the Kavli Royal Society International Center at Chicheley Hall, Chichely, Buckinghamshire, UK.

**Mu91** Chetan R. Murthy. 1991. *An Evaluation Semantics for Classical Proofs.* Proceedings of Sixth IEEE Symposium on Logic in Computer Science, pp. 96-109, (also Cornell TR 91-1213), 1991.

**Ta33** Alfred Tarski. 1933. *The concept of truth in the languages of the deductive sciences.* In *Logic, Semantics, Metamathematics, papers from 1923 to 1938.* (p152-378). ed. John Corcoran. 1983. Hackett Publishing Company, Indianapolis.

**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-365; corrections, Ibid, vol 43 (1937) pp. 544-546.

**An12** Bhupinder Singh Anand. 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.

**An13** … 2013. *A suggested mathematical perspective for the argument.* Presented on 7’th April at the workshop on `*Logical Quantum Structures*‘ at UNILOG’2013, 4’th World Congress and School on Universal Logic, 29’th March 2013 – 7’th April 2013, Rio de Janeiro, Brazil.\

**Notes**

Return to *: I am not alone! See for instance this blogpost of Timothy Gower’s representing one extreme; and this plaintive appeal representing the other.

Return to **: For a broader perspective on the relation of Gödel’s -function to this distinction, see this post.

Return to 1: See also Mo12.

Return to 1a: The distinction is explicitly introduced—and its significance in establishing a finitary proof of consistency for the first order Peano Arithmetic PA highlighted—in An12.

Return to 2: If is a formula of the first order Peano Arithmetic PA, the existence of such a checking relation is assured by An12, Theorem 2.

Return to 3: If is a PA formula, the existence of such a checking relation is assured by An12, Theorem 3.

Return to 3a: See here. We further note informally here how the distinction between the two concepts may have far-reaching and significant consequences not only for the foundations of mathematics, logic and computability, but also for our perspective on the underlying structure of the laws of nature.

Return to 4: Tu36.

Return to 5: “It is by now folklore … that one can view the *values* of a simple functional language as specifying *evidence* for propositions in a constructive logic …”; Mu91.

Return to 6: Tu36.

Return to 7: On the inductive assignment of satisfaction and truth values to the formulas of a formal language under an interpretation; Ta33.

Return to 8: An12, Theorem 2, Corollary 2.

Return to 9: We note that the Axiom Schema of Finite Induction can be finitarily verified as true under the standard interpretation of PA with respect to ‘truth’ as defined by the algorithmically verifiable formulas of PA.

Return to 10: Tu36.

Return to 11: An12, Theorem 5.

Return to 12: We note that the Axiom Schema of Finite Induction can be finitarily verified as true under the standard interpretation of PA with respect to ‘truth’ as defined by the algorithmically computable formulas of PA.

Return to 13: Tu36.

Return to 14: Kl52, pp.6-8.

Return to 15: From the point of view of a finitary mathematical philosophy, the significant difference between the two concepts could be expressed (An13) by saying that we may treat the decimal representation of a real number as corresponding to a physically measurable limit—and not only to a mathematically definable limit—if and only if such representation is definable by an algorithmically computable function.

Return to 16: Me64, p.131, Proposition 3.21.

Return to 17: Me64, p.131, Proposition 3.22.

Return to 18: Me64, p.118.

Return to 19: We use square brackets simply as a convenience in informal argumentation to differentiate between a formal expression and its interpretation over some domain when there is a possibility of confusion between the two.

Return to 20: cf., Me64, p.131, proposition 3.21.

## Leave a comment

Comments feed for this article