You are currently browsing the tag archive for the ‘finitary’ tag.

Three Dogmas of FOL: Hibertian Theism, Brouwerian Atheism, and Finitary Agnosticism (work in progress as on 10/07/2017)

(Notations, non-standard concepts, and definitions used commonly in these investigations are detailed in this post.)

What essentially differentiate our approach of finitary agnosticism to mathematical reasoning in this investigation from both the classical Hilbertian, and the intuitionistic Brouwerian, perspectives is how we address two significant dogmas of the classical first order logic FOL.

Hilbertian Theism

In a 1925 address[1] Hilbert had shown that the axiomatisation $\mathcal{L}_{\varepsilon}$ of classical Aristotlean predicate logic proposed by him as a formal first-order $\varepsilon$-predicate calculus[2] in which he used a primitive choice-function[3] symbol, $\varepsilon$‘, for defining the quantifiers $\forall$‘ and $\exists$‘ would adequately express—and yield, under a suitable interpretation—Aristotle’s logic of predicates if the $\varepsilon$-function was interpreted to yield Aristotlean particularisation[4].

Classical approaches to mathematics—essentially following Hilbert—can be labelled theistic’ in that they implicitly assume—without providing adequate objective criteria—[5] both that:

$\bullet$ The standard first order logic FOL is consistent;

and that:

$\bullet$ The standard interpretation of FOL is finitarily sound (which implies Aristotle’s particularisation).

The significance of the label theistic’ is that conventional wisdom tacitly believes that Aristotle’s particularisation remains valid—without qualification—even over infinite domains; a belief that is not unequivocally self-evident, but must be appealed to as an article of faith.

Although intended to highlight an entirely different distinction, that the choice of such a label may not be totally inappropriate is suggested by Tarski’s point of view[6] to the effect:

“… that Hilbert’s alleged hope that meta-mathematics would usher in a feeling of absolute security’ was a kind of theology’ that lay far beyond the reach of any normal human science’ …”.

Brouwerian Atheism

We note second that, in sharp contrast, constructive approaches to mathematics—such as Intuitionism[6a]—can be labelled atheistic’ since they deny both that:

$\bullet$ FOL is consistent (since they deny the Law of The Excluded Middle[7];

and that:

$\bullet$ The standard interpretation of FOL is sound (since they deny Aristotle’s particularisation).

The significance of the label atheistic’ is that whereas constructive approaches to mathematics deny the faith-based belief in the unqualified validity of Aristotle’s particularisation over infinite domains, their denial of the Law of the Excluded Middle is itself a belief—in the inconsistency of FOL—that is also not unequivocally self-evident, and must also be appealed to as an article of faith since it does not take into consideration the objective criteria for the consistency of FOL that follows from the Birmingham paper.

Although Brouwer’s explicitly stated objection appeared to be to the Law of the Excluded Middle as expressed and interpreted at the time[8], some of Kleene’s remarks[9], some of Hilbert’s remarks[10] and, more particularly, Kolmogorov’s remarks[11] suggest that the intent of Brouwer’s fundamental objection (see this post) can also be viewed today as being limited only to the yet prevailing belief—as an article of faith—that the validity of Aristotle’s particularisation can be extended without qualification to infinite domains.

Finitary Agnosticism

In our investigations, however, we adopt what may be labelled a finitarily agnostic’ perspective[12] by noting that although, if Aristotle’s particularisation holds in an interpretation then the Law of the Excluded Middle must also hold in the interpretation, the converse is not true.

We thus follow a middle path by explicitly assuming on the basis of the Birmingham paper (reproduced in this post) that:

$\bullet$ FOL is finitarily consistent;

and by explicitly stating when an argument appeals to the postulation that:

$\bullet$ The standard interpretation of FOL is sound.

The significance of the label agnostic’ is that we neither hold FOL to be inconsistent, nor hold that Aristotle’s particularisation can be applied—without qualification—over infinite domains.

The two seemingly contradictory but perhaps complementary perspectives

It follows from the above that the Brouwerian Atheistic perspective is merely a restricted perspective within the Finitary Agnostic perspective, whilst the Hilbertian Theistic perspective contradicts the Finitary Agnostic perspective.

Curiously, a case can be made (as is attempted in this post, and in this paper that I presented on 10th June 2015 at the Epsilon 2015 workshop on Hilberts Epsilon and Tau in Logic, Informatics and Linguistics, University of Montpellier, France, June 10-11-12) that the Hilbertian perspective formalises the concept of algorithmically verifiable truth’ in the non-finitary—hence essentially subjective—reasoning that circumscribes human intelligences (which, by the Anthropic principle, can be taken to reflect the ‘truths’ of natural laws), whilst the Finitary perspective formalises the concept of ‘algorithmically computable truth’ in the finitary—hence essentially objective—reasoning that circumscribes mechanical intelligences; and that the two are complementary, not contradictory, perspectives on the nature and scope of quantification.

References

BBJ03 George S. Boolos, John P. Burgess, Richard C. Jeffrey. 2003. Computability and Logic (4th ed). Cambridge University Press, Cambridge.

Be59 Evert W. Beth. 1959. The Foundations of Mathematics. Studies in Logic and the Foundations of Mathematics. Edited by L. E. J. Brouwer, E. W. Beth, A. Heyting. 1959. North Holland Publishing Company, Amsterdam.

BF58 Paul Bernays and Abraham A. Fraenkel. 1958. Axiomatic Set Theory. Studies in Logic and the Foundations of Mathematics. Edited by L. E. J. Brouwer, E. W. Beth, A. Heyting. 1959. North Holland Publishing Company, Amsterdam.

Br08 L. E. J. Brouwer. 1908. The Unreliability of the Logical Principles. English translation in A. Heyting, Ed. L. E. J. Brouwer: Collected Works 1: Philosophy and Foundations of Mathematics. Amsterdam: North Holland / New York: American Elsevier (1975): pp.107-111.

Br13 L. E. J. Brouwer. 1913. Intuitionism and Formalism. Inaugural address at the University of Amsterdam, October 14, 1912. Translated by Professor Arnold Dresden for the Bulletin of the American Mathematical Society, Volume 20 (1913), pp.81-96. 1999. Electronically published in Bulletin (New Series) of the American Mathematical Society, Volume 37, Number 1, pp.55-64.

Br23 L. E. J. Brouwer. 1923. On the significance of the principle of the excluded middle in mathematics, especially in function theory. Address delivered on 21 September 1923 at the annual convention of the Deutsche Mathematiker-Vereinigung in Marburg an der Lahn. In Jean van Heijenoort. 1967. Ed. From Frege to G&oumldel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

Co66 Paul J. Cohen. 1966. Set Theory and the Continuum Hypothesis. (Lecture notes given at Harvard University, Spring 1965) W. A. Benjamin, Inc., New York.

Cr05 John N. Crossley. 2005. What is Mathematical Logic? A Survey. Address at the First Indian Conference on Logic and its Relationship with Other Disciplines held at the Indian Institute of Technology, Powai, Mumbai from January 8 to 12. Reprinted in Logic at the Crossroads: An Interdisciplinary View – Volume I (pp.3-18). ed. Amitabha Gupta, Rohit Parikh and Johan van Bentham. 2007. Allied Publishers Private Limited, Mumbai.

Da82 Martin Davis. 1958. Computability and Unsolvability. 1982 ed. Dover Publications, Inc., New York.

EC89 Richard L. Epstein, Walter A. Carnielli. 1989. Computability: Computable Functions, Logic, and the Foundations of Mathematics. Wadsworth & Brooks, California.

Fr09 Curtis Franks. 2009. The Autonomy of Mathematical Knowledge: Hilbert’s Program Revisited}. Cambridge University Press, New York.

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.

HA28 David Hilbert & Wilhelm Ackermann. 1928. Principles of Mathematical Logic. Translation of the second edition of the Grundzüge Der Theoretischen Logik. 1928. Springer, Berlin. 1950. Chelsea Publishing Company, New York.

Hi25 David Hilbert. 1925. On the Infinite. Text of an address delivered in Münster on 4th June 1925 at a meeting of the Westphalian Mathematical Society. In Jean van Heijenoort. 1967.Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

Hi27 David Hilbert. 1927. The Foundations of Mathematics. Text of an address delivered in July 1927 at the Hamburg Mathematical Seminar. In Jean van Heijenoort. 1967.Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

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

Kn63 G. T. Kneebone. 1963. Mathematical Logic and the Foundations of Mathematics: An Introductory Survey. D. Van Norstrand Company Limited, London.

Ko25 Andrei Nikolaevich Kolmogorov. 1925. On the principle of excluded middle. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

Li64 A. H. Lightstone. 1964. The Axiomatic Method. Prentice Hall, NJ.

Me64 Elliott Mendelson. 1964. Introduction to Mathematical Logic. Van Norstrand, Princeton.

Ma09 Maria Emilia Maietti. 2009. A minimalist two-level foundation for constructive mathematics. Dipartimento di Matematica Pura ed Applicata, University of Padova.

MS05 Maria Emilia Maietti and Giovanni Sambin. 2005. Toward a minimalist foundation for constructive mathematics. Clarendon Press, Oxford.

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.

Nv64 P. S. Novikov. 1964. Elements of Mathematical Logic. Oliver & Boyd, Edinburgh and London.

Qu63 Willard Van Orman Quine. 1963. Set Theory and its Logic. Harvard University Press, Cambridge, Massachusette.

Rg87 Hartley Rogers Jr. 1987. Theory of Recursive Functions and Effective Computability.<i. MIT Press, Cambridge, Massachusetts.

Ro53 J. Barkley Rosser. 1953. Logic for Mathematicians McGraw Hill, New York.

Sh67 Joseph R. Shoenfield. 1967. Mathematical Logic. Reprinted 2001. A. K. Peters Ltd., Massachusetts.

Sk28 Thoralf Skolem. 1928. On Mathematical Logic Text of a lecture delivered on 22nd October 1928 before the Norwegian Mathematical Association. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

Sm92 Raymond M. Smullyan. 1992. Gödel’s Incompleteness Theorems. Oxford University Press, Inc., New York.

Su60 Patrick Suppes. 1960. Axiomatic Set Theory. Van Norstrand, Princeton.

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

Wa63 Hao Wang. 1963. A survey of Mathematical Logic. North Holland Publishing Company, Amsterdam.

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.

Notes

Return to 5: See for instance: Hi25, p.382; HA28, p.48; Sk28, p.515; Go31, p.32.; Kl52, p.169; Ro53, p.90; BF58, p.46; Be59, pp.178 & 218; Su60, p.3; Wa63, p.314-315; Qu63, pp.12-13; Kn63, p.60; Co66, p.4; Me64, p.52(ii); Nv64, p.92; Li64, p.33; Sh67, p.13; Da82, p.xxv; Rg87, p.xvii; EC89, p.174; Mu91; Sm92, p.18, Ex.3; BBJ03, p.102; Cr05, p.6.

Return to 7: “The formula $\forall x(A(x)\vee \neg A(x))$ is classically provable, and hence under classical interpretation true. But it is unrealizable. So if realizability is accepted as a necessary condition for intuitionistic truth, it is untrue intuitionistically, and therefore unprovable not only in the present intuitionistic formal system, but by any intuitionistic methods whatsoever”. Kl52, p.513.

Author’s working archives & abstracts of investigations

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

$\S 1$ 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 [1].

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 $f(x_{1}, x_{2})$ is representable in the first-order Peano Arithmetic PA by a formula $[F(x_{1}, x_{2}, x_{3})]$ 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.

In this earlier post on the Birmingham paper, we have also shown that:

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.

$\S 2$ Weakening the Church and Turing Theses

We begin by noting that the following theses are classically equivalent [1]:

Standard Church’s Thesis: [2] A number-theoretic function (or relation, treated as a Boolean function) is effectively computable if, and only if, it is recursive [3].

Standard Turing’s Thesis: [4] A number-theoretic function (or relation, treated as a Boolean function) is effectively computable if, and only if, it is Turing-computable [5].

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

$\S 2.1$ 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’ [6].

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[7], 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 $F(n) = G(n)$ of two number-theoretical functions which could be verified up to very great numbers $n$.” [8]

Alan Turing’s perspective

Such a possibility is also implicit in Turing’s remarks [9]:

“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 $\S8$ 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 [10].

Thus, Boolos, Burgess and Jeffrey [11] define a diagonal halting function, $d$, any value of which can be decided effectively, although there is no single algorithm that can effectively compute $d$.

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 [12]!

However, as Boolos, Burgess and Jeffrey note quizically:

“According to Turing’s Thesis, since $d$ is not Turing-computable, $d$ cannot be effectively computable. Why not? After all, although no Turing machine computes the function $d$, we were able to compute at least its first few values, For since, as we have noted, $f_{1} = f_{2} = f_{3} =$ the empty function we have $d(1) = d(2) = d(3) = 1$. And it may seem that we can actually compute $d(n)$ for any positive integer $n$—if we don’t run out of time.” [13]

Why should Chaitin’s constant $\Omega$ be labelled uncomputable’?

The reluctance to treat a function such as $d(n)$—or the function $\Omega(n)$ that computes the $n^{th}$ digit in the decimal expression of a Chaitin constant $\Omega$ [14]—as computable, on the grounds that the time’ needed to compute it increases monotonically with $n$, is curious [15]; the same applies to any total Turing-computable function $f(n)$![16]

Moreover, such a reluctance to treat instantiationally computable functions such as $d(n)$ 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).

$\S 2.2$ Distinguishing between algorithmic verifiability and algorithmic computability

We now show in Theorem 1 that if Aristotle’s particularisation is presumed valid over the structure $\mathbb{N}$ 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 [17]) Gödel $\beta$-function that a primitive recursive relation can be instantiationally equivalent to an arithmetical relation, where the former is algorithmically computable over $\mathbb{N}$, whilst the latter is algorithmically verifiable (i.e., instantiationally computable) but not algorithmically computable over $\mathbb{N}$.[18]

$\S 2.2.1$ Significance of Gödel’s $\beta$-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 $f(x)$ and any natural number $n$, we can construct a primitive recursive function $\beta(z, y, x)$ and natural numbers $b_{n}, c_{n}$ such that $\beta(b_{n}, c_{n}, i)$ $= f(i)$ for all $0 \leq i \leq n$.

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 $A(x)$ such that:

(a) for any given natural number $n$, there is an algorithm that can verify $A(i) = f(i)$ for all $0 \leq i \leq n$ (hence $A(x)$ may be said to be algorithmically verifiable if $f(x)$ is recursive);

(b) there is no algorithm that can verify $A(i) = f(i)$ for all $0 \leq i$ (so $A(x)$ may be said to be algorithmically uncomputable)?

$\S 2.2.2$ Defining effective computability

Now, in the Birmingham paper (reproduced in this post), we have formally defined what it means for a formula of an arithmetical language to be:

(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 [19].

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.

$\S 3$ 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 $\beta$-function—as [20]:

Definition 1: $\beta (x_{1}, x_{2}, x_{3}) = rm(1+(x_{3}+ 1) \star x_{2}, x_{1})$

where $rm(x_{1}, x_{2})$ denotes the remainder obtained on dividing $x_{2}$ by $x_{1}$.

Gödel showed that the above function has the remarkable property that:

Lemma 1: For any given denumerable sequence of natural numbers, say $f(k, 0),\ f(k, 1),\ \ldots$, and any given natural number $n$, we can construct natural numbers $b, c, j$ such that:

(i) $j = max(n, f(k, 0), f(k, 1), \ldots, f(k, n))$;

(ii) $c = j$!;

(iii) $\beta(b, c, i) = f(k, i)$ for $0 \leq i \leq n$.

Proof: This is a standard result [21]. $\Box$

Now we have the standard definition [22]:

Definition 2: A number-theoretic function $f(x_{1}, \ldots, x_{n})$ is said to be representable in PA if, and only if, there is a PA formula $[F(x_{1}, \dots, x_{n+1})]$ with the free variables $[x_{1}, \ldots, x_{n+1}]$, such that, for any given natural numbers $k_{1}, \ldots, k_{n+1}$:

(i) if $f(k_{1}, \ldots, k_{n}) = k_{n+1}$ then PA proves: $[F(k_{1}, \ldots, k_{n}, k_{n+1})]$;

(ii) PA proves: $[(\exists_{1} x_{n+1})F(k_{1}, \ldots, k_{n}, x_{n+1})]$.

The function $f(x_{1}, \ldots, x_{n})$ is said to be strongly representable in PA if we further have that:

(iii) PA proves: $[(\exists_{1} x_{n+1})F(x_{1}, \ldots, x_{n}, x_{n+1})]$

Interpretation of $[\exists_{1}]$‘: The symbol $[\exists_{1}]$‘ denotes uniqueness’ under an interpretation which assumes that Aristotle’s particularisation holds in the domain of the interpretation.

Formally, however, the PA formula:

$[(\exists_{1} x_{3})F(x_{1}, x_{2}, x_{3})]$

is merely a short-hand notation for the PA formula:

$[\neg(\forall x_{3})\neg F(x_{1}, x_{2}, x_{3}) \wedge (\forall y)(\forall z)(F(x_{1}, x_{2}, y) \wedge F(x_{1}, x_{2}, z) \rightarrow y=z)]$.

We then have:

Lemma 2 $\beta(x_{1}, x_{2}, x_{3})$ is strongly represented in PA by $[Bt(x_{1}, x_{2}, x_{3}, x_{4})]$, which is defined as follows:

$[(\exists w)(x_{1} = ((1 + (x_{3} + 1)\star x_{2}) \star w + x_{4}) \wedge (x_{4} < 1 + (x_{3} + 1) \star x_{2}))]$.

Proof: This is a standard result [23]. $\Box$

Gödel further showed (also under the tacit, but critical, presumption of Aristotle’s particularisation [24] that:

Lemma 3: If $f(x_{1}, x_{2})$ is a recursive function defined by:

(i) $f(x_{1}, 0) = g(x_{1})$

(ii) $f(x_{1}, (x_{2}+1)) = h(x_{1}, x_{2}, f(x_{1}, x_{2}))$

where $g(x_{1})$ and $h(x_{1}, x_{2}, x_{3})$ are recursive functions of lower rank [25] that are represented in PA by well-formed formulas $[G(x_{1}, x_{2})]$ and $[H(x_{1}, x_{2}, x_{3}, x_{4})]$,

then $f(x_{1}, x_{2})$ is represented in PA by the following well-formed formula, denoted by $[F(x_{1}, x_{2}, x_{3})]$:

$[(\exists u)(\exists v)(((\exists w)(Bt(u, v, 0, w) \wedge G(x_{1}, w))) \wedge Bt(u, v, x_{2}, x_{3}) \wedge (\forall w)(w < x_{2} \rightarrow (\exists y)(\exists z)(Bt(u, v, w, y) \wedge Bt(u, v, (w+1), z) \wedge H(x_{1}, w, y, z)))].$

Proof: This is a standard result [26]. $\Box$

$\S 4.1$ What does “$[(\exists_{1} x_{3})F(k, m, x_{3})]$ is provable” assert under the standard interpretation of PA?

Now, if the PA formula $[F(x_{1}, x_{2}, x_{3})]$ represents in PA the recursive function denoted by $f(x_{1}, x_{2})$ then by definition, for any given numerals $[k], [m]$, the formula $[(\exists_{1} x_{3})F(k, m, x_{3})]$ is provable in PA; and true under the standard interpretation of PA.

We thus have that:

Lemma 4:$[(\exists_{1} x_{3})F(k, m, x_{3})]$ is true under the standard interpretation of PA” is the assertion that:

Given any natural numbers $k, m$, we can construct natural numbers $t_{(k, m)}, u_{(k, m)}, v_{(k, m)}$—all functions of $k, m$—such that:

(a) $\beta(u_{(k, m)}, v_{(k, m)}, 0) = g(k)$;

(b) for all $i, $\beta(u_{(k, m)}, v_{(k, m)}, i) = h(k, i, f(k, i))$;

(c) $\beta(u_{(k, m)}, v_{(k, m)}, m) = t_{(k, m)}$;

where $f(x_{1}, x_{2})$, $g(x_{1})$ and $h(x_{1}, x_{2}, x_{3})$ are any recursive functions that are formally represented in PA by $F(x_{1}, x_{2}, x_{3}), G(x_{1}, x_{2})$ and $H(x_{1}, x_{2}, x_{3}, x_{4})$ respectively such that:

(i) $f(k, 0) = g(k)$

(ii) $f(k, (y+1)) = h(k, y, f(k, y))$ for all $y

(iii) $g(x_{1})$ and $h(x_{1}, x_{2}, x_{3})$ are recursive functions that are assumed to be of lower rank than $f(x_{1}, x_{2})$.

Proof: For any given natural numbers $k$ and $m$, if $[F(x_{1}, x_{2}, x_{3})]$ interprets as a well-defined arithmetical relation under the standard interpretation of PA, then we can define a deterministic Turing machine $TM$ that can construct’ the sequences:

$f(k, 0), f(k, 1), \ldots, f(k, m)$

and:

$\beta(u_{(k, m)}, v_{(k, m)}, 0), \beta(u_{(k, m)}, v_{(k, m)}, 1), \ldots, \beta(u_{(k, m)}, v_{(k, m)}, m)$

and give evidence to verify the assertion. $\Box$[27]

We now see that:

Theorem 1: Under the standard interpretation of PA $[(\exists_{1} x_{3})F(x_{1}, x_{2}, x_{3})]$ is algorithmically verifiable, but not algorithmically computable, as always true over $\mathbb{N}$.

Proof: It follows from Lemma 4 that:

(1) $[(\exists_{1} x_{3})F(k, m, x_{3})]$ is PA-provable for any given numerals $[k, m]$. Hence $[(\exists_{1} x_{3})F(k, m, x_{3})]$ is true under the standard interpretation of PA. It then follows from the definition of $[F(x_{1}, x_{2}, x_{3})]$ in Lemma 3 that, for any given natural numbers $k, m$, we can construct some pair of natural numbers $u_{(k, m)}, v_{(k, m)}$—where $u_{(k, m)}, v_{(k, m)}$ are functions of the given natural numbers $k$ and $m$—such that:

(a) $\beta(u_{(k, m)}, v_{(k, m)}, i) = f(k, i)$ for $0 \leq i \leq m$;

(b) $F^{*}(k, m, f(k, m))$ holds in $\mathbb{N}$.

Since $\beta(x_{1}, x_{2}, x_{3})$ is primitive recursive, $\beta(u_{(k, m)}, v_{(k, m)}, i)$ defines a deterministic Turing machine $TM$ that can construct’ the denumerable sequence $f'(k, 0), f'(k, 1), \ldots$ for any given natural numbers $k$ and $m$ such that:

(c) $f(k, i) = f'(k, i)$ for $0 \leq i \leq m$.

We can thus define a deterministic Turing machine $TM$ that will give evidence that the PA formula $[(\exists_{1} x_{3})F(k, m, x_{3})]$ is true under the standard interpretation of PA.

Hence $[(\exists_{1} x_{3})F(x_{1}, x_{2}, x_{3})]$ is algorithmically verifiable over $\mathbb{N}$ under the standard interpretation of PA.

(2) Now, the pair of natural numbers $u_{(x_{1}, x_{2})}, v_{(x_{1}, x_{2})}$ are defined such that:

(a) $\beta(u_{(x_{1}, x_{2})}, v_{(x_{1}, x_{2})}, i) = f(x_{1}, i)$ for $0 \leq i \leq x_{2}$;

(b) $F^{*}(x_{1}, x_{2}, f(x_{1}, x_{2}))$ holds in $\mathbb{N}$;

where $v_{(x_{1}, x_{2})}$ is defined in Lemma 3 as $j$!, and:

(c) $j = max(n, f(x_{1}, 0), f(x_{1}, 1), \ldots, f(x_{1}, x_{2}))$;

(d) $n$ is the number’ of terms in the sequence $f(x_{1}, 0), f(x_{1}, 1), \ldots, f(x_{1}, x_{2})$.

Since $j$ is not definable for a denumerable sequence $\beta(u_{(x_{1}, x_{2})}, v_{(x_{1}, x_{2})}, i)$ we cannot define a denumerable sequence $f'(x_{1}, 0), f'(x_{1}, 1), \ldots$ such that:

(e) $f(k, i) = f'(k, i)$ for all $i \geq 0$.

We cannot thus define a deterministic Turing machine $TM$ that will give evidence that the PA formula $[(\exists_{1} x_{3})F(x_{1}, x_{2}, x_{3})]$ interprets as true under the standard interpretation of PA for any given sequence of numerals $[(a_{1}, a_{2})]$.

Hence $[(\exists_{1} x_{3})F(x_{1}, x_{2}, x_{3})]$ is not algorithmically computable over $\mathbb{N}$ under the standard interpretation of PA.

The theorem follows. $\Box$

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 $\S 2$—rather than as identities—without any apparent loss of generality.

References

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.

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.

Notes

Return to 2: Church’s (original) Thesis: The effectively computable number-theoretic functions are the algorithmically computable number-theoretic functions Ch36.

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 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, $\S9(II)$, 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 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 14: Chaitin’s Halting Probability is given by $0 < \Omega = \sum2^{-|p|} < 1$, where the summation is over all self-delimiting programs $p$ that halt, and $|p|$ is the size in bits of the halting program $p$; see Ct75.

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 $f(n)$ for any given natural number $n$; in the former, we know we may need distinctly different programs for computing $f(n)$ for different values of $n$, where the length of the program will, sometime, reference $n$.

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 $\mathbb{N}$, whilst the latter is algorithmically verifiable but not algorithmically computable over $\mathbb{N}$.

Return to 19: See the Provability Theorem for PA in this post.

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 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 27: A critical philosophical issue that we do not address here is whether the PA formula $[F(x_{1}, x_{2}, x_{3}]$ can be considered to interpret under a sound interpretation of PA as a well-defined predicate, since the denumerable sequences $\{f(k, 0), f(k, 1), \ldots, f(k, m), m_{p}: p>0$ and $m_{p}$ is not equal to $m_{q}$ if $p$ is not equal to $q\}$—are represented by denumerable, distinctly different, functions $\beta(u_{p_{1}}, v_{p_{2}}, i)$ respectively. There are thus denumerable pairs $(u_{p_{1}}, v_{p_{2}})$ for which $\beta(u_{p_{1}}, v_{p_{2}}, i)$ yields the sequence $f(k, 0), f(k, 1), \ldots, f(k, m)$.

Author’s working archives & abstracts of investigations

A foundational argument for defining Effective Computability formally, and weakening the Church and Turing Theses – I

(Notations, non-standard concepts, and definitions used commonly in these investigations are detailed in this post.)

$\S 1.1$ The Philosophical Issue

In a previous post we have argued that standard interpretations of classical theory may inadvertently be weakening a desirable perception—of mathematics as the lingua franca of scientific expression—by ignoring the possibility that since mathematics is, indeed, indisputably accepted as the language that most effectively expresses and communicates intuitive truth, the chasm between formal truth and provability must, of necessity, be bridgeable.

We further queried whether the roots of such interpretations may lie in removable ambiguities that currently persist in the classical definitions of foundational elements; ambiguities that allow the introduction of non-constructive—hence non-verifiable, non-computational, ambiguous and essentially Platonic—elements into the standard interpretations of classical mathematics.

Query 1: Are formal classical theories essentially unable to adequately express the extent and range of human cognition, or does the problem lie in the way formal theories are classically interpreted at the moment?

We noted that the former addressed the question of whether there are absolute limits on our capacity to express human cognition unambiguously; the latter, whether there are only temporal limits—not necessarily absolute—to the capacity of classical interpretations to communicate unambiguously that which we intended to capture within our formal expression.

We argued that, prima facie, applied science continues, perforce, to interpret mathematical concepts Platonically, whilst waiting for mathematics to provide suitable, and hopefully reliable, answers as to how best it may faithfully express its observations verifiably.

$\S 1.2$ Are axiomatic computational concepts really unambiguous?

This now raises the corresponding philosophical question that is implicit in Selmer Bringsjord’s narrational case against Church’s Thesis [1]:

Query 2 Is there a duality in the classical acceptance of non-constructive, foundational, concepts as axiomatic?

We now argue that beyond the question raised in an earlier post of whether—as computer scientist Lance Fortnow believes—Turing machines can capture everything we can compute’, or whether—as computer scientists Peter Wegner and Dina Goldin suggest—they are inappropriate as a universal foundation for computational problem solving’, we also need to address the philosophical question—implicit in Bringsjord’s paper—of whether, or not, the concept of effective computability’ is capable of a constructive, and intuitionistically unobjectionable, definition; and the relation of such definition to that of formal provability and to the standard perceptions of the Church and Turing Theses as reviewed here by at heart Trinity mathmo and by profession Philosopher Peter Smith.

We therefore consider the case for introduction of such a definition from a philosophical point of view, and consider some consequences.

$\S 1.2.1$ Mendelson’s thesis

We note that Elliott Mendelson [2] is quoted by Bringsjord in his paper as saying (italicised parenthetical qualifications added):

(i) “Here is the main conclusion I wish to draw:

it is completely unwarranted to say that CT is unprovable just because it states an equivalence between a vague, imprecise notion (effectively computable function) and a precise mathematical notion (partial-recursive function)”.

(ii) “The concepts and assumptions that support the notion of partial-recursive function are, in an essential way, no less vague and imprecise (non-constructive, and intuitionistically objectionable) than the notion of effectively computable function; the former are just more familiar and are part of a respectable theory with connections to other parts of logic and mathematics.

(The notion of effectively computable function could have been incorporated into an axiomatic presentation of classical mathematics, but the acceptance of CT made this unnecessary.) …

Functions are defined in terms of sets, but the concept of set is no clearer (not more non-constructive, and intuitionistically objectionable) than that of function and a foundation of mathematics can be based on a theory using function as primitive notion instead of set.

Tarski’s definition of truth is formulated in set-theoretic terms, but the notion of set is no clearer (not more non-constructive, and intuitionistically objectionable), than that of truth.

The model-theoretic definition of logical validity is based ultimately on set theory, the foundations of which are no clearer (not more non-constructive, and intuitionistically objectionable) than our intuitive (non-constructive, and intuitionistically objectionable) understanding of logical validity”.

(iii) “The notion of Turing-computable function is no clearer (not more non-constructive, and intuitionistically objectionable) than, nor more mathematically useful (foundationally speaking) than, the notion of an effectively computable function …”

where:

(a) The Church-Turing Thesis, CT, is formulated as:

“A function is effectively computable if and only if it is Turing-computable”.

(b) An effectively computable function is defined to be the computing of the function by an algorithm.

(c) The classical notion of an algorithm is expressed by Mendelson as:

“… an effective and completely specified procedure for solving a whole class of problems. …

An algorithm does not require ingenuity; its application is prescribed in advance and does not depend upon any empirical or random factors”.

and, where Bringsjord paraphrases (iii) as:

(iv) “The notion of a formally defined program for guiding the operation of a TM is no clearer than, nor more mathematically useful (foundationally speaking) than, the notion of an algorithm”.

(v) “This proposition, it would then seem, is the very heart of the matter.

If (iv) is true then Mendelson has made his case; if this proposition is false, then his case is doomed, since we can chain back by modus tollens and negate (iii)”.

$\S 1.2.2$ The concept of constructive, and intuitionistically unobjectionable’

Now, prima facie, any formalisation of a vague and imprecise’, intuitive’ concept—say C—would normally be intended to capture the concept C both faithfully and completely within a constructive, and intuitionistically unobjectionable [3], language L.

Clearly, we could disprove the thesis—that C and its formalisation L are interchangeable, hence equivalent—by showing that there is a constructive aspect of C that is formalisable in a constructive language L’, but that such formalisation cannot be assumed expressible in L without introducing inconsistency.

However, equally clearly, there can be no way of proving the equivalence as this would contradict the premise that the concept is vague and imprecise’, hence essentially open-ended in a non-definable way, and so non-formalisable.

Obviously, Mendelson’s assertion that there is no justification for claiming Church’s Thesis as unprovable must, therefore, rely on an interpretation that differs significantly from the above; for instance, his concept of provability may appeal to the axiomatic acceptability of vague and imprecise’ concepts—as suggested by his remarks.

Now, we note that all the examples cited by Mendelson involve the decidability (computability) of an infinitude of meta-mathematical instances, where the distinction between the constructive meta-assertion that any given instance is individually decidable (instantiationally computable), and the non-constructive meta-assertion that all the instances are jointly decidable (uniformly computable), is not addressed explicitly.

However, $\S 1.2.1(a)$, $\S 1.2.1(b)$ and $\S 1.2.1(c)$ appear to suggest that Mendelson’s remarks relate implicitly to non-constructive meta-assertions.

Perhaps the real issue, then, is the one that emerges if we replace Mendelson’s use of implicitly open-ended concepts such as vague and imprecise’ and intuitive’ by the more meta-mathematically meaningful concept of non-constructive, and intuitionistically objectionable’, as italicised and indicated parenthetically.

The essence of Mendelson’s meta-assertion $\S 1.2.1(iii)$ then appears to be that, if the classically accepted definitions of foundational concepts such as partial recursive function’, function’, Tarskian truth’ etc. are also non-constructive, and intuitionistically objectionable, then replacing one non-constructive concept by another may be psychologically unappealing, but it should be meta-mathematically valid and acceptable.

$\S 1.2.3$ The duality

Clearly, meta-assertion $\S 1.2.1(iii)$ would stand refuted by a non-algorithmic’ effective method that is constructive.

However, if it is explicitly—and, as suggested by the nature of the arguments in Bringsjord’s paper, widely—accepted at the outset that any effective method is necessarily algorithmic (i.e. uniform as stated in $\S 1.2.1(c)$ above), then any counter-argument to CT can, prima facie, only offer non-algorithmic methods that may, paradoxically, be effective’ intuitively but in a non-constructive, and intuitionistically objectionable, way only!

Recognition of this dilemma is implicit in the admission that the various arguments, as presented by Bringsjord in the case against Church’s Thesis—including his narrational case—are open to reasonable, but inconclusive, refutations.

Nevertheless, if we accept Mendelson’s thesis that the inter-changeability of non-constructive concepts is valid in the foundations of mathematics, then Bringsjord’s case against Church’s Thesis, since it is based similarly on non-constructive concepts, should also be considered conclusive classically (even though it cannot, prima facie, be considered constructively conclusive in an intuitionistically unobjectionable way).

There is, thus, an apparent duality in the—seemingly extra-logical—decision as to whether an argument based on non-constructive concepts may be accepted as classically conclusive or not.

That this duality may originate in the very issues raised in Mendelson’s remarks—concerning the non-constructive roots of foundational concepts that are classically accepted as mathematically sound—is seen if we note that these issues may be more significant than is, prima facie, apparent.

$\S 1.2.4$ Definition of a formal mathematical object, and consequences

Thus, if we define a formal mathematical object as any symbol for an individual letter, function letter or a predicate letter that can be introduced through definition into a formal theory without inviting inconsistency, then it can be argued that unrestricted, non-constructive, definitions of non-constructive, foundational, set-theoretic concepts—such as mapping’, function’, recursively enumerable set’, etc.—in terms of constructive number-theoretic concepts—such as recursive number-theoretic functions and relations—may not always correspond to formal mathematical objects.

In other words, the assumption that every definition corresponds to a formal mathematical object may introduce a formal inconsistency into standard Peano Arithmetic and, ipso facto, into any Axiomatic Set Theory that models standard PA (an inconsistency which, loosely speaking, may be viewed as a constructive arithmetical parallel to Russell’s non-constructive impredicative set).

Since it can also be argued that the non-constructive element in Tarski’s definitions of satisfiability’ and truth’, and in Church’s Thesis, originate in a common, but removable, ambiguity in the interpretation of an effective method, perhaps it is worth considering whether Bringsjord’s acceptance of the assumption—that every constructive effective method is necessarily algorithmic, in the sense of being a uniform procedure as in $\S 1.2.1(c)$ above—is mathematically necessary, or even whether it is at all intuitively tenable.

(Uniform procedure: A property usually taken to be a necessary condition for a procedure to qualify as effective.)

Thus, we may argue that we can explicitly and constructively define a non-algorithmic’ effective method as one that, in any given instance, is instantiationally computable if, and only if, it terminates finitely with a conclusive result; and an algorithmic’ effective method as one that is uniformly computable if, and only if, it terminates finitely, with a conclusive result, in any given instance. [4]

$\S 1.2.5$ Bringsjord’s case against CT

Apropos the specific arguments against CT it would seem, prima facie, that a non-algorithmic effective—even if not obviously constructive—method could be implicit in the following argument considered by Bringsjord:

“Assume for the sake of argument that all human cognition consists in the execution of effective processes (in brains, perhaps). It would then follow by CT that such processes are Turing-computable, i.e., that computationalism is true. However, if computationalism is false, while there remains incontrovertible evidence that human cognition consists in the execution of effective processes, CT is overthrown”.

Assuming computationalism is false, the issue in this argument would, then, be whether there is a constructive, and adequate, expression of human cognition in terms of individually effective methods.

An appeal to such a non-algorithmic effective method may, in fact, be implicit in Bringsjord’s consideration of the predicate H, defined by:

$H(P, i)$ iff $(\exists n)S(P, i, n)$

where the predicate $S(P, u, n)$ holds if, and only if, TM M, running program P on input $u$, halts in exactly $n$ steps ($= MP : u =>n$ halt).

Bringsjord’s Total Computability

Bringsjord defines S as totally (and, implicitly, uniformly) computable in the sense that, given some triple $(P, u, n)$, there is some (uniform) program P* which, running on some TM M*, can infallibly give us a verdict, Y (yes’) or N (no’), for whether or not S is true of this triple.

He then notes that, since the ability to (uniformly) determine, for a pair $(P, i)$, whether or not H is true of it, is equivalent to solving the full halting problem, H is not totally computable.

Bringsjord’s Partial Computability

However, he also notes that there is a program (implicitly non-uniform, and so, possibly, effective individually) which, when asked whether or not some TM M run by P on $u$ halts, will produce Y iff $MP : u =>n$ halt. For this reason H is declared partially (implicitly, individually) computable.

More explicitly, Bringsjord remarks that Laszlo Kalmár’s refutation of CT [5] is classically inconclusive mainly because it does not admit any uniform effective method, but appeals to the existence of an infinitude of individually effective methods.

Kalmár’s Perspective of CT

Considering that it always seeks to calculate $g(n)$ (defined below) constructively even in the absence of a uniform procedure—not necessarily within a fixed postulate system—we shall show that Kalmár’s finitary argument ([6]as reproduced below from Bringsjord’s paper) makes a pertinent observation:

“First, he draws our attention to a function $g$ that isn’t Turing-computable, given that $f$ is [7]:

$g(x) = \mu y(f(x, y) = 0)$ = {the least $y$ such that $f(x, y) = 0$ if $y$ exists; and $0$ if there is no such $y$}

Kalmár proceeds to point out that for any $n$ in $N$ for which a natural number $y$ with $f(n, y) = 0$ exists,

an obvious method for the calculation of the least such $y$ … can be given,’

namely, calculate in succession the values $f(n, 0), f(n, 1), f(n, 2), \ldots$ (which, by hypothesis, is something a computist or TM can do) until we hit a natural number $m$ such that $f(n, m) = 0$, and set $y = m$.

On the other hand, for any natural number $n$ for which we can prove, not in the frame of some fixed postulate system but by means of arbitrary—of course, correct—arguments that no natural number $y$ with $f(n, y) = 0$ exists, we have also a method to calculate the value $g(n)$ in a finite number of steps.

Kalmár goes on to argue as follows. The definition of $g$ itself implies the tertium non datur, and from it and CT we can infer the existence of a natural number $p$ which is such that

(*) there is no natural number $y$ such that $f(p, y)= 0$; and

(**) this cannot be proved by any correct means.

Kalmár claims that (*) and (**) are very strange, and that therefore CT is at the very least implausible.”

Distinguishing between individually effective computability and uniformly effective computability

Now, the significant point that emerges from Bringsjord’s and Kalmár’s philosophical arguments is the need to distinguish formally between non-algorithmic (i.e., instantiational) computability (or, more precisely, algorithmic verifiability as defined here) and algorithmic (i.e., uniform) computability (or, more precisely, algorithmic computability as defined here) as highlighted in the Birmingham paper.

In the next post we note that this point has also been raised from a more formal, logical, perspective; and consider what is arguably an intuitively-more-adequate formal definability of effective computability’ in terms of ‘algorithmic verifiability’ under which the classical Church and Turing Theses do not hold, but weakened Church and Turing Theses do!

References

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.

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.

Notes

Return to 3: The terms constructive’ and constructive, and intuitionistically unobjectionable’ are used synonymously both in their familiar linguistic sense, and in a mathematically precise sense. Mathematically, we term a concept as constructive, and intuitionistically unobjectionable’ if, and only if, it can be defined in terms of pre-existing concepts without inviting inconsistency. Otherwise, we understand it to mean unambiguously verifiable, by some effective method’, within some finite, well-defined, language or meta-language. It may also be taken to correspond, broadly, to the concept of constructive, and intuitionistically unobjectionable’ in the sense apparently intended by Gödel in his seminal 1931 paper Go31, p.26.

Return to 4: We note that the possibility of a distinction between the interpreted number-theoretic meta-assertions, For any given natural number $x$, $F(x)$ is true’ and $F(x)$ is true for all natural numbers $x$‘, is not evident unless these are expressed symbolically as, $(\forall x)(F(x)$ is true)’ and $(\forall x)F(x)$ is true’, respectively. The issue, then, is whether the distinction can be given any mathematical significance. For instance, under a constructive formulation of Tarski’s definitions, we may qualify the latter by saying that it can be meaningfully asserted as a totality only if $F$‘ is a well-defined mathematical object.

Return to 7: Bringsjord notes that the original proof can be found on page 741 of Kleene Kl36.

Return to 8: We detail a formal proof of this Thesis in this post.

Author’s working archives & abstracts of investigations

So where exactly does the buck stop?

Another reason why Lucas and Penrose should not be faulted for continuing to believe in their well-known Gödelian arguments against computationalism lies in the lack of an adequate consensus on the concept of effective computability’.

For instance, Boolos, Burgess and Jeffrey (2003: Computability and Logic, 4th ed.~CUP, p37) define a diagonal halting function, $d$, any value of which can be computed effectively, although there is no single algorithm that can effectively compute $d$.

“According to Turing’s Thesis, since $d$ is not Turing-computable, $d$ cannot be effectively computable. Why not? After all, although no Turing machine computes the function $d$, we were able to compute at least its first few values, For since, as we have noted, $f_{1} = f_{2} = f_{3} =$ the empty function we have $d(1) = d(2) = d(3) = 1$. And it may seem that we can actually compute $d(n)$ for any positive integer $n$—if we don’t run out of time.”
… ibid. 2003. p37.

Now, the straightforward way of expressing this phenomenon should be to say that there are well-defined real numbers that are instantiationally computable, but not algorithmically computable.

Yet, following Church and Turing, such functions are labeled as effectively uncomputable!

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.

First, we may mean that an individually conceivable object exists, within a language $L$, if it lies within the range of the variables of $L$. The existence of such objects is necessarily derived from the grammar, and rules of construction, of the appropriate constant terms of the language—generally finitary in recursively defined languages—and can be termed as constructive in $L$ by definition.

Second, we may mean that an individually conceivable object exists, under a formal interpretation of $L$ in another formal language, say $L$, if it lies within the range of a variable of $L$ under the interpretation.

Again, the existence of such an object in $L$ is necessarily derivable from the grammar, and rules of construction, of the appropriate constant terms of $L$, and can be termed as constructive in $L$ by definition.

Third, we may mean that an individually conceivable object exists, in an interpretation $M$ of $L$, if it lies within the range of an interpreted variable of $L$, where $M$ is a Platonic interpretation of $L$ in an individual’s subjective mental conception (in Brouwer’s sense).

Clearly, the debatable issue is the third case.

So the question is whether we can—and, if so, how we may—correspond the Platonically conceivable objects of various individual interpretations of $L$, say $M$, $M$, $M$, …, unambiguously to the mathematical objects that are definable as the constant terms of $L$.

If we can achieve this, we can then attempt to relate $L$ to a common external world and try to communicate effectively about our individual mental concepts of the world that we accept as lying, by consensus, in a common, Platonic, concept-space’.

For mathematical languages, such a common concept-space’ is implicitly accepted as the collection of individual intuitive, Platonically conceivable, perceptions—$M$, $M$, $M$, …,—of the standard intuitive interpretation, say $M$, of Dedekind’s axiomatic formulation of the Peano Postulates.

Reasonably, if we intend a language or a set of languages to be adequate, first, for the expression of the abstract concepts of collective individual consciousnesses, and, second, for the unambiguous and effective communication of those of such concepts that we can accept as lying within our common concept-space, then we need to give effective guidelines for determining the Platonically conceivable mathematical objects of an individual perception of $M$ that we can agree upon, by common consensus, as corresponding to the constants (mathematical objects) definable within the language.

Now, in the case of mathematical languages in standard expositions of classical theory, this role is sought to be filled by the Church-Turing Thesis (CT). Its standard formulation postulates that every number-theoretic function (or relation, treated as a Boolean function) of $M$, which can intuitively be termed as effectively computable, is partial recursive / Turing-computable.

However, CT does not succeed in its objective completely.

Thus, even if we accept CT, we still cannot conclude that we have specified explicitly that the domain of $M$ consists of only constructive mathematical objects that can be represented in the most basic of our formal mathematical languages, namely, first-order Peano Arithmetic (PA) and Recursive Arithmetic (RA).

The reason seems to be that CT is postulated as a strong identity, which, prima facie, goes beyond the minimum requirements for the correspondence between the Platonically conceivable mathematical objects of $M$ and those of PA and RA.

“We now define the notion, already discussed, of an effectively calculable function of positive integers by identifying it with the notion of a recursive function of positive integers.”
… Church 1936: An unsolvable problem of elementary number theory, Am.~J.~Math., Vol.~58, pp.~345–363.

“The theorem that all effectively calculable sequences are computable and its converse are proved below in outline.
… Turing 1936: On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, ser.~2.~vol.~42 (1936–7), pp.~230–265.

This violation of the principle of Occam’s Razor is highlighted if we note (e.g., Gödel 1931: On undecidable propositions of Principia Mathematica and related systems I, Theorem VII) that, pedantically, every recursive function (or relation) is not shown as identical to a unique arithmetical function (or relation), but (see the comment following Lemma 9 of this paper) only as instantiationally equivalent to an infinity of arithmetical functions (or relations).

Now, the standard form of CT only postulates algorithmically computable number-theoretic functions of $M$ as effectively computable.

It overlooks the possibility that there may be number-theoretic functions and relations which are effectively computable / decidable instantiationally in a Tarskian sense, but not algorithmically.

References

BBJ03 George S. Boolos, John P. Burgess, Richard C. Jeffrey. 2003. Computability and Logic. (4th ed). Cambridge University Press, Cambridge.

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. pp.5-38.

Lu61 John Randolph Lucas. 1961. Minds, Machines and Gödel. In Philosophy. Vol. 36, No. 137 (Apr. – Jul., 1961), pp. 112-127, Cambridge University Press.

Lu03 John Randolph Lucas. 2003. The Gödelian Argument: Turn Over the Page. In Etica & Politica / Ethics & Politics, 2003, 1.

Lu06 John Randolph Lucas. 2006. Reason and Reality. Edited by Charles Tandy. Ria University Press, Palo Alto, California.

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

Pe90 Roger Penrose. 1990. The Emperor’s New Mind: Concerning Computers, Minds and the Laws of Physics. 1990, Vintage edition. Oxford University Press.

Pe94 Roger Penrose. 1994. Shadows of the Mind: A Search for the Missing Science of Consciousness. Oxford University Press.

Sc67 Joseph R. Schoenfield. 1967. Mathematical Logic. Reprinted 2001. A. K. Peters Ltd., Massachusetts.

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-278). ed. John Corcoran. 1983. Hackett Publishing Company, Indianapolis.

Wa63 Hao Wang. 1963. A survey of Mathematical Logic. North Holland Publishing Company, Amsterdam.

An07a Bhupinder Singh Anand. 2007. The Mechanist’s challenge. In The Reasoner, Vol(1)5 p5-6.

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.

Author’s working archives & abstracts of investigations

A finitary arithmetical perspective on the forcing of non-standard models onto PA

(Notations, non-standard concepts, and definitions used commonly in these investigations are detailed in this post.)

In the previous post we formally argued that the first order Peano Arithmetic PA is categorical from a finitary perspective ($\S 5$, Corollary 1).

We now argue that conventional wisdom which holds PA as essentially incomplete—and thus precludes categoricity—may appeal to finitarily fragile arguments (as mentioned in this earlier post and in this preprint, now reproduced below) for the existence of non-standard models of the first-order Peano Arithmetic PA.

Such wisdom ought, therefore, to be treated foundationally as equally fragile from a post-computationalist arithmetical perspective within classical logic, rather than accepted as foundationally sound relative to an ante-computationalist perspective of set theory.

Post-computationalist doctrine

“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 …” (cf. Mu91).

$\S 1$ Introduction

Once we accept as logically sound the set-theoretically based meta-argument [1] that the first-order Peano Arithmetic PA [2] can be forced—by an ante-computat- ionalist interpretation of the Compactness Theorem—into admitting non-standard models which contain an infinite’ integer, then the set-theoretical properties [3] of the algebraic and arithmetical structures of such putative models should perhaps follow without serious foundational reservation.

Compactness Theorem: If every finite subset of a set of sentences has a model, then the whole set has a model (BBJ03. p.147).

However we shall argue that, from an arithmetical perspective, we can only conclude by the Compactness Theorem that if $Th(\mathbb{N})$ is the $\mathcal{L}_{A}$-theory of the standard model (interpretation) (Ka91, p.10-11), then we may consistently add to it the following as an additional—not necessarily independent—axiom:

$(\exists y)(y > x)$.

Moreover, we shall argue that even though $(\exists y)(y > x)$ is algorithmically computable (Definition 2) as always true in the standard model (whence all of its instances are in $Th(\mathbb{N})$) we cannot conclude by the Compactness Theorem that:

$\cup_{k \in \mathbb{N}}\{Th(\mathbb{N}) \cup \{c > \underline{n}\ |\ n < k\}\}$

is consistent and has a model $M_{c}$ which contains an infinite’ integer [4].

Reason: We shall argue that the condition $k \in \mathbb{N}$ in the above definition of $\cup_{k \in \mathbb{N}}T_{k}$ requires, first of all, that we must be able to extend $Th(\mathbb{N})$ by the addition of a relativised’ axiom (cf. Fe92; Me64, p.192) such as:

$(\exists y)((x \in \mathbb{N}) \rightarrow (y > x))$,

from which we may conclude the existence of some $c$ such that:

$M_{c} \models c>\underline{n}$ for all $n \in \mathbb{N}$.

However, we shall further show that even this would not yield a model for $Th(\mathbb{N})$ since, by Theorem 1, we cannot introduce a completed’ infinity such as $\mathbb{N}$ into either $Th(\mathbb{N})$ or any model of $Th(\mathbb{N})$!

$\S 1.1$ A post-computationalist doctrine

More generally we shall argue that—if our interest is in the arithmetical properties of models of PA—then we first need to make explicit any appeal to non-constructive considerations such as Aristotle’s particularisation (Definition 3).

We shall then argue that, even from a classical perspective, there are serious foundational, post-computationalist, reservations to accepting that a consistent PA can be forced by the Compactness Theorem into admitting non-standard models which contain elements other than the natural numbers.

Reason: Any arithmetical application of the Compactness Theorem to PA can neither ignore currently accepted post-computationalist doctrines of objectivity—nor contradict the constructive assignments of satisfaction and truth to the atomic formulas of PA (therefore to the compound formulas under Tarski’s inductive definitions) in terms of either algorithmical verifiability or algorithmic computability (An12, $\S 3$).

The significance of this doctrine [5] is that it helps highlight how the algorithmically verifiable (Definition 1) formulas of PA define the classical non-finitary standard interpretation of PA [6] (to which standard arguments for the existence of non-standard models of PA critically appeal).

Accordingly, we shall show that standard arguments which appeal to the ante-computationalist interpretation of the Compactness Theorem—for forcing non-standard models of PA [7] which contain an infinite’ integer—cannot admit constructive assignments of satisfaction and truth [8] (in terms of algorithmical verifiability) to the atomic formulas of their putative extension of PA.

We shall conclude that such arguments therefore questionably postulate by axiomatic fiat that which they seek to prove’!

$\S 1.2$ Standard arguments for non-standard models of PA

In this limited investigation we shall consider only the following three standard arguments for the existence of non-standard models of the first-order Peano Arithmetic PA:

(i) If PA is consistent, then we obtain a non-standard model for PA which contains an infinite’ integer by applying the Compactness Theorem to the union of the set of formulas that are satisfied or true in the classical standard’ model of PA [9] and the countable set of all PA-formulas of the form $[c_{n} = S(c_{n+1})]$.

(ii) If PA is consistent, then we obtain a non-standard model for PA which contains an infinite’ integer by adding a constant $c$ to the language of PA and applying the Compactness Theorem to the theory P$\cup\{c > \underline{n}: \underline{n}\ =\ \underline{0},\ \underline{1},\ \underline{2},\ \ldots\}$.

(iii) If PA is consistent, then we obtain a non-standard model for PA which contains an infinite’ integer by adding the PA formula $[\neg (\forall x)R(x)]$ as an axiom to PA, where $[(\forall x)R(x)]$ is a Gödelian formula [10] that is unprovable in PA, even though $[R(n)$] is provable in PA for any given PA numeral $[n]$ (Go31, p.25(1)).

We shall first argue that (i) and (ii)—which appeal to Thoralf Skolem’s ante-computationalist reasoning (in Sk34) for the existence of a non-standard model of PA—should be treated as foundationally fragile from a finitary, post-computationalist perspective within classical logic [11].

We shall then argue that although (iii)—which appeals to Kurt Gödel’s (also ante-computationalist) reasoning (Go31) for the existence of a non-standard model of PA—does yield a model other than the classical standard’ model of PA, we cannot conclude by even classical (albeit post-computationalist) reasoning that the domain is other than the domain $N$ of the natural numbers unless we make the non-constructive—and logically fragile—extraneous assumption that a consistent PA is necessarily $\omega$-consistent.

($\omega$-consistency): A formal system S is $\omega$-consistent if, and only if, there is no S-formula $[F(x)]$ for which, first, $[\neg(\forall x)F(x)]$ is S-provable and, second, $[F(a)]$ is S-provable for any given S-term $[a]$.

$\S 2$ Algorithmically verifiable formulas and algorithmically computable formulas

We begin by distinguishing between:

Definition 1: An atomic formula $[F(x)]$ [12] of PA is algorithmically verifiable under an interpretation if, and only if, for any given numeral $[n]$, there is an algorithm $AL_{(F,\ n)}$ which can provide objective evidence (Mu91) for deciding the truth value of each formula in the finite sequence of PA formulas $\{[F(1)], [F(2)], \ldots, [F(n)]\}$ under the interpretation.

The concept is well-defined in the sense that 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 (An12).

We note further that the formulas of the first order Peano Arithmetic PA are decidable under the standard interpretation of PA over the domain $\mathbb{N}$ of the natural numbers if, and only if, they are algorithmically verifiable under the interpretation [13].

Definition 2: An atomic formula $[F(x)]$ of PA is algorithmically computable under an interpretation if, and only if, there is an algorithm $AL_{F}$ that can provide objective evidence for deciding the truth value of each formula in the denumerable sequence of PA formulas $\{[F(1)], [F(2)], \ldots\}$ under the interpretation.

This concept too is well-defined in the sense that 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 (An12).

We note further that the PA-formulas are decidable under an algorithmic interpretation of PA over $\mathbb{N}$ if, and only if, they are algorithmically computable under the interpretation [14].

Although we shall not appeal to the following in this paper, we note in passing that the foundational significance [15] of the distinction lies in the argument that:

Lemma 1: There are algorithmically verifiable number theoretical functions which are not algorithmically computable. [16]

Proof: Let $r(n)$ denote the $n^{th}$ digit in the decimal expansion $\sum_{n=1}^{\infty}r(n).10^{-n}$ of a putatively given real number $\mathbb{R}$ in the interval $0 < \mathbb{R} \leq 1$. By the definition of a real number as the limit of a Cauchy sequence of rationals, it follows that $r(n)$ is an algorithmically verifiable number-theoretic function. Since every algorithmically computable real is countable (Tu36), Cantor's diagonal argument (Kl52, pp.6-8) shows that there are real numbers that are not algorithmically computable. The Lemma follows. $\Box$

$\S 3$ Making non-finitary assumptions explicit

We next make explicit—and briefly review—a tacitly held fundamental tenet of classical logic which is unrestrictedly adopted as intuitively obvious by standard literature [17] that seeks to build upon the formal first-order predicate calculus FOL:

Definition 3: (Aristotle’s particularisation) This holds that from an assertion such as:

It is not the case that: For any given $x$, $P^{*}(x)$ does not hold’,

usually denoted symbolically by $\neg(\forall x)\neg P^{*}(x)$‘, we may always validly infer in the classical, Aristotlean, logic of predicates (HA28, pp.58-59) that:

There exists an unspecified $x$ such that $P^{*}(x)$ holds’,

usually denoted symbolically by $(\exists x)P^{*}(x)$‘.

$\S 3.1$ The significance of Aristotle’s particularisation for the first-order predicate calculus

Now we note that in a formal language the formula $[(\exists x)P(x)]$‘ is an abbreviation for the formula $[\neg(\forall x)\neg P(x)]$‘; and that the commonly accepted interpretation of this formula tacitly appeals to Aristotlean particularisation.

However, as L. E. J. Brouwer had noted in his seminal 1908 paper on the unreliability of logical principles (Br08), the commonly accepted interpretation of this formula is ambiguous if interpretation is intended over an infinite domain.

Brouwer essentially argued that, even supposing the formula $[P(x)]$‘ of a formal Arithmetical language interprets as an arithmetical relation denoted by $P^{*}(x)$‘, and the formula $[\neg(\forall x)\neg P(x)]$‘ as the arithmetical proposition denoted by $\neg(\forall x)\neg P^{*}(x)$‘, the formula $[(\exists x)P(x)]$‘ need not interpret as the arithmetical proposition denoted by the usual abbreviation $(\exists x)P^{*}(x)$‘; and that such postulation is invalid as a general logical principle in the absence of a means for constructing some putative object $a$ for which the proposition $P^{*}(a)$ holds in the domain of the interpretation.

Hence we shall follow the convention that the assumption that $(\exists x)P^{*}(x)$‘ is the intended interpretation of the formula $[(\exists x)P(x)]$‘—which is essentially the assumption that Aristotle’s particularisation holds over the domain of the interpretation—must always be explicit.

$\S 3.2$ The significance of Aristotle’s particularisation for PA

In order to avoid intuitionistic objections to his reasoning, Kurt Gödel introduced the syntactic property of $\omega$-consistency [18] as an explicit assumption in his formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions (Go31, p.23 and p.28).

Gödel explained at some length [19] that his reasons for introducing $\omega$-consistency explicitly was to avoid appealing to the semantic concept of classical arithmetical truth in Aristotle’s logic of predicates (which presumes Aristotle’s particularisation).

The two concepts are meta-mathematically equivalent in the sense that, if PA is consistent, then PA is $\omega$-consistent if, and only if, Aristotle’s particularisation holds under the standard interpretation of PA [20].

$\S 4$ The ambiguity in admitting an infinite’ constant

We begin our consideration of standard arguments for the existence of non-standard models of PA which contain an infinite’ integer by first highlighting and eliminating an ambiguity in the argument as it is usually found in standard texts [21]:

Corollary. There is a non-standard model of P with domain the natural numbers in which the denotation of every nonlogical symbol is an arithmetical relation or function.

Proof. As in the proof of the existence of nonstandard models of arithmetic, add a constant $\infty$ to the language of arithmetic and apply the Compactness Theorem to the theory

P$\cup\{\infty \neq$ n: $n\ =\ 0,\ 1,\ 2,\ \ldots\}$

to conclude that it has a model (necessarily infinite, since all models of P are). The denotations of $\infty$ in any such model will be a non-standard element, guaranteeing that the model is non-standard. Then apply the arithmetical Löwenheim-Skolem theorem to conclude that the model may be taken to have domain the natural numbers, and the denotations of all nonlogical symbols arithmetical.”

… BBJ03, p.306, Corollary 25.3.

$\S 4.1$ We cannot force PA to admit a transfinite ordinal

The ambiguity lies in a possible interpretation of the symbol $\infty$ as a completed’ infinity (such as Cantor’s first transfinite ordinal $\omega$) in the context of non-standard models of PA. To eliminate this possibility we establish trivially that, and briefly examine why:

Theorem 1: No model of PA can admit a transfinite ordinal under the standard interpretation of the classical logic FOL[22].

Proof: Let [$G(x)$] denote the PA-formula:

$[x=0 \vee \neg(\forall y)\neg(x=Sy)]$

Since Aristotle’s particularisation is tacitly assumed under the standard interpretation of FOL, this translates in every model of PA, as:

If $x$ denotes an element in the domain of a model of PA, then either $x$ is 0, or $x$ is a successor’.

Further, in every model of PA, if $G(x)$ denotes the interpretation of [$G(x)$]:

(a) $G(0)$ is true;

(b) If $G(x)$ is true, then $G(Sx)$ is true.

Hence, by Gödel’s completeness theorem:

(c) PA proves $[G(0)]$;

(d) PA proves $[G(x) \rightarrow G(Sx)]$.

Gödel’s Completeness Theorem: In any first-order predicate calculus, the theorems are precisely the logically valid well-formed formulas (i. e. those that are true in every model of the calculus).

Further, by Generalisation:

(e) PA proves $[(\forall x)(G(x) \rightarrow G(Sx))]$;

Generalisation in PA: [$(\forall x)A$] follows from [$A$].

Hence, by Induction:

(f) $[(\forall x)G(x)]$ is provable in PA.

Induction Axiom Schema of PA: For any formula [$F(x)$] of PA:

[$F(0) \rightarrow ((\forall x)(F(x) \rightarrow F(Sx)) \rightarrow (\forall x)F(x))$]

In other words, except 0, every element in the domain of any model of PA is a successor’. Further, the standard PA axioms ensure that $x$ can only be a successor’ of a unique element in any model of PA.

Since Cantor’s first limit ordinal $\omega$ is not the successor’ of any ordinal in the sense required by the PA axioms, and since there are no infinitely descending sequences of ordinals (cf. Me64, p.261) in a model—if any—of a first order set theory such as ZF, the theorem follows. $\Box$

$\S 4.2$ Why we cannot force PA to admit a transfinite ordinal

Theorem 1 reflects the fact that we can define the usual order relation $<$' in PA so that every instance of the PA Axiom Schema of Finite Induction, such as, say:

(i) [$F(0) \rightarrow ((\forall x)(F(x) \rightarrow F(Sx)) \rightarrow (\forall x)F(x))$]

yields the weaker PA theorem:

(ii) [$F(0) \rightarrow ((\forall x) ((\forall y)(y < x \rightarrow F(y)) \rightarrow F(x)) \rightarrow (\forall x)F(x))$]

Now, if we interpret PA without relativisation in ZF [23]— i.e., numerals as finite ordinals, [$Sx$] as [$x \cup \left \{ x \right \}$], etc.— then (ii) always translates in ZF as a theorem:

(iii) [$F(0) \rightarrow ((\forall x)((\forall y)(y \in x \rightarrow F(y)) \rightarrow F(x)) \rightarrow (\forall x)F(x))$]

However, (i) does not always translate similarly as a ZF-theorem, since the following is not necessarily provable in ZF:

(iv) [$F(0) \rightarrow ((\forall x)(F(x) \rightarrow F(x \cup \left \{x\right \})) \rightarrow (\forall x)F(x))$]

Example: Define [$F(x)$] as [$x \in \omega$]’.

We conclude that, whereas the language of ZF admits as a constant the first limit ordinal $\omega$ which would interpret in any putative model of ZF as the (completed’ infinite) set $\omega$ of all finite ordinals:

Corollary 1: The language of PA admits of no constant that interprets in any model of PA as the set $N$ of all natural numbers.

We note that it is the non-logical Axiom Schema of Finite Induction of PA which does not allow us to introduce—contrary to what is suggested by standard texts [24]—an actual’ (or completed’) infinity disguised as an arbitrary constant (usually denoted by $c$ or $\infty$) into either the language, or a putative model, of PA [25].

$\S 5$ Forcing PA to admit denumerable descending dense sequences

The significance of Theorem 1 is seen in the next two arguments, which attempt to implicitly bypass the Theorem’s constraint by appeal to the Compactness Theorem for forcing a non-standard model onto PA [26].

However, we argue in both cases that applying the Compactness Theorem constructively—even from a classical perspective—does not logically yield a non-standard model for PA with an infinite’ integer as claimed [27].

$\S 5.1$ An argument for a non-standard model of PA

The first is the argument (Ln08, p.7) that we can define a non-standard model of PA with an infinite descending chain of successors, where the only non-successor is the null element $0$:

1. Let $<$$N$ (the set of natural numbers); $=$ (equality); $S$ (the successor function); $+$ (the addition function); $\ast$ (the product function); $0$ (the null element)$>$ be the structure that serves to define a model of PA, say $N$.

2. Let T[$N$] be the set of PA-formulas that are satisfied or true in $N$.

3. The PA-provable formulas form a subset of T[$N$].

4. Let $\Gamma$ be the countable set of all PA-formulas of the form $[c_{n} = Sc_{n+1}]$, where the index $n$ is a natural number.

5. Let T be the union of $\Gamma$ and T[$N$].

6. T[$N$] plus any finite set of members of $\Gamma$ has a model, e.g., $N$ itself, since $N$ is a model of any finite descending chain of successors.

7. Consequently, by Compactness, T has a model; call it $M$.

8. $M$ has an infinite descending sequence with respect to $S$ because it is a model of $\Gamma$.

9. Since PA is a subset of T, $M$ is a non-standard model of PA.

$\S 5.2$ Why the argument in $\S 5.1$ is logically fragile

However if—as claimed in $\S 5.1(6)$ above—$N$ is a model of T[$N$] plus any finite set of members of $\Gamma$, and the PA term $[c_{n}]$ is well-defined for any given natural number $n$, then:

$\bullet$ All PA-formulas of the form $[c_{n} = Sc_{n+1}]$ are PA-provable,

$\bullet$ $\Gamma$ is a proper sub-set of the PA-provable formulas, and

$\bullet$ T is identically T[$N$].

Reason: The argument cannot be that some PA-formula of the form $[c_{n} = Sc_{n+1}]$ is true in $N$, but not PA-provable, as this would imply that if PA is consistent then PA+$[\neg (c_{n} = Sc_{n+1})]$ has a model other than $N$; in other words, it would presume that which is sought to be proved, namely that PA has a non-standard model [28]!

Consequently, the postulated model $M$ of T in $\S 5.1(7)$ by Compactness’ is the model $N$ that defines T[$N$]. However, $N$ has no infinite descending sequence with respect to $S$, even though it is a model of $\Gamma$.

Hence the argument does not establish the existence of a non-standard model of PA with an infinite descending sequence with respect to the successor function $S$.

$\S 5.3$ A formal argument for a non-standard model of PA

The second is the more formal argument [29]:

“Let $Th(\mathbb{N})$ denote the complete $\mathcal{L}_{A}$-theory of the standard model, i.e. $Th(\mathbb{N})$ is the collection of all true $\mathcal{L}_{A}$-sentences. For each $n \in \mathbb{N}$ we let $\underline{n}$ be the closed term $(\ldots(((1+1)+1)+ \ldots +1))) (n\ 1s)$ of $\mathcal{L}_{A}$; $\underline{0}$ is just the constant symbol $0$. We now expand our language $\mathcal{L}_{A}$ by adding to it a new constant symbol $c$, obtaining the new language $\mathcal{L}_{c}$, and consider the following $\mathcal{L}_{c}$-theory with axioms

$\rho$ (for each $\rho \in Th(\mathbb{N})$)

and

$c>\underline{n}$ (for each $n \in \mathbb{N}$)

This theory is consistent, for each finite fragment of it is contained in

$T_{k} = Th(\mathbb{N}) \cup \{c > \underline{n}\ |\ n < k\}$

for some $k \in \mathbb{N}$, and clearly the $\mathcal{L}_{c}$-structure $(\mathbb{N},\ k)$ with domain $\mathbb{N},\ 0,\ 1,\ +,\ \cdot$ and $<$ interpreted naturally, and $c$ interpreted by the integer $k$, satisfies $T_{k}$. Thus by the compactness theore $\cup_{k \in \mathbb{N}}T_{k}$ is consistent and has a model $M_{c}$. The first thing to note about $M_{c}$ is that

$M_{c} \models c>\underline{n}$

for all $n \in \mathbb{N}$, and hence it contains an infinite’ integer.”

$\S 5.4$ Why the argument in $\S 5.3$ too is logically fragile

We note again that, from an arithmetical perspective, any application of the Compactness Theorem to PA cannot ignore currently accepted computationalist doctrines of objectivity (cf. Mu91) and contradict the constructive assignment of satisfaction and truth to the atomic formulas of PA (therefore to the compound formulas under Tarski’s inductive definitions) in terms of either algorithmical verifiability or algorithmic computability (An12, $\S 3$).

Accordingly, from an arithmetical perspective we can only conclude by the Compactness Theorem that if $Th(\mathbb{N})$ is the $\mathcal{L}_{A}$-theory of the standard model (interpretation), then we may consistently add to it the following as an additional—not necessarily independent—axiom:

$(\exists y)(y > x)$.

Moreover, even though $(\exists y)(y > x)$ is algorithmically computable as always true in the standard model—whence all instances of it are also therefore in $Th(\mathbb{N})$—we cannot conclude by the Compactness Theorem that $\cup_{k \in \mathbb{N}}T_{k}$ is consistent and has a model $M_{c}$ which contains an infinite’ integer.

Reason: The condition $k \in \mathbb{N}$‘ in $\cup_{k \in \mathbb{N}}T_{k}$ requires, first of all, that we must be able to extend $Th(\mathbb{N})$ by the addition of a relativised’ axiom (cf. Fe92; Me64, p.192) such as:

$(\exists y)((x \in \mathbb{N}) \rightarrow (y > x))$,

from which we may conclude the existence of some $c$ such that:

$M_{c} \models c>\underline{n}$

for all $n \in \mathbb{N}$.

However, even this would not yield a model for $Th(\mathbb{N})$ since, by Theorem 1, we cannot introduce a completed’ infinity such as $\mathbb{N}$ into any model of $Th(\mathbb{N})$!

As the argument stands, it seeks to violate finitarity by adding a new constant $c$ to the language $\mathcal{L}_{A}$ of PA that is not definable in $\mathcal{L}_{A}$ and, ipso facto, adding an atomic formula $[c=x]$ to PA whose satisfaction under any interpretation of PA is not algorithmically verifiable!

Since the atomic formulas of PA are algorithmically verifiable under the standard interpretation (An12, Corollary 2), the above conclusion too postulates that which it seeks to prove!

Moreover, the postulation would be false if $Th(\mathbb{N})$ were categorical.

Since $Th(\mathbb{N})$ must have a non-standard model if it is not categorical, we consider next whether we may conclude from Gödel’s incompleteness argument (in Go31) that any such model can have an infinite’ integer.

$\S 6$ Gödel’s argument for a non-standard model of PA

We begin by considering the Gödelian formula $[(\forall x)R(x)]$ [30] which is unprovable in PA if PA is consistent, even though the formula $[R(n)]$ is provable in a consistent PA for any given PA numeral $[n]$.

Now, it follows from Gödel’s reasoning [31] that:

Theorem 2: If PA is consistent, then we may add the PA formula $[\neg (\forall x)R(x)]$ as an axiom to PA without inviting inconsistency.

Theorem 3: If PA is $\omega$-consistent, then we may add the PA formula $[(\forall x)R(x)]$ as an axiom to PA without inviting inconsistency.

Gödel concluded from this that:

Corollary 2: If PA is $\omega$-consistent, then there are at least two distinctly different models of PA. $\Box$

If we assume that a consistent PA is necessarily $\omega$-consistent, then it follows that one of the two putative models postulated by Corollary 2 must contain elements other than the natural numbers.

We conclude that Gödel’s justification for the assumption that non-standard models of PA containing elements other than the natural numbers are logically feasible lies in his non-constructive—and logically fragile—assumption that a consistent PA is necessarily $\omega$-consistent.

$\S 6.1$ Why Gödel’s assumption is logically fragile

Now, whereas Gödel’s proof of Corollary 2 appeals to the non-constructive Aristotle’s particularisation, a constructive proof of the Corollary follows trivially from evidence-based interpretations of PA (An12).

Reason: Tarski’s inductive definitions allow us to provide finitary satisfaction and truth certificates to all atomic (and ipso facto to all compound) formulas of PA over the domain $N$ of the natural numbers in two essentially different ways:

(1) In terms of algorithmic verifiabilty (An12, $\S 4.2$); and

(2) In terms of algorithmic computability (An12, $\S 4.3$).

That there can be even one, let alone two, logically sound and finitary assignments of satisfaction and truth certificates to both the atomic and compound formulas of PA was hitherto unsuspected!

Moreover, neither the putative algorithmically verifiable’ model, nor the algorithmically computable’ model, of PA defined by these finitary satisfaction and truth assignments contains elements other than the natural numbers.

(a) Any algorithmically verifiable model of PA is necessarily over $\mathbb{N}$

For instance if, in the first case, we assume that the algorithmically verifiable atomic formulas of PA determine an algorithmically verifiable model of PA over the domain $\mathbb{N}$ of the PA numerals, then such a putative model would be isomorphic to the standard model of PA over the domain $N$ of the natural numbers (An12, $\S 4.2$ & $\S 5$, Corollary 2).

However, such a putative model of PA over $\mathbb{N}$ would not be finitary since, if the formula $[(\forall x) F(x)]$ were to interpret as true in it, then we could only conclude that, for any numeral $[n]$, there is an algorithm which will finitarily certify the formula $[F(n)]$ as true under an algorithmically verifiable interpretation in $\mathbb{N}$.

We could not conclude that there is a single algorithm which, for any numeral $[n]$, will finitarily certify the formula $[F(n)]$ as true under the algorithmically verifiable interpretation in $\mathbb{N}$.

Consequently, the PA Axiom Schema of Finite Induction would not interpret as true finitarily under the algorithmically verifiable interpretation of PA over the domain $\mathbb{N}$ of the PA numerals.

Thus the algorithmically verifiable interpretation of PA would not define a finitary model of PA.

However, if we were to assume that the algorithmically verifiable interpretation of PA defines a non-finitary model of PA, then it would follow that:

$\bullet$ PA is necessarily $\omega$-consistent;

$\bullet$ Aristotle’s particularisation holds over $N$; and

$\bullet$ The standard’ interpretation of PA also defines a non-finitary model of PA over $N$.

(b) The algorithmically computable interpretation of PA is over $\mathbb{N}$

The second case is where the algorithmically computable atomic formulas of PA determine an algorithmically computable model of PA over the domain $N$ of the natural numbers (An12, $\S 4.3$ & $\S 5.2$).

The algorithmically computable model of PA is finitary since we can show that, if the formula $[(\forall x) F(x)]$ interprets as true under it, then we may always conclude that there is a single algorithm which, for any numeral $[n]$, will finitarily certify the formula $[F(n)]$ as true in $N$ under the algorithmically computable interpretation.

Consequently we can show that all the PA axioms—including the Axiom Schema of Finite Induction—interpret finitarily as true in $N$ under the algorithmically computable interpretation of PA, and the PA Rules of Inference preserve such truth finitarily (An12, $\S 5.2$ Theorem 4).

Thus the algorithmically computable interpretation of PA defines a finitary model of PA from which we may conclude that:

$\bullet$ PA is consistent (An12, $\S 5.3$, Theorem 6).

$\S 6.2$ Why we cannot conclude that PA is necessarily $\omega$-consistent

By the way the above finitary interpretation (b) is defined under Tarski’s inductive definitions (An12, $\S 4.3$), if a PA-formula $[F]$ interprets as true in the corresponding finitary model of PA, then there is an algorithm that provides a certificate for such truth for $[F]$ in $N$; whilst if $[F]$ interprets as false in the above finitary model of PA, then there is no algorithm that can provide such a truth certificate for $[F]$ in $N$ (An12, $\S 2$).

Now, if there is no algorithm that can provide such a truth certificate for the Gödelian formula $[R(x)]$ in $N$, then we would have by definition first that the PA formula $[\neg(\forall x)R(x)]$ is true in the model, and second by Gödel’s reasoning that the formula $[R(n)]$ is true in the model for any given numeral $[n]$. Hence Aristotle’s particularisation would not hold in the model.

However, by definition if PA were $\omega$-consistent then Aristotle’s particularisation must necessarily hold in every model of PA.

It follows that unless we can establish that there is some algorithm which can provide such a truth certificate for the Gödelian formula $[R(x)]$ in $N$, we cannot make the unqualified assumption—as Gödel appears to do—that a consistent PA is necessarily $\omega$-consistent.

Conclusion

We have argued that standard arguments for the existence of non-standard models of the first-order Peano Arithmetic PA with domains other than the domain $N$ of the natural numbers should be treated as logically fragile even from within classical logic. In particular we have argued that although Gödel’s argument for the existence of a non-standard model of PA does yield a model of PA other than the classical non-finitary standard’ model, we cannot conclude from it that the domain is other than the domain $N$ of the natural numbers unless we make the non-constructive—and logically fragile—assumption that a consistent PA is necessarily $\omega$-consistent.

References

BBJ03 George S. Boolos, John P. Burgess, Richard C. Jeffrey. 2003. Computability and Logic (4th ed). Cambridge University Press, Cambridge.

Be59 Evert W. Beth. 1959. The Foundations of Mathematics. In Studies in Logic and the Foundations of Mathematics. Edited by L. E. J. Brouwer, E. W. Beth, A. Heyting. 1959. North Holland Publishing Company, Amsterdam.

BF58 Paul Bernays and Abraham A. Fraenkel. 1958. Axiomatic Set Theory In Studies in Logic and the Foundations of Mathematics. Edited by L. E. J. Brouwer, E. W. Beth, A. Heyting. 1959. North Holland Publishing Company, Amsterdam.

Bo00 Andrey I. Bovykin. 2000. On order-types of models of arithmetic. Thesis submitted to the University of Birmingham for the degree of Ph.D. in the Faculty of Science, School of Mathematics and Statistics, The University of Birmingham, Edgbaston, Birmingham, B15 2TT, United Kingdom, 13 April 2000.

Br08 L. E. J. Brouwer. 1908. The Unreliability of the Logical Principles. English translation in A. Heyting, Ed. L. E. J. Brouwer: Collected Works 1: Philosophy and Foundations of Mathematics. Amsterdam: North Holland / New York: American Elsevier (1975): pp.107-111.

Co66 Paul J. Cohen. 1966. Set Theory and the Continuum Hypothesis. (Lecture notes given at Harvard University, Spring 1965) W. A. Benjamin, Inc., New York.

Da82 Martin Davis. 1958. Computability and Unsolvability. 1982 ed. Dover Publications, Inc., New York.

EC89 Richard L. Epstein, Walter A. Carnielli. 1989. Computability: Computable Functions, Logic, and the Foundations of Mathematics. Wadsworth & Brooks, California.

Fe92 Solomon Feferman. 1992. What rests on what: The proof-theoretic analysis of mathematics Invited lecture, 15th International Wittgenstein Symposium: Philosophy of Mathematics, held in Kirchberg/Wechsel, Austria, 16-23 August 1992.

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.

HA28 David Hilbert & Wilhelm Ackermann. 1928. Principles of Mathematical Logic. Translation of the second edition of the Grundzüge Der Theoretischen Logik. 1928. Springer, Berlin. 1950. Chelsea Publishing Company, New York.

Hi25 David Hilbert. 1925. On the Infinite. Text of an address delivered in Münster on 4th June 1925 at a meeting of the Westphalian Mathematical Society. In Jean van Heijenoort. 1967.Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

HP98 Petr Hájek and Pavel Pudlák. 1998. Metamathematics of First-Order Arithmetic. Volume 3 of Perspectives in Mathematical Logic Series, ISSN 0172-6641. Springer-Verlag, Berlin, 1998.

Ka91 Richard Kaye. 1991. Models of Peano Arithmetic. Oxford Logic Guides, 15. Oxford Science Publications. The Clarendon Press, Oxford University Press, New York, 1991.

Ka11 Richard Kaye. 2011. Tennenbaum’s theorem for models of arithmetic. In Set Theory, Arithmetic, and Foundations of Mathematics. Eds. Juliette Kennedy & Roman Kossak. Lecture Notes in Logic (No. 36). pp.66-79. Cambridge University Press, 2011. Cambridge Books Online. http://dx.doi.org/10.1017/CBO9780511910616.005.

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

Kn63 G. T. Kneebone. 1963. Mathematical Logic and the Foundations of Mathematics: An Introductory Survey. D. Van Norstrand Company Limited, London.

Ko06 Roman Kossak and James H. Schmerl. 2006. The structure of models of Peano arithmetic. Oxford Logic Guides, 50. Oxford Science Publications. The Clarendon Press, Oxford University Press, Oxford, 2006.

Li64 A. H. Lightstone. 1964. The Axiomatic Method. Prentice Hall, NJ.

Ln08 Laureano Luna. 2008. On non-standard models of Peano Arithmetic. In The Reasoner, Vol(2)2 p7.

Me64 Elliott Mendelson. 1964. Introduction to Mathematical Logic. Van Norstrand, Princeton.

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.

Nv64 P. S. Novikov. 1964. Elements of Mathematical Logic. Oliver & Boyd, Edinburgh and London.

Qu63 Willard Van Orman Quine. 1963. Set Theory and its Logic. Harvard University Press, Cambridge, Massachusette.

Rg87 Hartley Rogers Jr. 1987. Theory of Recursive Functions and Effective Computability. MIT Press, Cambridge, Massachusetts.

Ro53 J. Barkley Rosser. 1953. Logic for Mathematicians. McGraw Hill, New York.

Sh67 Joseph R. Shoenfield. 1967. Mathematical Logic. Reprinted 2001. A. K. Peters Ltd., Massachusetts.

Sk28 Thoralf A. Skolem. 1928. On Mathematical Logic. Text of a lecture delivered on 22nd October 1928 before the Norwegian Mathematical Association. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931 Harvard University Press, Cambridge, Massachusetts.

Sk34 Thoralf A. Skolem. 1934. \”{U}ber die Nicht-charakterisierbarkeit der Zahlenreihe mittels endlich oder abz\”{a}hlbar unendlich vieler Aussagen mit ausschliesslich Zahlenvariablen. Fundamenta Mathematicae, 23, 150-161. English version: Peano’s axioms and models of arithmetic. In Mathematical interpretations of formal systems. North Holland, Amsterdam, 1955, pp.1-14.

Sm92 Raymond M. Smullyan. 1992. Gödel’s Incompleteness Theorems. Oxford University Press, Inc., New York.

Su60 Patrick Suppes. 1960. Axiomatic Set Theory. Van Norstrand, Princeton.

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.

Wa63 Hao Wang. 1963. A survey of Mathematical Logic. North Holland Publishing Company, Amsterdam.

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 $EPR$ 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 1: By which we mean arguments such as in Ka91 (see pg.1), where the meta-theory is taken to be a set-theory such as ZF or ZFC, and the logical consistency of the meta-theory is not considered relevant to the argumentation.

Return to 2: For purposes of this investigation we may take this to be a first order theory such as the theory S defined in Me64, pp.102-103.

Return to 5: Some of the—hitherto unsuspected—consequences of this doctrine are detailed in An12.

Return to 6: An12, Corollary 2; non-finitary’ because the Axiom Schema of Finite Induction cannot 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 8: cf. The standard non-constructive set-theoretical assignment-by-postulation (S5) of the satisfaction properties (S1) to (S8) in BBJ03, p.153, Lemma 13.1 (Satisfaction properties lemma), which appeals critically to Aristotle’s particularisation.

Return to 9: For purposes of this investigation we may take this to be an interpretation of PA as defined in Me64, p.107.

Return to 10: In his seminal 1931 paper Go31, Kurt Gödel defines, and refers to, the formula corresponding to $[R(x)]$ only by its Gödel’ number $r$ (op. cit., p.25, Eqn.(12)), and to the formula corresponding to $[(\forall x)R(x)]$ only by its Gödel’ number $17\ Gen\ r$.

Return to 11: By classical logic’ we mean the standard first-order predicate calculus FOL where we neither deny the Law of the Excludeds Middle, nor assume that the FOL is $\omega$-consistent (i.e., we do not assume that Aristotle’s particularisation must hold under any interpretation of the logic).

Return to 12: Notation: For the sake of convenience, we shall use square brackets to indicate that the expression enclosed by them is to be treated as denoting a formula of a formal theory, and not as denoting an interpretation.

Return to 13: However, as noted earlier, the Axiom Schema of Finite Induction cannot 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 14: In this case however, 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 (An12, Theorem 4).

Return to 15: The far reaching—hitherto unsuspected—consequences of this distinction for PA are detailed in An12.

Return to 16: We note that algorithmic computability implies the existence of an 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 an algorithm that can decide the truth/falsity of each proposition in a well-defined denumerable sequence of propositions. 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 17: See Hi25, p.382; HA28, p.48; Sk28, p.515; Go31, p.32.; Kl52, p.169; Ro53, p.90; BF58, p.46; Be59, pp.178 & 218; Su60, p.3; Wa63, p.314-315; Qu63, pp.12-13; Kn63, p.60; Co66, p.4; Me64, pp.45, 47, 52(ii), 214(fn); Nv64, p.92; Li64, p.33; Sh67, p.13; Da82, p.xxv; Rg87, p.xvii; EC89, p.174; Mu91; Sm92, p.18, Ex.3; BBJ03, p.102.

Return to 18: The significance of $\omega$-consistency for the formal system PA is highlighted inAn12.

Return to 21: cf. HP98, p.13, $\S 0.29$; Me64, p.112, Ex. 2.

Return to 22: For purposes of this investigation we may take this to be the first order predicate calculus $K$ as defined in Me64, p.57.

Return to 24: eg. HP98, p.13, $\S 0.29$; Ka91, p.11 & p.12, fig.1; BBJ03. p.306, Corollary 25.3; Me64, p.112, Ex. 2.

Return to 25: A possible reason why the Axiom Schema of Finite Induction does not admit non-finitary reasoning into either PA, or into any model of PA, is suggested in $\S 6.1$ below.

Return to 26: eg. Ln08, p.7; Ka91, pp.10-11, p.74 & p.75, Theorem 6.4.

Return to 27: And as suggested also by standard texts in such cases; eg. BBJ03. p.306, Corollary 25.3; Me64, p.112, Ex. 2.

Return to 28: To place this distinction in perspective, Adrien-Marie Legendre and Carl Friedrich Gauss independently conjectured in 1796 that, if $\pi (x)$ denotes the number of primes less than $x$, then $\pi (x)$ is asymptotically equivalent to $x$/In$(x)$. Between 1848/1850, Pafnuty Lvovich Chebyshev confirmed that if $\pi (x)$/($x$/In$(x)$) has a limit, then it must be 1. However, the crucial question of whether $\pi (x)$/($x$/In$(x)$) has a limit at all was answered in the affirmative using analytic methods independently by Jacques Hadamard and Charles Jean de la Vallée Poussin only in 1896, and using only elementary methods by Atle Selberg and Paul Erdös in 1949.

Return to 29: Ka91, pp.10-11; attributed as essentially Skolem’s argument in Sk34.

Return to 30: In his seminal 1931 paper Go31, Kurt Gödel defines, and refers to, the formula corresponding to $[R(x)]$ only by its Gödel’ number $r$ (op. cit., p.25, Eqn.(12)), and to the formula corresponding to $[(\forall x)R(x)]$ only by its Gödel’ number $17\ Gen\ r$.

Author’s working archives & abstracts of investigations

$\S 1$ The Holy Grail of Arithmetic: Bridging Provability and Computability

(Notations, non-standard concepts, and definitions used commonly in these investigations are detailed in this post.)

Peter Wegner and Dina Goldin

In a short opinion paper, Computation Beyond Turing Machines‘, Computer Scientists Peter Wegner and Dina Goldin (Wg03) advanced the thesis that:

A paradigm shift is necessary in our notion of computational problem solving, so it can provide a complete model for the services of today’s computing systems and software agents.’

We note that Wegner and Goldin’s arguments, in support of their thesis, seem to reflect an extraordinarily eclectic view of mathematics, combining both an implicit acceptance of, and implicit frustration at, the standard interpretations and dogmas of classical mathematical theory:

(i) … Turing machines are inappropriate as a universal foundation for computational problem solving, and … computer science is a fundamentally non-mathematical discipline.’

(ii) (Turing’s) 1936 paper … proved that mathematics could not be completely modeled by computers.’

(iii) … the Church-Turing Thesis … equated logic, lambda calculus, Turing machines, and algorithmic computing as equivalent mechanisms of problem solving.’

(iv) Turing implied in his 1936 paper that Turing machines … could not provide a model for all forms of mathematics.’

(v) … Gödel had shown in 1931 that logic cannot model mathematics … and Turing showed that neither logic nor algorithms can completely model computing and human thought.’

These remarks vividly illustrate the dilemma with which not only Theoretical Computer Sciences, but all applied sciences that depend on mathematics—for providing a verifiable language to express their observations precisely—are faced:

Query: Are formal classical theories essentially unable to adequately express the extent and range of human cognition, or does the problem lie in the way formal theories are classically interpreted at the moment?

The former addresses the question of whether there are absolute limits on our capacity to express human cognition unambiguously; the latter, whether there are only temporal limits—not necessarily absolute—to the capacity of classical interpretations to communicate unambiguously that which we intended to capture within our formal expression.

Prima facie, applied science continues, perforce, to interpret mathematical concepts Platonically, whilst waiting for mathematics to provide suitable, and hopefully reliable, answers as to how best it may faithfully express its observations verifiably.

Lance Fortnow

This dilemma is also reflected in Computer Scientist Lance Fortnow’s on-line rebuttal of Wegner and Goldin’s thesis, and of their reasoning.

Thus Fortnow divides his faith between the standard interpretations of classical mathematics (and, possibly, the standard set-theoretical models of formal systems such as standard Peano Arithmetic), and the classical computational theory of Turing machines.

He relies on the former to provide all the proofs that matter:

Not every mathematical statement has a logical proof, but logic does capture everything we can prove in mathematics, which is really what matters’;

and, on the latter to take care of all essential, non-provable, truth:

… what we can compute is what computer science is all about’.

Can faith alone suffice?

However, as we shall argue in a subsequent post, Fortnow’s faith in a classical Church-Turing Thesis that ensures:

… Turing machines capture everything we can compute’,

may be as misplaced as his faith in the infallibility of standard interpretations of classical mathematics.

The reason: There are, prima facie, reasonably strong arguments for a Kuhnian (Ku62) paradigm shift; not, as Wegner and Goldin believe, in the notion of computational problem solving, but in the standard interpretations of classical mathematical concepts.

However, Wegner and Goldin could be right in arguing that the direction of such a shift must be towards the incorporation of non-algorithmic effective methods into classical mathematical theory (as detailed in the Birmingham paper); presuming, from the following remarks, that this is, indeed, what external interactions’ are assumed to provide beyond classical Turing-computability:

(vi) … that Turing machine models could completely describe all forms of computation … contradicted Turing’s assertion that Turing machines could only formalize algorithmic problem solving … and became a dogmatic principle of the theory of computation’.

(vii) … interaction between the program and the world (environment) that takes place during the computation plays a key role that cannot be replaced by any set of inputs determined prior to the computation’.

(viii) … a theory of concurrency and interaction requires a new conceptual framework, not just a refinement of what we find natural for sequential [algorithmic] computing’.

(ix) … the assumption that all of computation can be algorithmically specified is still widely accepted’.

A widespread notion of particular interest, which seems to be recurrently implicit in Wegner and Goldin’s assertions too, is that mathematics is a dispensable tool of science, rather than its indispensable mother tongue.

Elliott Mendelson

However, the roots of such beliefs may also lie in ambiguities, in the classical definitions of foundational elements, that allow the introduction of non-constructive—hence non-verifiable, non-computational, ambiguous, and essentially Platonic—elements into the standard interpretations of classical mathematics.

For instance, in a 1990 philosophical reflection, Elliott Mendelson’s following remarks (in Me90; reproduced from Selmer Bringsjord (Br93)), implicitly imply that classical definitions of various foundational elements can be argued as being either ambiguous, or non-constructive, or both:

Here is the main conclusion I wish to draw: it is completely unwarranted to say that CT is unprovable just because it states an equivalence between a vague, imprecise notion (effectively computable function) and a precise mathematical notion (partial-recursive function). … The concepts and assumptions that support the notion of partial-recursive function are, in an essential way, no less vague and imprecise than the notion of effectively computable function; the former are just more familiar and are part of a respectable theory with connections to other parts of logic and mathematics. (The notion of effectively computable function could have been incorporated into an axiomatic presentation of classical mathematics, but the acceptance of CT made this unnecessary.) … Functions are defined in terms of sets, but the concept of set is no clearer than that of function and a foundation of mathematics can be based on a theory using function as primitive notion instead of set. Tarski’s definition of truth is formulated in set-theoretic terms, but the notion of set is no clearer than that of truth. The model-theoretic definition of logical validity is based ultimately on set theory, the foundations of which are no clearer than our intuitive understanding of logical validity. … The notion of Turing-computable function is no clearer than, nor more mathematically useful (foundationally speaking) than, the notion of an effectively computable function.’

Consequently, standard interpretations of classical theory may, inadvertently, be weakening a desirable perception—of mathematics as the lingua franca of scientific expression—by ignoring the possibility that, since mathematics is, indeed, indisputably accepted as the language that most effectively expresses and communicates intuitive truth, the chasm between formal truth and provability must, of necessity, be bridgeable.

Cristian Calude, Elena Calude and Solomon Marcus

The belief in the existence of such a bridge is occasionally implicit in interpretations of computational theory.

For instance, in an arXived paper Passages of Proof, Computer Scientists Cristian Calude, Elena Calude and Solomon Marcus remark that:

“Classically, there are two equivalent ways to look at the mathematical notion of proof: logical, as a finite sequence of sentences strictly obeying some axioms and inference rules, and computational, as a specific type of computation. Indeed, from a proof given as a sequence of sentences one can easily construct a Turing machine producing that sequence as the result of some finite computation and, conversely, given a machine computing a proof we can just print all sentences produced during the computation and arrange them into a sequence.”

In other words, the authors seem to hold that Turing-computability of a proof’, in the case of an arithmetical proposition, is equivalent to provability of its representation in PA.

Wilfrid Sieg

We now attempt to build such a bridge formally, which is essentially one between the arithmetical ‘Decidability and Calculability’ described by Philosopher Wilfrid Sieg in his in-depth and wide-ranging survey ‘On Comptability‘, in which he addresses Gödel’s lifelong belief that an iff bridge between the two concepts is ‘impossible’ for ‘the whole calculus of predicates’ (Wi08, p.602).

$\S 2$ Bridging provability and computability: The foundations

In the paper titled “Evidence-Based Interpretations of $PA$” that was presented to the Symposium on Computational Philosophy at the AISB/IACAP World Congress 2012-Alan Turing 2012, held from $2^{nd}$ to $6^{th}$ July 2012 at the University of Birmingham, UK (reproduced in this post) we have defined what it means for a number-theoretic function to be:

We have shown there that:

(i) The standard interpretation $\mathcal{I}_{PA(N,\ Standard)}$ of the first order Peano Arithmetic PA is finitarily sound if, and only if, Aristotle’s particularisation holds over $N$; and the latter is the case if, and only if, PA is $\omega$-consistent.

(ii) We can define a finitarily sound algorithmic interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ of PA over the domain $N$ where, if $[A]$ is an atomic formula $[A(x_{1}, x_{2}, \ldots, x_{n})]$ of PA, then the sequence of natural numbers $(a_{1}, a_{2}, \ldots, a_{n})$ satisfies $[A]$ if, and only if $[A(a_{1}, a_{2}, \ldots, a_{n})]$ is algorithmically computable under $\mathcal{I}_{PA(N,\ Algorithmic)}$, but we do not presume that Aristotle’s particularisation is valid over $N$.

(iii) The axioms of PA are always true under the finitary interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$, and the rules of inference of PA preserve the properties of satisfaction/truth under $\mathcal{I}_{PA(N,\ Algorithmic)}$.

We concluded that:

Theorem 1: The interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ of PA is finitarily sound.

Theorem 2: PA is consistent.

$\S 3$ Extending Buss’ Bounded Arithmetic

One of the more significant consequences of the Birmingham paper is that we can extend the iff bridge between the domain of provability and that of computability envisaged under Buss’ Bounded Arithmetic by showing that an arithmetical formula $[F]$ is PA-provable if, and only if, $[F]$ interprets as true under an algorithmic interpretation of PA.

$\S 4$ A Provability Theorem for PA

We first show that PA can have no non-standard model (for a distinctly different proof of this convention-challenging thesis see this post and this paper), since it is algorithmically’ complete in the sense that:

Theorem 3: (Provability Theorem for PA) A PA formula $[F(x)]$ is PA-provable if, and only if, $[F(x)]$ is algorithmically computable as always true in $N$.

Proof: We have by definition that $[(\forall x)F(x)]$ interprets as true under the interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ if, and only if, $[F(x)]$ is algorithmically computable as always true in $N$.

Since $\mathcal{I}_{PA(N,\ Algorithmic)}$ is finitarily sound, it defines a finitary model of PA over $N$—say $\mathcal{M}_{PA(\beta)}$—such that:

If $[(\forall x)F(x)]$ is PA-provable, then $[F(x)]$ is algorithmically computable as always true in $N$;

If $[\neg(\forall x)F(x)]$ is PA-provable, then it is not the case that $[F(x)]$ is algorithmically computable as always true in $N$.

Now, we cannot have that both $[(\forall x)F(x)]$ and $[\neg(\forall x)F(x)]$ are PA-unprovable for some PA formula $[F(x)]$, as this would yield the contradiction:

(i) There is a finitary model—say $M1_{\beta}$—of PA+$[(\forall x)F(x)]$ in which $[F(x)]$ is algorithmically computable as always true in $N$.

(ii) There is a finitary model—say $M2_{\beta}$—of PA+$[\neg(\forall x)F(x)]$ in which it is not the case that $[F(x)]$ is algorithmically computable as always true in $N.$

The lemma follows. $\Box$

$\S 5$ The holy grail of arithmetic

We thus have that:

Corollary 1: PA is categorical finitarily.

Now we note that:

Lemma 2: If PA has a sound interpretation $\mathcal{I}_{PA(N,\ Sound)}$ over $N$, then there is a PA formula $[F]$ which is algorithmically verifiable as always true over $N$ under $\mathcal{I}_{PA(N,\ Sound)}$ even though $[F]$ is not PA-provable.

Proof In his seminal 1931 paper on formally undecidable arithmetical propositions, Kurt Gödel has shown how to construct an arithmetical formula with a single variable—say $[R(x)]$ [1]—such that $[R(x)]$ is not PA-provable [2], but $[R(n)]$ is instantiationally PA-provable for any given PA numeral $[n]$. Hence, for any given numeral $[n]$, the PA formula $xB \lceil [R(n)] \rceil$ must hold for some $x$. The lemma follows. $\Box$

By the argument in Theorem 3 it follows that:

Corollary 2: The PA formula $[\neg(\forall x)R(x)]$ defined in Lemma 2 is PA-provable.

Corollary 3: Under any sound interpretation of PA, Gödel’s $[R(x)]$ interprets as an algorithmically verifiable, but not algorithmically computable, tautology over $N$.

Proof Gödel has shown that $[R(x)]$ [3] interprets as an algorithmically verifiable tautology [4]. By Corollary 2 $[R(x)]$ is not algorithmically computable as always true in $N$. $\Box$

Corollary 4: PA is not $\omega$-consistent. [5]

Proof Gödel has shown that if PA is consistent, then $[R(n)]$ is PA-provable for any given PA numeral $[n]$ [6]. By Corollary 2 and the definition of $\omega$-consistency, if PA is consistent then it is not $\omega$-consistent. $\Box$

Corollary 5: The standard interpretation $\mathcal{I}_{PA(N,\ Standard)}$ of PA is not finitarily sound, and does not yield a finitary model of PA [7].

Proof If PA is consistent but not $\omega$-consistent, then Aristotle’s particularisation does not hold over $N$. Since the standard’, interpretation of PA appeals to Aristotle’s particularisation, the lemma follows. $\Box$

Since formal quantification is currently interpreted in classical logic [8] so as to admit Aristotle’s particularisation over $N$ as axiomatic [9], the above suggests that we may need to review number-theoretic arguments [10] that appeal unrestrictedly to classical Aristotlean logic.

$\S 6$ The Provability Theorem for PA and Bounded Arithmetic

In a 1997 paper [11], Samuel R. Buss considered Bounded Arithmetics obtained by:

(a) limiting the applicability of the Induction Axiom Schema in PA only to functions with quantifiers bounded by an unspecified natural number bound $b$;

(b) weakening’ the statement of the axiom with the aim of differentiating between effective computability over the sequence of natural numbers, and feasible polynomial-time’ computability over a bounded sequence of the natural numbers [12].

Presumably Buss’ intent—as expressed below—is to build an iff bridge between provability in a Bounded Arithmetic and Computability so that a $\Pi_{k}$ formula, say $[(\forall x)f(x)]$, is provable in the Bounded Arithmetic if, and only if, there is an algorithm that, for any given numeral $[n]$, decides the $\Delta_{(k/(k-1))}$ formula $[f(n)]$ as true’:

If $[(\forall x)(\exists y)f(x, y)]$ is provable, then there should be an algorithm to find $y$ as a function of $x$ [13].

Since we have proven such a Provability Theorem for PA in the previous section, the first question arises:

$\S 7$ Does the introduction of bounded quantifiers yield any computational advantage?

Now, one difference [14] between a Bounded Arithmetic and PA is that we can presume in the Bounded Arithmetic that, from a proof of $[(\exists y)f(n, y)]$, we may always conclude that there is some numeral $[m]$ such that $[f(n, m)]$ is provable in the arithmetic; however, this is not a finitarily sound conclusion in PA.

Reason: Since $[(\exists y)f(n, y)]$ is simply a shorthand for $[\neg (\forall y)\neg f(n, y)]$, such a presumption implies that Aristotle’s particularisation holds over the natural numbers under any finitarily sound interpretation of PA.

To see that (as Brouwer steadfastly held) this may not always be the case, interpret $[(\forall x)f(x)]$ as [15]:

There is an algorithm that decides $[f(n)]$ as true’ for any given numeral $[n]$.

In such case, if $[(\forall x)(\exists y)f(x, y)]$ is provable in PA, then we can only conclude that:

There is an algorithm that, for any given numeral $[n]$, decides that it is not the case that there is an algorithm that, for any given numeral $[m]$, decides $[\neg f(n, m)]$ as true’.

We cannot, however, conclude—as we can in a Bounded Arithmetic—that:

There is an algorithm that, for any given numeral $[n]$, decides that there is an algorithm that, for some numeral $[m]$, decides $[f(n, m)]$ as true’.

Reason: $[(\exists y)f(n, y)]$ may be a Halting-type formula for some numeral $[n]$.

This could be the case if $[(\forall x)(\exists y)f(x, y)]$ were PA-unprovable, but $[(\exists y)f(n, y)]$ PA-provable for any given numeral $[n]$.

Presumably it is the belief that any finitarily sound interpretation of PA requires Aristotle’s particularisation to hold in $N$, and the recognition that the latter does not admit linking provability to computability in PA, which has led to considering the effect of bounding quantification in PA.

However, as we have seen in the preceding sections, we are able to link provability to computability through the Provability Theorem for PA by recognising precisely that, to the contrary, any interpretation of PA which requires Aristotle’s particularisation to hold in $N$ cannot be finitarily sound!

The postulation of an unspecified bound in a Bounded Arithmetic in order to arrive at a provability-computability link thus appears dispensible.

The question then arises:

$\S 8$ Does weakening’ the PA Induction Axiom Schema yield any computational advantage?

Now, Buss considers a bounded arithmetic $S_{2}$ which is, essentially, PA with the following weakened’ Induction Axiom Schema, PIND [16]:

$[\{f(0)\ \&\ (\forall x)(f(\lfloor \frac{x}{2} \rfloor) \rightarrow f(x))\} \rightarrow (\forall x)f(x)]$

However, PIND can be expressed in first-order Peano Arithmetic PA as follows:

$[\{f(0)\ \&\ (\forall x)(f(x) \rightarrow (f(2*x)\ \&\ f(2*x+1)))\} \rightarrow (\forall x)f(x)]$.

Moreover, the above is a particular case of PIND($k$):

$[\{f(0)\ \&\ (\forall x)(f(x) \rightarrow (f(k*x)\ \&\ f(k*x+1)\ \&\ \ldots\ \&\ f(k*x+k-1)))\}$ $\rightarrow (\forall x)f(x)]$.

Now we have the PA theorem:

$[(\forall x)f(x) \rightarrow \{f(0)\ \&\ (\forall x)(f(x) \rightarrow f(x+1))\}]$

It follows that the following is also a PA theorem:

$[\{f(0)\ \&\ (\forall x)(f(x) \rightarrow f(x+1))\} \rightarrow$ $\{f(0)\ \&\ (\forall x)(f(x) \rightarrow (f(k*x)\ \&\ f(k*x+1)\ \&\ \ldots\ \&\ f(k*x+k-1)))\}]$

In other words, for any numeral $[k]$, PIND($k$) is equivalent in PA to the standard Induction Axiom of PA!

Thus, the Provability Theorem for PA suggests that all arguments and conclusions of a Bounded Arithmetic can be reflected in PA without any loss of generality.

References

Br93 Selmer Bringsjord 1993. The Narrational Case Against Church’s Thesis. Easter APA meetings, Atlanta.

Br08 L. E. J. Brouwer. 1908. The Unreliability of the Logical Principles. English translation in A. Heyting, Ed. L. E. J. Brouwer: Collected Works 1: Philosophy and Foundations of Mathematics. Amsterdam: North Holland / New York: American Elsevier (1975): pp.107-111.

Bu97 Samuel R. Buss. 1997. Bounded Arithmetic and Propositional Proof Complexity. In Logic of Computation. pp.67-122. Ed. H. Schwichtenberg. Springer-Verlag, Berlin.

CCS01 Cristian S. Calude, Elena Calude and Solomon Marcus. 2001. Passages of Proof. Workshop, Annual Conference of the Australasian Association of Philosophy (New Zealand Division), Auckland. Archived at: http://arxiv.org/pdf/math/0305213.pdf. Also in EATCS Bulletin, Number 84, October 2004, viii+258 pp.

Da82 Martin Davis. 1958. Computability and Unsolvability. 1982 ed. Dover Publications, Inc., New York.

EC89 Richard L. Epstein, Walter A. Carnielli. 1989. Computability: Computable Functions, Logic, and the Foundations of Mathematics. Wadsworth & Brooks, California.

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.

HA28 David Hilbert & Wilhelm Ackermann. 1928. Principles of Mathematical Logic. Translation of the second edition of the Grundzüge Der Theoretischen Logik. 1928. Springer, Berlin. 1950. Chelsea Publishing Company, New York.

He04 Catherine Christer-Hennix. 2004. Some remarks on Finitistic Model Theory, Ultra-Intuitionism and the main problem of the Foundation of Mathematics. ILLC Seminar, 2nd April 2004, Amsterdam.

Hi25 David Hilbert. 1925. On the Infinite. Text of an address delivered in Münster on 4th June 1925 at a meeting of the Westphalian Mathematical Society. In Jean van Heijenoort. 1967.Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

Ku62 Thomas S. Kuhn. 1962. The structure of Scientific Revolutions. 2nd Ed. 1970. University of Chicago Press, Chicago.

Me90 Elliott Mendelson. 1990. Second Thoughts About Church’s Thesis and Mathematical Proofs. In Journal of Philosophy 87.5.

Pa71 Rohit Parikh. 1971. Existence and Feasibility in Arithmetic. In The Journal of Symbolic Logic,>i> Vol.36, No. 3 (Sep., 1971), pp. 494-508.

Rg87 Hartley Rogers Jr. 1987. Theory of Recursive Functions and Effective Computability. MIT Press, Cambridge, Massachusetts.

Ro36 J. Barkley Rosser. 1936. Extensions of some Theorems of Gödel and Church. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York. Reprinted from The Journal of Symbolic Logic. Vol.1. pp.87-91.

Si08 Wilfrid Sieg. 2008. On Computability in Handbook of the Philosophy of Science. Philosophy of Mathematics. pp.525-621. Volume Editor: Andrew Irvine. General Editors: Dov M. Gabbay, Paul Thagard and John Woods. Elsevier BV. 2008.

WG03 Peter Wegner and Dina Goldin. 2003. Computation Beyond Turing Machines. Communications of the ACM, 46 (4) 2003.

Notes

Return to 1: Gödel refers to this formula only by its Gödel number $r$ (Go31, p.25(12)).

Return to 2: Gödel’s immediate aim in Go31 was to show that $[(\forall x)R(x)]$ is not P-provable; by Generalisation it follows, however, that $[R(x)]$ is also not P-provable.

Return to 3: Gödel refers to this formula only by its Gödel number $r$ (Go31, p.25, eqn.12).

Return to 4: Go31, p.26(2): “$(n)\neg(nB_{\kappa}(17Gen\ r))$ holds”.

Return to 5: This conclusion is contrary to accepted dogma. See, for instance, Davis’ remarks in Da82, p.129(iii) that:

“… there is no equivocation. Either an adequate arithmetical logic is $\omega$-inconsistent (in which case it is possible to prove false statements within it) or it has an unsolvable decision problem and is subject to the limitations of Gödel’s incompleteness theorem”.

Return to 7: I note that finitists of all hues—ranging from Brouwer Br08 to Alexander Yessenin-Volpin He04—have persistently questioned the finitary soundness of the standard’ interpretation $\mathcal{I}_{PA(N,\ Standard)}$.

Return to 8: See Hi25, p.382; HA28, p.48; Be59, pp.178 \& 218.

Return to 9: In the sense of being intuitively obvious. See, for instance, Da82, p.xxiv; Rg87, p.308 (1)-(4); EC89, p.174 (4); BBJ03, p.102.

Return to 10: For instance Rosser’s construction of an undecidable arithmetical proposition in PA (see Ro36)—which does not explicitly assume that PA is $\omega$-consistent—implicitly presumes that Aristotle’s particularisation holds over $N$.

Return to 15: We have seen in the earlier sections that such an interpretation is finitarily sound.

Return to 16: Where $\lfloor \frac{x}{2} \rfloor$ denotes the largest natural number lower bound of the rational $\frac{x}{2}$.

Author’s working archives & abstracts of investigations

Evidence-Based Interpretations of PA

In July 2012 I presented a paper titled “Evidence-Based Interpretations of $PA$” to the Symposium on Computational Philosophy at the AISB/IACAP World Congress 2012-Alan Turing 2012, held from $2^{nd}$ to $6^{th}$ July 2012 at the University of Birmingham, UK.

The title was accurate pedantically, but deliberately misleading!

Misleading‘ because—had I kept the interest of the audience paramount—the more appropriate title should have been the provocative claim:

‘A solution to the Second of Hilbert’s Twenty Three Problems‘.

Deliberately‘ because whether or not the argumentation of the paper did lead to a finitary proof of consistency for $PA$ seemed, by itself, of little mathematical interest or consequence.

Reason: Because what did seem mathematically significant, however, was a distinction upon which the argumentation rested—between the use of algorithmic computability and algorithmic verifiabilty for logical validity—which had hitherto remained implicit.

Why the deception? Well, partly because caution was understandably advised, but to a larger extent because we know that either $PA$ has a sound interpretation, or it is inconsistent.

Now if—following David Hilbert’s line of reasoning in the Second of his celebrated Twenty Three problems—we embrace the former (since the latter seems u-u-u-un-un-un-unthinkable‘), then we must believe either that assignment of unique truth values to the $PA$ formulas under any sound interpretation of $PA$ is essentially human-intelligence subjective (eerily akin to a human revelation), or that there must be an objective such assignment that does not depend upon some unique way in which a human intelligence perceives and reasons.

The point of the conference paper was to highlight that the standard interpretation $\mathcal{I}_{PA(N,\ Standard)}$ of $PA$ does not address this issue, since it is silent on the methodology for such an assignment.

$\mathcal{I}_{PA(N,\ Standard)}$ essentially asserts that, under Tarski’s inductive definitions of the satisfaction and truth of the formulas of $PA$ under the interpretation, if there is a methodology for uniquely defining the satisfaction and truth of the atomic formulas of $PA$ (presumably in a way that can be taken to mirror our—i.e. humankind’s—intuitive notion of the truth of the corresponding arithmetical propositions), then the satisfaction and truth of the compound PA formulas are defined uniquely under the interpretation by induction (and may also be taken to mirror our intuitive notion of the truth of the corresponding arithmetical propositions).

The consequences of not specifying a methodology are actually best illustrated by this example (in the borrowed terminology of a correspondent):

Let $E(A)$ mean that there is an assignment which provides objective evidence (o.e.) for $A$. It seems $\mathcal{I}_{PA(N,\ Standard)}$ breaks down in the general treatment of conditionals $A \rightarrow B$. In order to have $E(A \rightarrow B)$, we need to have an assignment which, first of all decides whether $E(A)$ and, if it verifies that, then verifies $E(B)$. But to decide whether $E(A)$ we have to decide whether or not there is an assignment that provides o.e. for $A$, and that can’t be done in general under $\mathcal{I}_{PA(N,\ Standard)}$ in the absence of a methodology for assigning objective satisfaction and truth values to the atomic formulas of $PA$.

The aim of the Birmingham paper (reproduced below) was to bridge this gap.

We formally showed there that there are, indeed, two essentially different methods of constructively assigning objective truth values uniquely to the atomic formulas of $PA$.

We then argued that if Tarski’s definitions are further accepted as inductively determining unique satisfaction and truth values for the compound formulas of $PA$, then we arrive at two interpretations of $PA$, say $\mathcal{I}_{PA(\mathbb {N},\ Instantiational)}$ and $\mathcal{I}_{PA(N,\ Algorithmic)}$.

We showed that $\mathcal{I}_{PA(\mathbb {N},\ Instantiational)}$ is sound if, and only if, $\mathcal{I}_{PA(N,\ Standard)}$ is sound; whence the latter, if sound, can indeed be taken to mirror our intuitive notion of the truth of the corresponding arithmetical propositions over the structure of the natural numbers as intended.

However, this interpretation is not finitary since the Axiom Schema of Finite Induction is not justified finitarily under the interpretation.

We further showed that $\mathcal{I}_{PA(\mathbb {N},\ Instantiational)}$ is sound if, and only if, $PA$ is $\omega$-consistent; which illuminates Gödel’s undecidability Theorem (if $PA$ is $\omega$-consistent, it must have a formally undecidable proposition).

We then argued that the other interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ is sound since the Axiom Schema of Finite Induction is justified finitarily under the interpretation.

However, what interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ can be taken to mirror is only the algorithmic decidability of our intuitive notion of the truth of the corresponding arithmetical propositions!

In other words, arithmetical provability can be taken to correspond not to our intuitive notion of arithmetical truth (which is subjective), but to the algorithmic decidability of our intuitive notion of arithmetical truth (which is objective).

Abstract

We shall now show formally that Tarski’s inductive definitions admit evidence-based interpretations of the first-order Peano Arithmetic PA that allow us to define the satisfaction and truth of the quantified formulas of PA constructively over the domain $N$ of the natural numbers in two essentially different ways:

(1) in terms of algorithmic verifiabilty; and

(2) in terms of algorithmic computability.

We shall argue that the algorithmically computable PA-formulas can provide a finitary interpretation of PA over the domain $N$ of the natural numbers from which we may conclude that PA is consistent.

1 Introduction

In this paper we seek to address one of the philosophical challenges associated with accepting arithmetical propositions as true under an interpretation—either axiomatically or on the basis of subjective self-evidence—without any effective methodology for objectively evidencing such acceptance [1].

For instance, conventional wisdom accepts Alfred Tarski’s definitions of the satisfiability and truth of the formulas of a formal language under an interpretation [2] and postulates that, under the standard interpretation $\mathcal{I}_{PA(N,\ Standard)}$ of the first-order Peano Arithmetic PA [3] over the domain $N$ of the natural numbers:

(i) The atomic formulas of PA can be assumed as decidable under $\mathcal{I}_{PA(N,\ Standard)}$;

(ii) The PA axioms can be assumed to interpret as satisfied/true under $\mathcal{I}_{PA(N,\ Standard)}$;

(iii) the PA rules of inference—Generalisation and Modus Ponens—can be assumed to preserve such satisfaction/truth under $\mathcal{I}_{PA(N,\ Standard)}$.

Standard interpretation of PA: The standard interpretation $\mathcal{I}_{PA(N,\ Standard)}$ of PA over the domain $N$ of the natural numbers is the one in which the logical constants have their usual’ interpretations [4] in Aristotle’s logic of predicates (which subsumes Aristotle’s particularisation [5]), and [7]:

(a) the set of non-negative integers is the domain;

(b) the symbol [0] interprets as the integer 0;

(c) the symbol $[']$ interprets as the successor operation (addition of 1);

(d) the symbols $[+]$ and $[\star]$ interpret as ordinary addition and multiplication;

(e) the symbol $[=]$ interprets as the identity relation.

The axioms of first-order Peano Arithmetic (PA)

PA$_{1}$ $[(x_{1} = x_{2}) \rightarrow ((x_{1} = x_{3}) \rightarrow (x_{2} = x_{3}))]$;

PA$_{2}$ $[(x_{1} = x_{2}) \rightarrow (x_{1}^{\prime} = x_{2}^{\prime})]$;

PA$_{3}$ $[0 \neq x_{1}^{\prime}]$;

PA$_{4}$ $[(x_{1}^{\prime} = x_{2}^{\prime}) \rightarrow (x_{1} = x_{2})]$;

PA$_{5}$ $[( x_{1} + 0) = x_{1}]$;

PA$_{6}$ $[(x_{1} + x_{2}^{\prime}) = (x_{1} + x_{2})^{\prime}]$;

PA$_{7}$ $[( x_{1} \star 0) = 0]$;

PA$_{8}$ $[( x_{1} \star x_{2}^{\prime}) = ((x_{1} \star x_{2}) + x_{1})]$;

PA$_{9}$ For any well-formed formula $[F(x)]$ of PA:

$[F(0) \rightarrow (((\forall x)(F(x) \rightarrow F(x^{\prime}))) \rightarrow (\forall x)F(x))]$.

Generalisation in PA: If $[A]$ is PA-provable, then so is $[(\forall x)A]$.

Modus Ponens in PA: If $[A]$ and $[A \rightarrow B]$ are PA-provable, then so is $[B]$.

We shall show that although the seemingly innocent and self-evident assumption in (i) can, indeed, be justified, it conceals an ambiguity whose impact on (ii) and (iii) is far-reaching in significance and needs to be made explicit.

Reason: Tarski’s inductive definitions admit evidence-based interpretations of PA that actually allow us to metamathematically define the satisfaction and truth of the atomic (and, ipso facto, quantified) formulas of PA constructively over $N$ in two essentially different ways as below, only one of which is finitary [7]:

(1) in terms of algorithmic verifiabilty [8];

(2) in terms of algorithmic computability [9].

Case 1: We show in Section 4.2 that the algorithmically verifiable PA-formulas admit an unusual, instantiational’ Tarskian interpretation $\mathcal{I}_{PA(\mathbb {N},\ Instantiational)}$ of PA over the domain $\mathbb {N}$ of the PA numerals; and that this interpretation is sound if, and only if, PA is $\omega$-consistent.

Soundness (formal system): We define a formal system S as sound under a Tarskian interpretation $\mathcal{I}_{S}$ over a domain $D$ if, and only if, every theorem $[T]$ of S translates as $[T]$ is true under $\mathcal{I}_{S}$ in $D$‘.

Soundness (interpretation): We define a Tarskian interpretation $\mathcal{I}_{S}$ of a formal system S as sound over a domain $D$ if, and only if, S is sound under the interpretation $\mathcal{\mathcal{I}_{S}}$ over the domain $D$.

Simple consistency: A formal system S is simply consistent if, and only if, there is no S-formula $[F(x)]$ for which both $[(\forall x)F(x)]$ and $[\neg(\forall x)F(x)]$ are S-provable.

$\omega$-consistency: A formal system S is $\omega$-consistent if, and only if, there is no S-formula $[F(x)]$ for which, first, $[\neg(\forall x)F(x)]$ is S-provable and, second, $[F(a)]$ is S-provable for any given S-term $[a]$.

We further show that this interpretation can be viewed as a formalisation of the standard interpretation $\mathcal{I}_{PA(N,\ Standard)}$ of PA over $N$; in the sense that—under Tarski’s definitions—$\mathcal{I}_{PA(\mathbb {N},\ Instantiational)}$ is sound over $\mathbb {N}$ if, and only if, $\mathcal{I}_{PA(N,\ Standard)}$ is sound over $N$ (as postulated in (ii) and (iii) above).

Although the standard interpretation $\mathcal{I}_{PA(N,\ Standard)}$ is assumed to be sound over $N$ (as expressed by (ii) and (iii) above), it cannot claim to be finitary since it it is not known to lead to a finitary justification of the truth—under Tarski’s definitions—of the Axiom Schema of (finite) Induction of PA in $N$ from which we may conclude—in an intuitionistically unobjectionable manner—that PA is consistent [10].

We note that Gerhard Gentzen’s constructive’ [11] consistency proof for formal number theory [12] is debatably finitary [13], since it involves a Rule of Infinite Induction that appeals to the properties of transfinite ordinals.

Case 2: We show further in Section 4.3 that the algorithmically computable PA-formulas admit an algorithmic’ Tarskian interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ of PA over $N$.

We then argue in Section 5 that $\mathcal{I}_{PA(N,\ Algorithmic)}$ is essentially different from $\mathcal{I}_{PA(\mathbb {N},\ Instantiational)}$ since the PA-axioms—including the Axiom Schema of (finite) Induction—are algorithmically computable as satisfied/true under the standard interpretation of PA over $N$, and the PA rules of inference preserve algorithmically computable satisfiability/truth under the interpretation [14].

We conclude from the above that the interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ is finitary, and hence sound over $N$ [15].

We further conclude from the soundness of the interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ over $N$ that PA is consistent [16].

2 Interpretation of an arithmetical language in terms of the computations of a simple functional language

We begin by noting that we can, in principle, define [17] the classical satisfaction’ and truth’ of the formulas of a first order arithmetical language, such as PA, verifiably under an interpretation using as evidence [18] the computations of a simple functional language.

Such definitions follow straightforwardly for the atomic formulas of the language (i.e., those without the logical constants that correspond to negation’, conjunction’, implication’ and quantification’) from the standard definition of a simple functional language [19].

Moreover, it follows from Alfred Tarski’s seminal 1933 paper on the concept of truth in the languages of the deductive sciences [20] that the satisfaction’ and truth’ of those formulas of a first-order language which contain logical constants can be inductively defined, under an interpretation, in terms of the satisfaction’ and truth’ of the interpretations of only the atomic formulas of the language.

Hence the satisfaction’ and truth’ of those formulas (of an arithmetical language) which contain logical constants can, in principle, also be defined verifiably under an interpretation using as evidence the computations of a simple functional language.

We show in Section 4 that this is indeed the case for PA under its standard interpretation $\mathcal{I}_{PA(N,\ Standard)}$, when this is explicitly defined as in Section 5.

We show, moreover, that we can further define algorithmic truth’ and algorithmic falsehood’ under $\mathcal{I}_{PA(N,\ Standard)}$ such that the PA axioms interpret as always algorithmically true, and the rules of inference preserve algorithmic truth, over the domain $N$ of the natural numbers.

2.1 The definitions of algorithmic truth’ and algorithmic falsehood’ under $\mathcal{I}_{PA(N,\ Standard)}$ are not symmetric with respect to truth’ and falsehood’ under $\mathcal{I}_{PA(N,\ Standard)}$

However, the definitions of algorithmic truth’ and algorithmic falsehood’ under $\mathcal{I}_{PA(N,\ Standard)}$ are not symmetric with respect to classical (verifiable) truth’ and falsehood’ under $\mathcal{I}_{PA(N,\ Standard)}$.

For instance, if a formula $[(\forall x)F(x)]$ of an arithmetic is algorithmically true under an interpretation (such as $\mathcal{I}_{PA(N,\ Standard)}$), then we may conclude that there is an algorithm that, for any given numeral $[a]$, provides evidence that the formula $[F(a)]$ is algorithmically true under the interpretation.

In other words, there is an algorithm that provides evidence that the interpretation $F^{*}(a)$ of $[F(a)]$ holds in $N$ for any given natural number $a$.

Notation: We use enclosing square brackets as in $[F(x)]$‘ to indicate that the expression inside the brackets is to be treated as denoting a formal expression (formal string) of a formal language. We use an asterisk as in $F^{*}(x)$‘ to indicate the asterisked expression $F^{*}(x)$ is to be treated as denoting the interpretation of the formula $[F(x)]$ in the corresponding domain of the interpretation.

Defining the term hold’: We define the term hold’—when used in connection with an interpretation of a formal language L and, more specifically, with reference to the computations of a simple functional language associated with the atomic formulas of the language L—explicitly in Section 4; the aim being to avoid appealing to the classically subjective (and existential) connotation implicitly associated with the term under an implicitly defined standard interpretation of an arithmetic [21].

However, if a formula $[(\forall x)F(x)]$ of an arithmetic is algorithmically false under an interpretation, then we can only conclude that there is no algorithm that, for any given natural number $a$, can provide evidence whether the interpretation $F^{*}(a)$ holds or not in $N$ .

We cannot conclude that there is a numeral $[a]$ such that the formula $[F(a)]$ is algorithmically false under the interpretation; nor can we conclude that there is a natural number $b$ such that $F^{*}(b)$ does not hold in $N$.

Such a conclusion would require:

(i) either some additional evidence that will verify for some assignment of numerical values to the free variables of $[F]$ that the corresponding interpretation $F^{*}$ does not hold [22];

(ii) or the additional assumption that either Aristotle’s particularisation holds over the domain of the interpretation (as is implicitly presumed under the standard interpretation of PA over $N$) or, equivalently, that the arithmetic is $\omega$-consistent [23].

Aristotle’s particularisation: This holds that from a meta-assertion such as:

It is not the case that: For any given $x$, $P^{*}(x)$ does not hold’,

usually denoted symbolically by $\neg(\forall x)\neg P^{*}(x)$‘, we may always validly infer in the classical, Aristotlean, logic of predicates [24] that:

There exists an unspecified $x$ such that $P^{*}(x)$ holds’,

usually denoted symbolically by $(\exists x)P^{*}(x)$‘.

The significance of Aristotle’s particularisation for the first-order predicate calculus: We note that in a formal language the formula $[(\exists x)P(x)]$‘ is an abbreviation for the formula $[\neg(\forall x)\neg P(x)]$‘. The commonly accepted interpretation of this formula—and a fundamental tenet of classical logic unrestrictedly adopted as intuitively obvious by standard literature [25] that seeks to build upon the formal first-order predicate calculus—tacitly appeals to Aristotlean particularisation.

However, L. E. J. Brouwer had noted in his seminal 1908 paper on the unreliability of logical principles [26] that the commonly accepted interpretation of this formula is ambiguous if interpretation is intended over an infinite domain.

Brouwer essentially argued that, even supposing the formula $[P(x)]$‘ of a formal Arithmetical language interprets as an arithmetical relation denoted by $P^{*}(x)$‘, and the formula $[\neg(\forall x)\neg P(x)]$‘ as the arithmetical proposition denoted by $\neg(\forall x)\neg P^{*}(x)$‘, the formula $[(\exists x)P(x)]$‘ need not interpret as the arithmetical proposition denoted by the usual abbreviation $(\exists x)P^{*}(x)$‘; and that such postulation is invalid as a general logical principle in the absence of a means for constructing some putative object $a$ for which the proposition $P^{*}(a)$ holds in the domain of the interpretation.

Hence we shall follow the convention that the assumption that $(\exists x)P^{*}(x)$‘ is the intended interpretation of the formula $[(\exists x)P(x)]$‘—which is essentially the assumption that Aristotle’s particularisation holds over the domain of the interpretation—must always be explicit.

The significance of Aristotle’s particularisation for PA: In order to avoid intuitionistic objections to his reasoning, Kurt Gödel introduced the syntactic property of $\omega$-consistency as an explicit assumption in his formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions [27].

Gödel explained at some length [28] that his reasons for introducing $\omega$-consistency explicitly was to avoid appealing to the semantic concept of classical arithmetical truth in Aristotle’s logic of predicates (which presumes Aristotle’s particularisation).

It is straightforward to show that the two concepts are meta-mathematically equivalent in the sense that, if PA is consistent, then PA is $\omega$-consistent if, and only if, Aristotle’s particularisation holds under the standard interpretation of PA over $N$.

3 Defining algorithmic verifiability and algorithmic computability

The asymmetry of Section 2.1 suggests the following two concepts [29]:

Definition 1: Algorithmic verifiability: An arithmetical formula $[(\forall x)F(x)]$ is algorithmically verifiable as true under an interpretation if, and only if, for any given numeral $[a]$, we can define an algorithm which provides evidence that $[F(a)]$ interprets as true under the interpretation.

Tarskian interpretation of an arithmetical language verifiably in terms of the computations of a simple functional language: We show in Section 4 that 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; further, that the PA-formulas are decidable under the standard interpretation of PA over $N$ if, and only if, they are algorithmically verifiable under the interpretation (Corollary 2).

Definition 2: Algorithmic computability: An arithmetical formula $[(\forall x)F(x)]$ is algorithmically computable as true under an interpretation if, and only if, we can define an algorithm that, for any given numeral $[a]$, provides evidence that $[F(a)]$ interprets as true under the interpretation.

Tarskian interpretation of an arithmetical language algorithmically in terms of the computations of a simple functional language: We show in Section 4 that 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; further, that the PA-formulas are decidable under an algorithmic interpretation of PA over $N$ if, and only if, they are algorithmically computable under the interpretation .

We now show that the above concepts are well-defined under the standard interpretation of PA over $N$.

4 The implicit Satisfaction condition in Tarski’s inductive assignment of truth-values under an interpretation

We first consider the significance of the implicit Satisfaction condition in Tarski’s inductive assignment of truth-values under an interpretation.

We note that—essentially following standard expositions [30] of Tarski’s inductive definitions on the satisfiability’ and truth’ of the formulas of a formal language under an interpretation—we can define:

Definition 3: If $[A]$ is an atomic formula $[A(x_{1}, x_{2}, \ldots, x_{n})]$ of a formal language S, then the denumerable sequence $(a_{1}, a_{2}, \ldots)$ in the domain $D$ of an interpretation $\mathcal{I}_{S(D)}$ of S satisfies $[A]$ if, and only if:

(i) $[A(x_{1}, x_{2}, \ldots, x_{n})]$ interprets under $\mathcal{I}_{S(D)}$ as a unique relation $A^{*}(x_{1}, x_{2},$ $\ldots, x_{n})$ in $D$ for any witness $\mathcal{W}_{D}$ of $D$;

(ii) there is a Satisfaction Method, SM($\mathcal{I}_{S(D)}$) that provides objective evidence [30] by which any witness $\mathcal{W}_{D}$ of $D$ can objectively define for any atomic formula $[A(x_{1}, x_{2}, \ldots, x_{n})]$ of S, and any given denumerable sequence $(b_{1}, b_{2}, \ldots)$ of $D$, whether the proposition $A^{*}(b_{1}, b_{2}, \ldots, b_{n})$ holds or not in $D$;

(iii) $A^{*}(a_{1}, a_{2}, \ldots, a_{n})$ holds in $D$ for any $\mathcal{W}_{D}$.

Witness: From a constructive perspective, the existence of a witness’ as in (i) above is implicit in the usual expositions of Tarski’s definitions.

Satisfaction Method: From a constructive perspective, the existence of a Satisfaction Method as in (ii) above is also implicit in the usual expositions of Tarski’s definitions.

A constructive perspective: We highlight the word define‘ in (ii) above to emphasise the constructive perspective underlying this paper; which is that the concepts of satisfaction’ and truth’ under an interpretation are to be explicitly viewed as objective assignments by a convention that is witness-independent. A Platonist perspective would substitute decide’ for define’, thus implicitly suggesting that these concepts can exist’, in the sense of needing to be discovered by some witness-dependent means—eerily akin to a revelation’—if the domain $D$ is $N$.

We can now inductively assign truth values of satisfaction’, truth’, and falsity’ to the compound formulas of a first-order theory S under the interpretation $\mathcal{I}_{S(D)}$ in terms of only the satisfiability of the atomic formulas of S over $D$ as usual [31]:

Definition 4: A denumerable sequence $s$ of $D$ satisfies $[\neg A]$ under $\mathcal{I}_{S(D)}$ if, and only if, $s$ does not satisfy $[A]$;

Definition 5: A denumerable sequence $s$ of $D$ satisfies $[A \rightarrow B]$ under $\mathcal{I}_{S(D)}$ if, and only if, either it is not the case that $s$ satisfies $[A]$, or $s$ satisfies $[B]$;

Definition 6: A denumerable sequence $s$ of $D$ satisfies $[(\forall x_{i})A]$ under $\mathcal{I}_{S(D)}$ if, and only if, given any denumerable sequence $t$ of $D$ which differs from $s$ in at most the $i$‘th component, $t$ satisfies $[A]$;

Definition 7: A well-formed formula $[A]$ of $D$ is true under $\mathcal{I}_{S(D)}$ if, and only if, given any denumerable sequence $t$ of $D$, $t$ satisfies $[A]$;

Definition 8: A well-formed formula $[A]$ of $D$ is false under $\mathcal{I}_{S(D)}$ if, and only if, it is not the case that $[A]$ is true under $\mathcal{I}_{S(D)}$.

It follows that [32]:

Theorem 1: (Satisfaction Theorem) If, for any interpretation $\mathcal{I}_{S(D)}$ of a first-order theory S, there is a Satisfaction Method SM($\mathcal{I}_{S(D)}$) which holds for a witness $\mathcal{W}_{D}$ of $D$, then:

(i) The $\Delta_{0}$ formulas of S are decidable as either true or false over $D$ under $\mathcal{I}_{S(D)}$;

(ii) If the $\Delta_{n}$ formulas of S are decidable as either true or as false over $D$ under $\mathcal{I}_{S(D)}$, then so are the $\Delta(n+1)$ formulas of S.

Proof: It follows from the above definitions that:

(a) If, for any given atomic formula $[A(x_{1}, x_{2}, \ldots, x_{n})]$ of S, it is decidable by $\mathcal{W}_{D}$ whether or not a given denumerable sequence $(a_{1}, a_{2}, \ldots)$ of $D$ satisfies $[A(x_{1}, x_{2}, \ldots, x_{n})]$ in $D$ under $\mathcal{I}_{S(D)}$ then, for any given compound formula $[A^{1}(x_{1}, x_{2}, \ldots, x_{n})]$ of S containing any one of the logical constants $\neg, \rightarrow, \forall$, it is decidable by $\mathcal{W}_{D}$ whether or not $(a_{1}, a_{2}, \ldots)$ satisfies $[A^{1}(x_{1}, x_{2}, \ldots, x_{n})]$ in $D$ under $\mathcal{I}_{S(D)}$;

(b) If, for any given compound formula $[B^{n}(x_{1}, x_{2}, \ldots, x_{n})]$ of S containing $n$ of the logical constants $\neg, \rightarrow, \forall$, it is decidable by $\mathcal{W}_{D}$ whether or not a given denumerable sequence $(a_{1}, a_{2}, \ldots)$ of $D$ satisfies $[B^{n}(x_{1}, x_{2}, \ldots, x_{n})]$ in $D$ under $\mathcal{I}_{S(D)}$ then, for any given compound formula $[B^{(n+1)}(x_{1}, x_{2}, \ldots, x_{n})]$ of S containing $n+1$ of the logical constants $\neg, \rightarrow, \forall$, it is decidable by $\mathcal{W}_{D}$ whether or not $(a_{1}, a_{2}, \ldots)$ satisfies $[B^{(n+1)}(x_{1}, x_{2}, \ldots, x_{n})]$ in $D$ under $\mathcal{I}_{S(D)}$;

We thus have that:

(c) The $\Delta_{0}$ formulas of S are decidable by $\mathcal{W}_{D}$ as either true or false over $D$ under $\mathcal{I}_{S(D)}$;

(d) If the $\Delta_{n}$ formulas of S are decidable by $\mathcal{W}_{D}$ as either true or as false over $D$ under $\mathcal{I}_{S(D)}$, then so are the $\Delta(n+1)$ formulas of S. $\Box$

In other words, if the atomic formulas of of S interpret under $\mathcal{I}_{S(D)}$ as decidable with respect to the Satisfaction Method SM($\mathcal{I}_{S(D)}$) by a witness $\mathcal{W}_{D}$ over some domain $D$, then the propositions of S (i.e., the $\Pi_{n}$ and $\Sigma_{n}$ formulas of S) also interpret as decidable with respect to SM($\mathcal{I}_{S(D)}$) by the witness $\mathcal{W}_{D}$ over $D$.

We now consider the application of Tarski’s definitions to various interpretations of first-order Peano Arithmetic PA.

4.1 The standard interpretation of PA over the domain $N$ of the natural numbers

The standard interpretation $\mathcal{I}_{PA(N,\ Standard)}$ of PA over the domain $N$ of the natural numbers is obtained if, in $\mathcal{I}_{S(D)}$:

(a) we define S as PA with standard first-order predicate calculus as the underlying logic [34];

(b) we define $D$ as the set $N$ of natural numbers;

(c) for any atomic formula $[A(x_{1}, x_{2}, \ldots, x_{n})]$ of PA and sequence $(a_{1}, a_{2}, \ldots, a_{n})$ of $N$, we take $\|$SATCON($\mathcal{I}_{PA(N)}$)$\|$ as:

$\|$$A^{*}(a_{1}^{*}, a_{2}^{*}, \ldots, a_{n}^{*})$ holds in $N$ and, for any given sequence $(b_{1}^{*}, b_{2}^{*}, \ldots, b_{n}^{*})$ of $N$, the proposition $A^{*}(b_{1}^{*}, b_{2}^{*}, \ldots, b_{n}^{*})$ is decidable in $N$$\|$;

(d) we define the witness $\mathcal{W}_{(N,\ Standard)}$ informally as the mathematical intuition’ of a human intelligence for whom, classically, $\|$SATCON($\mathcal{I}_{PA(N)}$)$\|$ has been implicitly accepted as objectively decidable’ in $N$;

We shall show that such acceptance is justified, but needs to be made explicit since:

Lemma 1: $A^{*}(x_{1}, x_{2}, \ldots, x_{n})$ is both algorithmically verifiable and algorithmically computable in $N$ by $\mathcal{W}_{(N,\ Standard)}$.

Proof: (i) It follows from the argument in Theorem 2 (below) that $A^{*}(x_{1}, x_{2}, \ldots, x_{n})$ is algorithmically verifiable in $N$ by $\mathcal{W}_{(N,\ Standard)}$.

(ii) It follows from the argument in Theorem 3 (below) that $A^{*}(x_{1}, x_{2},$ $\ldots, x_{n})$ is algorithmically computable in $N$ by $\mathcal{W}_{(N,\ Standard)}$. The lemma follows. $\Box$

Now, although it is not immediately obvious from the standard interpretation of PA over $N$ which of (i) or (ii) may be taken for explicitly deciding $\|$SATCON($\mathcal{I}_{PA(N)}$)$\|$ by the witness $\mathcal{W}_{(N,\ Standard)}$, we shall show in Section 4.2 that (i) is consistent with (e) below; and in Section 4.3 that (ii) is inconsistent with (e). Thus the standard interpretation of PA over $N$ implicitly presumes (i).

(e) we postulate that Aristotle’s particularisation holds over $N$ [35].

Clearly, (e) does not form any part of Tarski’s inductive definitions of the satisfaction, and truth, of the formulas of PA under the above interpretation. Moreover, its inclusion makes $\mathcal{I}_{PA(N,\ Standard)}$ extraneously non-finitary [36].

We note further that if PA is $\omega$inconsistent, then Aristotle’s particularisation does not hold over $N$, and the interpretation $\mathcal{I}_{PA(N,\ Standard)}$ is not sound over $N$.

4.2 An instantiational interpretation of PA over the domain $\mathbb {N}$ of the PA numerals

We next consider an instantiational interpretation $\mathcal{I}_{PA(\mathbb {N},\ Instantiational)}$ of PA over the domain $\mathbb {N}$ of the PA numerals [37] where:

(a) we define S as PA with standard first-order predicate calculus as the underlying logic;

(b) we define $D$ as the set $\mathbb {N}$ of PA numerals;

(c) for any atomic formula $[A(x_{1}, x_{2}, \ldots, x_{n})]$ of PA and any sequence $[(a_{1}, a_{2}, \ldots, a_{n})]$ of PA numerals in $\mathbb {N}$, we take $\|$SATCON($\mathcal{I}_{PA(\mathbb{N})}$)$\|$ as:

$\|$$[A(a_{1}, a_{2}, \ldots, a_{n})]$ is provable in PA and, for any given sequence of numerals $[(b_{1}, b_{2}, \ldots, b_{n})]$ of PA, the formula $[A(b_{1}, b_{2}, \ldots, b_{n})]$ is decidable as either provable or not provable in PA$\|$;

(d) we define the witness $\mathcal{W}_{(\mathbb {N},\ Instantiational)}$ as the meta-theory $\mathcal{M}_{PA}$ of PA.

Lemma 2: $[A(x_{1}, x_{2}, \ldots, x_{n})]$ is always algorithmically verifiable in PA by $\mathcal{W}_{(\mathbb {N},\ Instantiational)}$.

Proof: It follows from Gödel’s definition of the primitive recursive relation $xBy$ [38]—where $x$ is the Gödel number of a proof sequence in PA whose last term is the PA formula with Gödel-number $y$—that, if $[A(x_{1}, x_{2}, \ldots, x_{n})]$ is an atomic formula of PA, $\mathcal{M}_{PA}$ can algorithmically verify for any given sequence $[(b_{1}, b_{2}, \ldots, b_{n})]$ of PA numerals which one of the PA formulas $[A(b_{1}, b_{2}, \ldots, b_{n})]$ and $[\neg A(b_{1}, b_{2}, \ldots, b_{n})]$ is necessarily PA-provable. $\Box$

Now, if PA is consistent but not $\omega$-consistent, then there is a Gödelian formula $[R(x)]$ [39] such that:

(i) $[(\forall x)R(x)]$ is not PA-provable;

(ii) $[\neg (\forall x)R(x)]$ is PA-provable;

(iii) for any given numeral $[n]$, the formula $[R(n)]$ is PA-provable.

However, if $\mathcal{I}_{PA(\mathbb {N},\ Instantiational)}$ is sound over $\mathbb {N}$, then (ii) implies contradictorily that it is not the case that, for any given numeral $[n]$, the formula $[R(n)]$ is PA-provable.

It follows that if $\mathcal{I}_{PA(\mathbb {N},\ Instantiational)}$ is sound over $\mathbb {N}$, then PA is $\omega$-consistent and, ipso facto, Aristotle’s particularisation must hold over $N$.

Moreover, if PA is consistent, then every PA-provable formula interprets as true under some sound interpretation of PA over $N$. Hence $\mathcal{M}_{PA}$ can effectively decide whether, for any given sequence of natural numbers $(b_{1}^{*}, b_{2}^{*},$ $\ldots, b_{n}^{*})$ in $N$, the proposition $A^{*}(b_{1}^{*}, b_{2}^{*}, \ldots, b_{n}^{*})$ holds or not in $N$.

It follows that $\mathcal{I}_{PA(\mathbb {N},\ Instantiational)}$ can be viewed as a constructive formalisation of the standard’ interpretation $\mathcal{I}_{PA(N,\ Standard)}$ of PA in which we do not need to non-constructively assume that Aristotle’s particularisation holds over $N$.

4.3 An algorithmic interpretation of PA over the domain $N$ of the natural numbers

We finally consider the purely algorithmic interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ of PA over the domain $N$ of the natural numbers where:

(a) we define S as PA with standard first-order predicate calculus as the underlying logic;

(b) we define $D$ as the set $N$ of natural numbers;

(c) for any atomic formula $[A(x_{1}, x_{2}, \ldots, x_{n})]$ of PA and any sequence $(a_{1}, a_{2}, \ldots, a_{n})$ of natural numbers in $N$, we take $\|$SATCON($\mathcal{I}_{PA(N)}$)$\|$ as:

$\|$$A^{*}(a_{1}^{*}, a_{2}^{*}, \ldots, a_{n}^{*})$ holds in $N$ and, for any given sequence $(b_{1}^{*}, b_{2}^{*}, \ldots, b_{n}^{*})$ of $N$, the proposition $A^{*}(b_{1}^{*}, b_{2}^{*}, \ldots, b_{n}^{*})$ is decidable as either holding or not holding in $N$$\|$;

(d) we define the witness $\mathcal{W}_{(N,\ Algorithmic)}$ as any simple functional language that gives evidence that $\|$SATCON($\mathcal{I}_{PA(N)}$)$\|$ is always effectively decidable in $N$:

Lemma 3: $A^{*}(x_{1}, x_{2}, \ldots, x_{n})$ is always algorithmically computable in $N$ by $\mathcal{W}_{(N,\ Algorithmic)}$.

Proof: If $[A(x_{1}, x_{2}, \ldots, x_{n})]$ is an atomic formula of PA then, for any given sequence of numerals $[b_{1}, b_{2}, \ldots, b_{n}]$, the PA formula $[A(b_{1}, b_{2},$ $\ldots, b_{n})]$ is an atomic formula of the form $[c=d]$, where $[c]$ and $[d]$ are atomic PA formulas that denote PA numerals. Since $[c]$ and $[d]$ are recursively defined formulas in the language of PA, it follows from a standard result [40] that, if PA is consistent, then $[c=d]$ is algorithmically computable as either true or false in $N$. In other words, if PA is consistent, then $[A(x_{1}, x_{2}, \ldots, x_{n})]$ is algorithmically computable (since there is an algorithm that, for any given sequence of numerals $[b_{1}, b_{2}, \ldots, b_{n}]$, will give evidence whether $[A(b_{1}, b_{2},$ $\ldots, b_{n})]$ interprets as true or false in $N$. The lemma follows. $\Box$

It follows that $\mathcal{I}_{PA(N,\ Algorithmic)}$ is an algorithmic formulation of the standard’ interpretation of PA over $N$ in which we do not extraneously assume either that Aristotle’s particularisation holds over $N$ or, equivalently, that PA is $\omega$-consistent.

5 Formally defining the standard interpretation of PA over $N$ constructively

It follows from the analysis of the applicability of Tarski’s inductive definitions of satisfiability’ and truth’ in Section 4 that we can formally define the standard interpretation $\mathcal{I}_{PA(N,\ Standard)}$ of PA constructively where:

(a) we define S as PA with standard first-order predicate calculus as the underlying logic;

(b) we define $D$ as $N$;

(c) we take SM($\mathcal{I}_{PA(N,\ Standard)}$) as any simple functional language.

We note that:

Theorem 2: The atomic formulas of PA are algorithmically verifiable under the standard interpretation $\mathcal{I}_{PA(N,\ Standard)}$.

Proof: If $[A(x_{1}, x_{2}, \ldots, x_{n})]$ is an atomic formula of PA then, for any given denumerable sequence of numerals $[b_{1}, b_{2}, \ldots]$, the PA formula $[A(b_{1}, b_{2},$ $\ldots, b_{n})]$ is an atomic formula of the form $[c=d]$, where $[c]$ and $[d]$ are atomic PA formulas that denote PA numerals. Since $[c]$ and $[d]$ are recursively defined formulas in the language of PA, it follows from a standard result that, if PA is consistent, then $[c=d]$ interprets as the proposition $c=d$ which either holds or not for a witness $\mathcal{W}_{N}$ in $N$.

Hence, if PA is consistent, then $[A(x_{1}, x_{2}, \ldots, x_{n})]$ is algorithmically verifiable since, for any given denumerable sequence of numerals $[b_{1}, b_{2}, \ldots]$, we can define an algorithm that provides evidence that the PA formula $[A(b_{1}, b_{2}, \ldots, b_{n})]$ is decidable under the interpretation.

The theorem follows. $\Box$

It immediately follows that:

Corollary 1: The satisfaction’ and truth’ of PA formulas containing logical constants can be defined under the standard interpretation of PA over $N$ in terms of the evidence provided by the computations of a simple functional language.

Corollary 2: The PA-formulas are decidable under the standard interpretation of PA over $N$ if, and only if, they are algorithmically verifiable under the interpretation.

5.1 Defining algorithmic truth’ under the standard interpretation of PA over $N$

Now we note that, in addition to Theorem 2:

Theorem 3: The atomic formulas of PA are algorithmically computable under the standard interpretation $\mathcal{I}_{PA(N,\ Standard)}$.

Proof: If $[A(x_{1}, x_{2}, \ldots, x_{n})]$ is an atomic formula of PA then we can define an algorithm that, for any given denumerable sequence of numerals $[b_{1}, b_{2}, \ldots]$, provides evidence whether the PA formula $[A(b_{1}, b_{2}, \ldots, b_{n})]$ is true or false under the interpretation.

The theorem follows. $\Box$

This suggests the following definitions:

Definition 9: A well-formed formula $[A]$ of PA is algorithmically true under $\mathcal{I}_{PA(N,\ Standard)}$ if, and only if, there is an algorithm which provides evidence that, given any denumerable sequence $t$ of $N$, $t$ satisfies $[A]$;

Definition 10:A well-formed formula $[A]$ of PA is algorithmically false under $\mathcal{I}_{PA(N,\ Standard)}$ if, and only if, it is not algorithmically true under $\mathcal{I}_{PA(N)}$.

5.2 The PA axioms are algorithmically computable

The significance of defining algorithmic truth’ under $\mathcal{I}_{PA(N,\ Standard)}$ as above is that:

Lemma 4: The PA axioms PA$_{1}$ to PA$_{8}$ are algorithmically computable as algorithmically true over $N$ under the interpretation $\mathcal{I}_{PA(N,\ Standard)}$.

Proof: Since $[x+y]$, $[x \star y]$, $[x = y]$, $[{x^{\prime}}]$ are defined recursively [41], the PA axioms PA$_{1}$ to PA$_{8}$ interpret as recursive relations that do not involve any quantification. The lemma follows straightforwardly from Definitions 3 to 8 in Section 4 and Theorem 2. $\Box$

Lemma 5: For any given PA formula $[F(x)]$, the Induction axiom schema $[F(0)$ $\rightarrow (((\forall x)(F(x) \rightarrow F(x^{\prime}))) \rightarrow (\forall x)F(x))]$ interprets as algorithmically true under $\mathcal{I}_{PA(N,\ Standard)}$.

Proof: By Definitions 3 to 10:

(a) If $[F(0)]$ interprets as algorithmically false under $\mathcal{I}_{PA(N,\ Standard)}$ the lemma is proved.

Since $[F(0) \rightarrow (((\forall x)(F(x) \rightarrow F(x^{\prime}))) \rightarrow (\forall x)F(x))]$ interprets as algorithmically true if, and only if, either $[F(0)]$ interprets as algorithmically false or $[((\forall x)(F(x) \rightarrow F(x^{\prime}))) \rightarrow (\forall x)F(x)]$ interprets as algorithmically true.

(b) If $[F(0)]$ interprets as algorithmically true and $[(\forall x)(F(x) \rightarrow F(x^{\prime}))]$ interprets as algorithmically false under $\mathcal{I}_{PA(N,\ Standard)}$, the lemma is proved.

(c) If $[F(0)]$ and $[(\forall x)(F(x) \rightarrow F(x^{\prime}))]$ both interpret as algorithmically true under $\mathcal{I}_{PA(N,\ Standard)}$, then by Definition 9 there is an algorithm which, for any natural number $n$, will give evidence that the formula $[F(n) \rightarrow F(n^{\prime})]$ is true under $\mathcal{I}_{PA(N,\ Standard)}$.

Since $[F(0)]$ interprets as algorithmically true under $\mathcal{I}_{PA(N,\ Standard)}$, it follows that there is an algorithm which, for any natural number $n$, will give evidence that the formula $[F(n)]$ is true under the interpretation.

Hence $[(\forall x)F(x)]$ is algorithmically true under $\mathcal{I}_{PA(N,\ Standard)}$.

Since the above cases are exhaustive, the lemma follows. $\Box$

The Poincaré-Hilbert debate: We note that Lemma 5 appears to settle the Poincaré-Hilbert debate [42] in the latter’s favour. Poincaré believed that the Induction Axiom could not be justified finitarily, as any such argument would necessarily need to appeal to infinite induction. Hilbert believed that a finitary proof of the consistency of PA was possible.

Lemma 6: Generalisation preserves algorithmic truth under $\mathcal{I}_{PA(N,\ Standard)}$.

Proof: The two meta-assertions:

$[F(x)]$ interprets as algorithmically true under $\mathcal{I}_{PA(N,\ Standard)}$ [43]

and

$[(\forall x)F(x)]$ interprets as algorithmically true under $\mathcal{I}_{PA(N,\ Standard)}$

both mean:

$[F(x)]$ is algorithmically computable as always true under $\mathcal{I}_{PA(N),}$ $_{Standard)}$. $\Box$

It is also straightforward to see that:

Modus Ponens preserves algorithmic truth under $\mathcal{I}_{PA(N,\ Standard)}$. $\Box$

We thus have that:

Theorem 4: The axioms of PA are always algorithmically true under the interpretation $\mathcal{I}_{PA(N,\ Standard)}$, and the rules of inference of PA preserve the properties of algorithmic satisfaction/truth under $\mathcal{I}_{PA(N,\ Standard)}$ [44]. $\Box$

5.3 The interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ of PA over $N$ is sound

We conclude from Section 4.3 and Section 5.2 that there is an algorithmic interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ of PA over $N$ such that:

Theorem 5: The interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ of PA is sound over $N$.

Proof: It follows immediately from Theorem 4 that the axioms of PA are always true under the interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$, and the rules of inference of PA preserve the properties of satisfaction/truth under $\mathcal{I}_{PA(N,\ Algorithmic)}$. $\Box$

We thus have a finitary proof that:

Theorem 6: PA is consistent. $\Box$

Conclusion

We have shown that although conventional wisdom is justified in assuming that the quantified arithmetical propositions of the first order Peano Arithmetic PA are constructively decidable under the standard interpretation of PA over the domain $N$ of the natural numbers, the assumption does not address—and implicitly conceals—a significant ambiguity that needs to be made explicit.

Reason: Tarski’s inductive definitions admit evidence-based interpretations of the first-order Peano Arithmetic PA that allow us to define the satisfaction and truth of the quantified formulas of PA constructively over $N$ in two essentially different ways.

First in terms of algorithmic verifiabilty. We show that this allows us to define a formal instantiational interpretation $\mathcal{I}_{PA(\mathbb {N},\ Instantiational)}$ of PA over the domain $\mathbb {N}$ of the PA numerals that is sound (i.e. PA theorems interpret as true in $N$) if, and only if, the standard interpretation of PA over $N$—which is not known to be finitary—is sound.

Second in terms of algorithmic computability. We show that this allows us to define a finitary algorithmic interpretation $\mathcal{I}_{PA(N,\ Algorithmic)}$ of PA over $N$ which is sound, and so we may conclude that PA is consistent.

Acknowledgements

We would like to thank Professor Rohit Parikh for his suggestion that this paper should appeal to the computations of a simple functional language in general, and avoid appealing to the computations of a Turing machine in particular.

References

BBJ03 George S. Boolos, John P. Burgess, Richard C. Jeffrey. 2003. Computability and Logic (4th ed). Cambridge University Press, Cambridge.

Be59 Evert W. Beth. 1959. The Foundations of Mathematics. Studies in Logic and the Foundations of Mathematics. Edited by L. E. J. Brouwer, E. W. Beth, A. Heyting. 1959. North Holland Publishing Company, Amsterdam.

BF58 Paul Bernays and Abraham A. Fraenkel. 1958. Axiomatic Set Theory. Studies in Logic and the Foundations of Mathematics. Edited by L. E. J. Brouwer, E. W. Beth, A. Heyting. 1959. North Holland Publishing Company, Amsterdam.

Br08 L. E. J. Brouwer. 1908. The Unreliability of the Logical Principles. English translation in A. Heyting, Ed. L. E. J. Brouwer: Collected Works 1: Philosophy and Foundations of Mathematics. Amsterdam: North Holland / New York: American Elsevier (1975): pp.107-111.

Br13 L. E. J. Brouwer. 1913. Intuitionism and Formalism. Inaugural address at the University of Amsterdam, October 14, 1912. Translated by Professor Arnold Dresden for the Bulletin of the American Mathematical Society, Volume 20 (1913), pp.81-96. 1999. Electronically published in Bulletin (New Series) of the American Mathematical Society, Volume 37, Number 1, pp.55-64.

Co66 Paul J. Cohen. 1966. Set Theory and the Continuum Hypothesis. (Lecture notes given at Harvard University, Spring 1965) W. A. Benjamin, Inc., New York.

Cr05 John N. Crossley. 2005. What is Mathematical Logic? A Survey. Address at the First Indian Conference on Logic and its Relationship with Other Disciplines held at the Indian Institute of Technology, Powai, Mumbai from January 8 to 12. Reprinted in Logic at the Crossroads: An Interdisciplinary View – Volume I (pp.3-18). ed. Amitabha Gupta, Rohit Parikh and Johan van Bentham. 2007. Allied Publishers Private Limited, Mumbai.

Da82 Martin Davis. 1958. Computability and Unsolvability. 1982 ed. Dover Publications, Inc., New York.

EC89 Richard L. Epstein, Walter A. Carnielli. 1989. Computability: Computable Functions, Logic, and the Foundations of Mathematics. Wadsworth & Brooks, California.

Fe06 Solomon Feferman. 2006. Are There Absolutely Unsolvable Problems? Gödel’s Dichotomy. Philosophia Mathematica (2006) 14 (2): 134-152.

Fe08 Solomon Feferman. 2008. Lieber Herr Bernays!, Lieber Herr Gödel! Gödel on finitism, constructivity and Hilbert’s program. in Special Issue: Gödel’s dialectica Interpretation Dialectica, Volume 62, Issue 2, June 2008, pp. 245-290.

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.

HA28 David Hilbert & Wilhelm Ackermann. 1928. Principles of Mathematical Logic. Translation of the second edition of the Grundzüge Der Theoretischen Logik. 1928. Springer, Berlin. 1950. Chelsea Publishing Company, New York.

Hi25 David Hilbert. 1925. On the Infinite. Text of an address delivered in Münster on 4th June 1925 at a meeting of the Westphalian Mathematical Society. In Jean van Heijenoort. 1967.Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

Hi27 David Hilbert. 1927. The Foundations of Mathematics. Text of an address delivered in July 1927 at the Hamburg Mathematical Seminar. In Jean van Heijenoort. 1967.Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

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

Kn63 G. T. Kneebone. 1963. Mathematical Logic and the Foundations of Mathematics: An Introductory Survey. D. Van Norstrand Company Limited, London.

Li64 A. H. Lightstone. 1964. The Axiomatic Method. Prentice Hall, NJ.

Me64 Elliott Mendelson. 1964. Introduction to Mathematical Logic. Van Norstrand, Princeton.

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.

Nv64 P. S. Novikov. 1964. Elements of Mathematical Logic. Oliver & Boyd, Edinburgh and London.

Pa71 Rohit Parikh. 1971. Existence and Feasibility in Arithmetic. The Journal of Symbolic Logic, Vol.36, No. 3 (Sep., 1971), pp. 494-508.

Qu63 Willard Van Orman Quine. 1963. Set Theory and its Logic. Harvard University Press, Cambridge, Massachusette.

Rg87 Hartley Rogers Jr. 1987. Theory of Recursive Functions and Effective Computability.<i. MIT Press, Cambridge, Massachusetts.

Ro53 J. Barkley Rosser. 1953. Logic for Mathematicians McGraw Hill, New York.

Ru53 Walter Rudin. 1953. Principles of Mathematical Analysis. McGraw Hill, New York.

Sh67 Joseph R. Shoenfield. 1967. Mathematical Logic. Reprinted 2001. A. K. Peters Ltd., Massachusetts.

Sk28 Thoralf Skolem. 1928. On Mathematical Logic Text of a lecture delivered on 22nd October 1928 before the Norwegian Mathematical Association. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

Sm92 Raymond M. Smullyan. 1992. Gödel’s Incompleteness Theorems. Oxford University Press, Inc., New York.

Su60 Patrick Suppes. 1960. Axiomatic Set Theory. Van Norstrand, Princeton.

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

Wa63 Hao Wang. 1963. A survey of Mathematical Logic. North Holland Publishing Company, Amsterdam.

We27 Hermann Weyl. 1927. Comments on Hilbert’s second lecture on the foundations of mathematics In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

Notes

Return to 1: For a brief recent review of such challenges, see Fe06, Fe08.

Return to 3: We take this to be the first-order theory S defined in Me64, p.102.

Return to 5: We define this important concept explicitly later in Section 2.1. Loosely speaking, Aristotle’s particularisation is the assumption that we may always interpret the formal expression [$(\exists x)F(x)$]’ of a formal language under an interpretation as There exists an object $s$ in the domain of the interpretation such that $F(s)$‘.

Return to 7: Finitary’ in the sense that “… there should be an algorithm for deciding the truth or falsity of any mathematical statement“. For a brief review of finitism’ and constructivity’ in the context of this paper see Fe08.

Return to 10: The possibility/impossibility of such justification was the subject of the famous Poincaré-Hilbert debate. See Hi27, p.472; also Br13, p.59; We27, p.482; Pa71, p.502-503.

Return to 11: In the sense highlighted by Elliott Mendelson in Me64, p.261.

Return to 19: Such as, for instance, that of a deterministic Turing machine (Me64, pp.229-231) based essentially on Alan Turing’s seminal 1936 paper on computable numbers (Tu36).

Return to 22: Essentially reflecting Brouwer’s objection to the assumption of Aristotle’s particularisation over an infinite domain.

Return to 25: See Hi25, p.382; HA28, p.48; Sk28, p.515; Go31, p.32.; Kl52, p.169; Ro53, p.90; BF58, p.46; Be59, pp.178 & 218; Su60, p.3; Wa63, p.314-315; Qu63, pp.12-13; Kn63, p.60; Co66, p.4; Me64, p.52(ii); Nv64, p.92; Li64, p.33; Sh67, p.13; Da82, p.xxv; Rg87, p.xvii; EC89, p.174; Mu91; Sm92, p.18, Ex.3; BBJ03, p.102; Cr05, p.6.

Return to 29: The distinction sought to be made between algorithmic verifiabilty and algorithmic computability can be viewed as reflecting in number theory the similar distinction in analysis between, for instance, continuous functions (Ru53, p.65, $\S$4.5) and uniformly continuous functions (Ru53, p.65, $\S$4.13); or that between convergent sequences (Ru53, p.65, $\S$7.1) and uniformly convergent sequences (Ru53, p.65, $\S$7.7).}

Return to 34: Where the string $[(\exists \ldots)]$ is defined as—and is to be treated as an abbreviation for—the string $[\neg (\forall \ldots) \neg]$. We do not consider the case where the underlying logic is Hilbert’s formalisation of Aristotle’s logic of predicates in terms of his $\epsilon$-operator (Hi27, pp.465-466).

Return to 35: Hence a PA formula such as $[(\exists x)F(x)]$ interprets under $\mathcal{I}_{PA(N,\ Standard)}$ as There is some natural number $n$ such that $F(n)$ holds in $N$.

Return to 37: The raison d’être, and significance, of such interpretation is outlined in this short unpublished note accessible at http://alixcomsi.com/8\_Meeting\_Wittgenstein\_requirement\_1000.pdf.

Return to 39: Gödel constructively defines, and refers to, this formula by its Gödel number $r$‘: see Go31, p.25, Eqn.(12).

Return to 40: For any natural numbers $m,\ n$, if $m \neq n$, then PA proves $[\neg(m = n)]$ (Me64, p.110, Proposition 3.6). The converse is obviously true.

Return to 42: See Hi27, p.472; also Br13, p.59; We27, p.482; Pa71, p.502-503.

Author’s working archives & abstracts of investigations

See also (i) this later publication by Sebastian Grève, where he concludes that “… while Gödel indeed showed some significant understanding of Wittgenstein here, ultimately, Wittgenstein perhaps understood Gödel better than Gödel understood himself”; and (ii) this note on Rosser’s Rule C and Wittgenstein’s objections on purely philosophical considerations to Gödel’s reasoning and conclusions, where we show that, although not at all obvious (perhaps due to Gödel’s overpoweringly plausible presentation of his interpretation of his own formal reasoning over the years) what Gödel claimed to have proven is not—as suspected and held by Wittgenstein—supported by Gödel’s formal argumentation.

A: Misunderstanding Gödel’s Theorems VI and XI: Incompleteness and Undecidability

In an informal essay, “Misunderstanding Gödel’s Theorems VI and XI: Incompleteness and Undecidability“, DPhil candidate Sebastian Grève at The Queen’s College, Oxford, attempts to come to terms with what he subjectively considers:

“… has not been properly addressed as such by philosophers hitherto as of great philosophical importance in our understanding of Gödel’s Incompleteness Theorems.”

Grève’s is an unusual iconoclastic perspective:

“This essay is an open enquiry towards a better understanding of the philosophical significance of Gödel’s two most famous theorems. I proceed by a discussion of several common misunderstandings, led by the following four questions:

1) Is the Gödel sentence true?

2) Is the Gödel sentence undecidable?

3) Is the Gödel sentence a statement?

4) Is the Gödel sentence a sentence?

Asking these questions in this order means to trace back the steps of Gödel’s basic philosophical interpretation of his formal results. What I call the basic philosophical interpretation is usually just taken for granted by philosopher’s writing about Gödel’s theorems.”

In a footnote Grève acknowledges Wittgenstein’s influence by suggesting that:

“This essay can be read as something like a free-floating interpretation of the theme of Wittgenstein’s remarks on Gödel’s Incompleteness Theorems in Wittgenstein: 1978[RFM], I-(III), partly following Floyd: 1995 but especially Kienzler: 2008, and constituting a reply to inter alia Rodych: 2003”.

B: Why we may see the trees, but not the forest

We note that Grève’s four points are both overdue and well-made:

1. Is the Gödel sentence true?

Grève’s objection that standard interpretations are obscure when they hold the Gödel sentence as being intuitively true deserves consideration (see this post).

The ‘truth’ of the sentence should and does—as Wittgenstein stressed and suggested—follow objectively from the axioms and rules of inference of arithmetic.

2. Is the Gödel sentence undecidable?

Grève’s observation that the ‘undecidability’ of the Gödel sentence conceals a philosophically questionable assumption is well-founded.

The undecidability in question follows only on the assumption of ‘$\omega$-consistency’ made explicitly by Gödel.

This assumption is actually logically equivalent to the philosophically questionable assertion that from the provability of $[\neg(\forall x)R(x)]$ we may conclude the existence of some numeral $[n]$ for which $[R(n)]$ is provable.

Since Rosser’s proof implicitly makes this assumption by means of his logically questionable Rule C, his claim of avoiding omega-consistency for arithmetic is illusory.

3. Is the Gödel sentence a statement?

Grève rightly holds that the Gödel sentence should be treated as a valid statement within the formal arithmetic S, since it is structurally defined as a well-formed formula of S.

4. Is the Gödel sentence a sentence?

Grève’s concern about whether the Gödel sentence of S is a valid arithmetical proposition under interpretation also seems to need serious philosophical consideration.

It can be argued (see the comment following the proof of Lemma 9 of this preprint) that the way the sentence is formally defined as the universal quantification of an instantiationally (but not algorithmically) defined arithmetical predicate does not yield an unequivocally defined arithmetical proposition in the usual sense under interpretation.

In this post [*] we shall not only echo Grève’s disquietitude, but argue further that Gödel’s interpretation and assessment of his own formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions is, essentially, a post-facto imposition that continues to influence standard expositions of Gödel’s reasoning misleadingly.

Feynman’s cover-up factor

Our thesis is influenced by physicist Richard P. Feynman, who started his 1965 Nobel Lecture with a penetrating observation:

We have a habit in writing articles published in scientific journals to make the work as finished as possible, to cover up all the tracks, to not worry about the blind alleys or describe how you had the wrong idea first, and so on. So there isn’t any place to publish, in a dignified manner, what you actually did in order to get to do the work.

That such cover up’ may have unintended—and severely limiting—consequences on a discipline is suggested by Gödel’s interpretation, and assessment, of his own formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions (Go31).

Thus, in his informal preamble to the result that he intended to prove formally, Gödel wrote (cf. Go31, p.9):

The analogy of this result with Richard’s antinomy is immediately evident; there is also a close relationship with the Liar Paradox … Thus we have a proposition before us which asserts its own unprovability.

Further, interpreting the significance of his formal reasoning as having established the existence of a formally undecidable arithmetical proposition that is, however, decidable by meta-mathematical arguments, Gödel noted that:

The precise analysis of this remarkable circumstance leads to surprising results concerning consistency proofs of formal systems … (Go31, p.9)

The true reason for the incompleteness which attaches to all formal systems of mathematics lies, as will be shown in Part II of this paper, in the fact that the formation of higher and higher types can be continued into the transfinite (c.f., D. Hilbert, Über das Unendliche’, Math. Ann. 95, p. 184), while, in every formal system, only countable many are available. Namely, one can show that the undecidable sentences which have been constructed here always become decidable through adjunction of suitable high types (e.g. of the type $\omega$ to the system $P$. A similar result also holds for the axiom systems of set theory. (Go31, p.28, footnote 48a)

The explicit thesis of this foundational paper is that the above interpretation is an instance of a cover up’—in Feynman’s sense—which appears to be a post-facto imposition that, first, continues to echo in and misleadingly [1] influence standard expositions of Gödel’s reasoning when applied to a first-order Peano Arithmetic, PA, and, second, that it obscures the larger significance of the genesis of Gödel’s reasoning.

As Gödel’s various remarks in Go31 suggest, this possibly lay in efforts made at the dawn of the twentieth century—largely as a result of Brouwer’s objections (Br08)—to define unambiguously the role that the universal and existential quantifiers played in formal mathematical reasoning.

That this issue is critical to Gödel’s reasoning in Go31, but remains unresolved in it, is obscured by his powerful presentation and interpretation.

So, to grasp the underlying mathematical significance of Gödel’s reasoning, and of what he has actually achieved, one may need to avoid focusing (as detailed in the previous posts on A foundational perspective on the semantic and logical paradoxes; in this post on undecidable Gödelian propositions, and in this preprint on undecidable Gödelian propositions):

$\bullet$ on the analogy of the so-called Liar paradox’;

$\bullet$ on Gödel’s interpretation of his arithmetical proposition as asserting its own formal unprovability in his formal Peano Arithmetic P (Go31, pp.9-13);

$\bullet$ on his interpretation of the reasons for the incompleteness’ of P; and

$\bullet$ on his assessment and interpretation of the formal consequences of such incompleteness’.

We show in this paper that, when applied to PA [2], all of these obscure the deeper significance of what Gödel actually achieved in Go31.

C: Hilbert: If the $\omega$-Rule is true, can P be completed?

Instead, Gödel’s reasoning may need to be located specifically in the context of Hilbert’s Program (cf. Hi30, pp.485-494) in which he proposed an $\omega$-rule as a finitary means of extending a Peano Arithmetic—such as his formal system P in Go31—to a possible completion (i.e. to logically showing that, given any arithmetical proposition, either the proposition, or its negation, is formally provable from the axioms and rules of inference of the extended Arithmetic).

Hilbert’s $\omega$-Rule: If it is proved that the P-formula [$F(x)$] interprets as a true numerical formula for each given P-numeral [$x$], then the P-formula $[(\forall x)F(x)]$ may be admitted as an initial formula (axiom) in P.

It is likely that Gödel’s 1931 paper evolved out of attempts to prove Hilbert’s $\omega$-rule in the limited—and more precise—sense that if a formula [$F(n)$] is provable in P for each given numeral [$n$], then the formula [$(\forall x)F(x)$] must be provable in P.

Now, if we meta-assume Hilbert’s $\omega$-rule for P, then it follows that, if P is consistent, then there is no P-formula [$F(x)$] for which, first, [$\neg(\forall x)F(x)$] is P-provable and, second, [$F(n)$] is P-provable for any given P-numeral [$n$].

Gödel defined a consistent Peano Arithmetic with the above property as additionally $\omega$-consistent (Go31, pp.23-24).

D: The significance of $\omega$-consistency

To place the significance of $\omega$-consistency in a current perspective, we note that the standard model of the first order Peano Arithmetic PA (cf. Me64, p.107; Sc67, p.23, p.209; BBJ03, p.104) presumes [3] that the standard interpretation M of PA (under which the PA-formula [$(\exists x)R(x)$], which is merely an abbreviation for $[\neg(\forall x)\neg R(x)]$, interprets as true if, and only if, $R(n)$ holds for some natural number $n$ under M) is sound (cf. BBJ03, p.174).

Clearly, if such an interpretation of the existential quantifier is sound, it immediately implies that PA is necessarily $\omega$-consistent [4].

Since Brouwer’s main objection was to Hilbert’s presumption that such an interpretation of the existential quantifier is sound, Gödel explicitly avoided this assumption in his seminal 1931 paper (Go31, p.9) in order to ensure that his reasoning was acceptable as “constructive” and “intuitionistically unobjectionable” (Go31, p.26).

He chose, instead, to present the formal undecidability of his arithmetical proposition—and the consequences arising from it—as explicitly conditional on the assumption of the formal property of $\omega$-consistency for his Peano Arithmetic P under the unqualified—and, as we show below, mistaken—belief that:

PA is $\omega$-consistent (Go31, p.28, footnote 48a).

E: Gödel: If the $\omega$-Rule is true, P cannot be completed

Now, Gödel’s significant achievement in Go31 was the discovery that, if P is consistent, then it was possible to construct a P-formula, [$R(x)$] [5], such that $[R(n)]$ is P-provable for any given P-numeral [$n$] (Go31, p.25(2)), but [$(\forall x)R(x)$] is P-unprovable (Go31, p.25(1)).

However, it becomes apparent from his remarks in Go31 that Gödel considered his more significant achievement the further argument that, if P is assumed $\omega$-consistent, then both [$(\forall x)R(x)$] and [$\neg (\forall x)R(x)$] [6] are P-unprovable, and so P is incomplete!

This is the substance of Gödel’s Theorem VI (Go31, p.24).

Although this Theorem neither validated nor invalidated Hilbert’s $\omega$-rule, it did imply that assuming the rule led not to the completion of a Peano Arithmetic as desired by Hilbert, but to its essential incompletability!

F: The $\omega$-Rule is inconsistent with PA

Now, apparently, the possibility neither considered by Gödel in 1931, nor seriously since, is that a formal sytem of Peano Arithmetic—such as PA—may be consistent and $\omega$inconsistent.

If so, one would ascribe this omission to the cover up’ factor mentioned by Feynman, since a significant consequence of Gödel’s reasoning—in the first half of his proof of his Theorem VI—is that it actually establishes PA as $\omega$inconsistent (as detailed in Corollary 9 of this preprint and Corollary 4 of this post).

In other words, we can logically show for Gödel’s formula [$R(x)$] that [$\neg(\forall x)$ $R(x)$] is PA-provable, and that [$R(n)$] is PA-provable for any given PA-numeral [$n$].

Consequently, Gödel’s Theorem VI is vacuously true for PA, and it also follows that Hilbert’s $\omega$-Rule is inconsistent with PA!

G: Need: A paradigm shift in interpreting the quantifiers

Thus Gödel’s unqualified belief that:

PA is $\omega$-consistent

was misplaced, and Brouwer’s objection to Hilbert’s presumption—that the above interpretation of the existential quantifier is sound—was justified; since, if PA is consistent, then it is provably $\omega$inconsistent, from which it follows that the standard interpretation M of PA is not sound.

Hence we can no longer interpret [$\neg(\forall x)F(x)$] is true’ maximally under the standard interpretation of PA as:

(i) The arithmetical relation $F(n)$ is not always [7] true.

However, since the theorems of PA—when treated as Boolean functions—are Turing-computable as always true under a sound finitary interpretation $\beta$ of PA, we can interpret [$\neg(\forall x)F(x)$] is true’ minimally as:

(ii) The arithmetical relation $F(n)$ is not Turing-computable as always true.

This interpretation allows us to conclude from Gödel’s meta-mathematical argument that we can construct a PA-formula [$(\forall x)R(x)$] that is unprovable in PA, but which is true under a sound interpretation of PA [8] although we may now no longer conclude from Gödel’s reasoning that there is an undecidable arithmetical PA-proposition.

Moreover, the interpretation admits an affirmative answer to Hilbert’s query: Is PA complete or completeable?

H: PA is algorithmically complete

In outline, the basis from which this conclusion follows formally is that:

(i) Gödel’s proof of the essential incompleteness of any formal system of Peano Arithmetic (Go31, Theorem VI, p.24) explicitly assumes that the arithmetic is $\omega$-consistent;

(ii) Rosser’s extension of Gödel’s proof of the essential incompleteness of any formal system of Peano Arithmetic (cf. Ro36, Theorem II, p.233) implicitly presumes that the Arithmetic is $\omega$-consistent (as detailed in this post);

(iii) PA is $\omega$inconsistent (as detailed in Corollary 9 of this preprint);

(iv) The classical standard’ interpretation of PA (cf. Me64, section \S 2, pp.49-53; p107) over the structure [$N$]—defined as {$N$ (the set of natural numbers); $=$ (equality); $'$ (the successor function); $+$ (the addition function); $\ast$ (the product function); $0$ (the null element)}— does not define a finitary model of PA (as detailed in the paper titled Evidence-Based Interpretations of PA presented at IACAP/AISB Turing 2012, Birmingham, UK in July 2012);

(v) We can define a sound interpretation $\beta$ of PA—in terms of Turing-computability—which yields a finitary model of PA, but which does not admit a non-standard model for PA (as detailed in this paper);

(vi) PA is algorithmically complete in the sense that an arithmetical proposition $F$ defines a Turing-machine TM$_{F}$ which computes $F$ as true under $\beta$ if, and only if, the corresponding PA-formula [$F$] is PA-provable (as detailed in Section 8 of this preprint).

I: Gödel’s proof of his Theorem XI does not withstand scrutiny

Since Gödel’s proof of his Theorem XI (Go31, p.36)—in which he claims to show that the consistency of his formal system of Peano Arithmetic P can be expressed as a P-formula which is not provable in P—appeals critically to his Theorem VI, it follows that this proof cannot be applied to PA.

However, we show below that there are other, significant, reasons why Gödel’s reasoning in this proof must be treated as classically objectionable per se.

J: Why Gödel’s interpretation of the significance of his Theorem XI is classically objectionable

Now, in his Theorem XI, Gödel constructs a formula [$W$] [9] in P and assumes that [$W$] translates—under a sound interpretation of P—as an arithmetical proposition that is true if, and only if, a specified formula of P is unprovable in P.

Now, if there were such a P-formula, then, since an inconsistent system necessarily proves every well-formed formula of the system, it would follow that a proof sequence within P proves that P is consistent.

However, Gödel shows that his formula [$W$] is not P-provable (Go31, p.37).

He concludes that the consistency of any formal system of Peano Arithmetic is not provable within the Arithmetic. [10]

K: Defining meta-propositions of P arithmetically

Specifically, Gödel first shows how 46 meta-propositions of P can be defined by means of primitive recursive functions and relations (Go31, pp.17-22).

These include:

($\#23$) A primitive recursive relation, Form($x$), which is true if, and only if, $x$ is the Gödel-number of a formula of P;

($\#45$) A primitive recursive relation, $xBy$, which is true if, and only if, $x$ is the Gödel-number of a proof sequence of P whose last formula has the Gödel-number $y$.

Gödel assures the constructive nature of the first 45 definitions by specifying (cf. Go31, p.17, footnote 34):

Everywhere in the following definitions where one of the expressions $\forall x$‘, $\exists x$‘, $\epsilon x$ (There is a unique $x$)’ occurs it is followed by a bound for $x$. This bound serves only to assure the recursive nature of the defined concept.

Gödel then defines a meta-mathematical proposition that is not recursive:

($\#46$) A proposition, $Bew(x)$, which is true if, and only if, $(\exists y)yBx$ is true.

Thus $Bew(x)$ is true if, and only if, $x$ is the Gödel-number of a provable formula of P.

L: Expressing arithmetical functions and relations in P

Now, by Gödel’s Theorem VII (Go31, p.29), any recursive relation, say $Q(x)$, can be represented in P by some, corresponding, arithmetical formula, say [$R(x)$], such that, for any natural number $n$:

If $Q(n)$ is true, then [$R(n)$] is P-provable;

If $Q(n)$ is false, then [$\neg R(n)$] is P-provable.

However, Gödel’s reasoning in the first half of his Theorem VI (Go31, p.25(1)) establishes that the above representation does not extend to the closure of a recursive relation, in the sense that we cannot assume:

If $(\forall x)Q(x)$ is true (i.e, $Q(n)$ is true for any given natural number), then $[(\forall x)R(x)]$ is P-provable.

In other words, we cannot assume that, even though the recursive relation $Q(x)$ is instantiationally equivalent to a sound interpretation of the P-formula [$R(x)$], the number-theoretic proposition $(\forall x)Q(x)$ must, necessarily, be logically equivalent to the—correspondingly sound—interpretation of the P-formula [$(\forall x)R(x)$].

The reason: In recursive arithmetic, the expression $(\exists x)F(x)$‘ is an abbreviation for the assertion:

(*) There is some (at least one) natural number $n$ such that $F(n)$ holds.

In a formal Peano Arithmetic, however, the formula [$(\exists x)F(x)$]’ is simply an abbreviation for [$\neg (\forall x)\neg F(x)$]’, which, under a sound finitary interpretation of the Arithmetic can have the verifiable translation:

(**) The relation $\neg F(x)$ is not Turing-computable as always true.

Moreover, Gödel’s Theorem VI establishes that we cannot conclude (*) from (**) without risking inconsistency.

Consequently, although a primitive recursive relation may be instantiationally equivalent to a sound interpretation of a P-formula, we cannot assume that the existential closure of the relation must have the same meaning as the interpretation of the existential closure of the corresponding P-formula.

However this, precisely, is the presumption made by Gödel in the proof of Theorem XI, from which he concludes that the consistency of P can be expressed in P, but is not P-provable.

M: Ambiguity in the interpreted meaning’ of formal mathematical expressions

The ambiguity in the meaning’ of formal mathematical expressions containing unrestricted universal and existential closure under an interpretation was emphasised by Wittgenstein (Wi56):

Do I understand the proposition “There is . . .” when I have no possibility of finding where it exists? And in so far as what I can do with the proposition is the criterion of understanding it … it is not clear in advance whether and to what extent I understand it.

N: Expressing “P is consistent” arithmetically

Specifically, Gödel defines the notion of “P is consistent” classically as follows:

P is consistent if, and only if, Wid(P) is true

where Wid(P) is defined as:

$( \exists x) (Form(x) \wedge \neg Bew(x))$

This translates as:

There is a natural number $n$ which is the Gödel-number of a formula of P, and this formula is not P-provable.

Thus, Wid(P) is true if, and only if, P is consistent.

O: Gödel: “P is consistent” is always expressible in P

However, Gödel, then, presumes that:

(i) Wid(P) can be represented by some formula [$W$] of P such that “[$W$] is true” and “Wid(P) is true” are logically equivalent (i.e., have the same meaning) under a sound interpretation of P;

(ii) if the recursive relation, $Q(x, p)$ (1931, p24(8.1)), is represented by the P-formula [$R(x, p)$], then the proposition “[$(\forall x)R(x, p)$] is true” is logically equivalent to (i.e., has the same meaning as) “$(\forall x)Q(x, p)$ is true” under a sound interpretation of P.

P: The loophole in Gödel’s presumption

Although, (ii), for instance, does follow if “[$(\forall x)R(x, p)$] is true” translates as “$R(x, p)$ is Turing-computable as always true”, it does not if “[$(\forall x)R(x, p)$] is true” translates as “$R(x, p)$ is constructively computable as true for any given natural number $n$, but it is not Turing-computable as true for any given natural number $n$“.

So, if [$W$], too, interprets as an arithmetical proposition that is constructively computable as true, but not Turing-computable as true, then the consistency of P may be provable instantiationally in P [11].

Hence, at best, Gödel’s reasoning can only be taken to establish that the consistency of P is not provable algorithmically in P.

Gödel’s broader conclusion only follows if P purports to prove its own consistency algorithmically.

However, Gödel’s particular argument, based on his definition of Wid(P), does not support this claim.

Bibliography

BBJ03 George S. Boolos, John P. Burgess, Richard C. Jeffrey. 2003. Computability and Logic (4th ed). Cambridge University Press, Cambridge.

Br08 L. E. J. Brouwer. 1908. The Unreliability of the Logical Principles. English translation in A. Heyting, Ed. L. E. J. Brouwer: Collected Works 1: Philosophy and Foundations of Mathematics. Amsterdam: North Holland / New York: American Elsevier (1975): pp. 107-111.

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.

Hi27 David Hilbert. 1927. The Foundations of Mathematics. In The Emergence of Logical Empiricism. 1996. Garland Publishing Inc.

Hi30 David Hilbert. 1930. Die Grundlegung der elementaren Zahlenlehre. Mathematische Annalen. Vol. 104 (1930), pp. 485-494.

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

Ro36 J. Barkley Rosser. 1936. Extensions of some Theorems of Gödel and Church. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York. Reprinted from The Journal of Symbolic Logic. Vol.1. pp.87-91.

Sc67 Joseph R. Schoenfield. 1967. Mathematical Logic. Reprinted 2001. A. K. Peters Ltd., Massachusetts.

Tu36 Alan Turing. 1936. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, ser. 2. vol. 42 (1936-7), pp.230-265; corrections, Ibid, vol 43 (1937) pp. 544-546.

Wi56 Ludwig Wittgenstein. 1956. Remarks on the Foundations of Mathematics. Edited by G. H. von Wright and R. Rhees. Translated by G. E. M. Anscombe. Basil Blackwell, Oxford.

Notes

Return to *: Edited and transcribed from this 2010 preprint. Some of its pedantic conclusions regarding the soundness’ of the standard interpretation of PA (and consequences thereof) should, however, be treated as qualified by the broader philosophical perspective that treats the standard and algorithmic interpretations of PA as complementary—rather than contradictory—interpretations (as detailed in this post).

Return to 1: We show in this paper that, from a finitary perspective (such as that of this preprint) the proofs of both of Gödel’s celebrated theorems in Go31—his Theorem VI postulating the existence of an undecidable proposition in his formal Peano Arithmetic, P, and his Theorem XI postulating that the consistency of P can be expressed, but not proven, within P—hold vacuously for first order Peano Arithmetic, PA.

Return to 2: Although we have restricted ourselves in this paper to considering only PA, the arguments would—prima facie—apply equally to any first-order theory that contains sufficient Peano Arithmetic in Gödel’s sense (cf. Go31, p.28(2)), by which we mean that every primitive recursive relation is definable within the theory in the sense of Gödel’s Theorems V (Go31, p.22) and VII (Go31, p.29).

Return to 4: Since we cannot, then, have that $[\neg(\forall x)\neg R(x)]$ is PA-provable and that $[\neg R(n)]$ is also PA-provable for any given numeral $[n]$.

Return to 5: This corresponds to the P-formula of his paper that Gödel defines, and refers to, only by its Gödel-number $r$ (cf. Go31, p.25, eqn.(12)).

Return to 6: Gödel refers to these P-formulas only by their Gödel-numbers $17Gen \hspace{+.5ex} r$ and $Neg(17Gen \hspace{+.5ex} r)$ respectively (cf. Go31, p.25, eqn.13).

Return to 7: i.e., for any given natural number $n$.

Return to 8: Because the arithmetical relation $R(x)$ is a Halting-type of relation (cf.Tu36, $\S 8$) that is constructively computable as true for any given natural number $n$, although it is not Turing-computable as true for any given natural number $n$ (as detailed in this post).

Return to 9: Gödel refers to it only by its Gödel-number $w$ (Go31, p.37).

Return to 10: Gödel’s broader conclusion—unchallenged so far but questionable—was that his reasoning could be validly “… carried over, word for word, to the axiom systems of set theory M and of classical mathematics A”.

Return to 11: That Gödel was open to such a possibility in 1931 is evidenced by his remark (Go31, p37) that “… it is conceivable that there might be finitary proofs which cannot be represented in P (or in M or A)”.

Author’s working archives & abstracts of investigations

Preamble

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

I call it the $PvNP$ Separation Problem.

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

Verifiability: A number-theoretical formula $F(x)$ is verifiable under an interpretation (and should by intent be defined in $NP$) if, and only if, for any given natural number $n$, there is a deterministic algorithm $AL_{(F,\ n)}$ which can provide objective evidence for deciding the value of each formula in the finite sequence $\{F(1), F(2), \ldots, F(n)\}$.

Decidability: A number theoretical formula $F(x)$ is decidable under an interpretation (and should by intent be defined in $P$) if, and only if, there is a deterministic algorithm $AL_{F}$ that can provide objective evidence for deciding the value of each formula in the denumerable sequence $\{F(1), F(2), \ldots\}$.

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 $P$ and $NP$ 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 $F(x)$ is verifiable under an interpretation (and is defined in $NP$) if, and only if, for any given natural number $n$, there is a deterministic polynomial-time algorithm $AL_{(F,\ n)}$ which can provide objective evidence for deciding the value of each formula in the finite sequence $\{F(1), F(2), \ldots, F(n)\}$.

Decidability (standard): A number theoretical formula $F(x)$ is decidable under an interpretation (and is defined in $P$) if, and only if, there is a deterministic polynomial-time algorithm $AL_{F}$ that can provide objective evidence for deciding the value of each formula in the denumerable sequence $\{F(1), F(2), \ldots\}.$

The following argument attempts to view the consequence for the $PvNP$ problem if we separate the two classes $P$ and $NP$ 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 $PA$ 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 $P$ and $NP$ 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 $P$ and $NP$ 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 $P$ and $NP$ can also be defined qualitatively, and need not be expressed only in terms of computational complexity.

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

Introduction

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

Thus the problem Satisfiability is: Given a propositional formula $F$, determine whether $F$ is satisfiable. To show that this is in $NP$ we define the polynomial-time checking relation $R(x, y)$, which holds iff $x$ codes a propositional formula $F$ and $y$ codes a truth assignment to the variables of $F$ which makes $F$ 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 $P$ and $NP$ 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 $F$ is algorithmically verifiable under an interpretation (and should therefore be defined in $NP$) if, and only if, we can define a checking relation $R(x, y)$[2]—where $x$ codes a propositional formula $F$ and $y$ codes a truth assignment to the variables of $F$—such that, for any given natural number values $(m, n)$, there is a deterministic algorithm which will finitarily decide whether or not $R(m, n)$ holds over the domain $\mathbb{N}$ of the natural numbers.

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

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

In other words, standard interpretations of the classes $P$ and $NP$ 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 $P$ and $NP$ 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 $P$ and $NP$ is also qualitative, and cannot be adequately expressed in terms of only computational complexity.

The $PvNP$ 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 $PvNP$ Separation Problem in arithmetic:

Non-standard $PvNP\ (NS)$: Is there an arithmetical formula $F$ that is algorithmically verifiable but not algorithmically computable?

We shall first show how Gödel’s $\beta$-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 $F(x)$ is algorithmically verifiable under an interpretation if, and only if, for any given natural number $n$, there is a deterministic algorithm $AL_{(F,\ n)}$ which can provide objective evidence[5] for deciding the value of each formula in the finite sequence $\{F(1), F(2), \ldots, F(n)\}$.

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 $\mathbb{N}$ of the natural numbers if, and only if, they are algorithmically verifiable under the interpretation.[9]

Definition 2: A number theoretical formula $F(x)$ is algorithmically computable under an interpretation if, and only if, there is a deterministic algorithm $AL_{F}$ that can provide objective evidence for deciding the value of each formula in the denumerable sequence $\{F(1), F(2), \ldots\}$.

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 $\mathbb{N}$ 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 $r(n)$ denote the $n^{th}$ digit in the decimal expression $\sum_{i=1}^{\infty}r(i).10^{-i}$ of a putatively given real number $\mathbb{R}$ in the interval $0 < \mathbb{R} \leq 1$.

By the definition of the real number $\mathbb{R}$ as the limit of the Cauchy sequence of rationals $\{\sum_{i=1}^{k}r(i).10^{-i}: k = 1, 2, \ldots\}$, it follows that $r(n)$ 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. $\Box$

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 $\beta$-function

We note next that Gödel’s $\beta$-function is the primitive recursive number-theoretic function defined by[16]:

Definition 3: $\beta (x_{1}, x_{2}, x_{3}) = rm(1+(x_{3}+ 1) \star x_{2}, x_{1})$, where $rm(x_{1}, x_{2})$ denotes the remainder obtained on dividing $x_{2}$ by $x_{1}$.

We also note that:

Lemma 2: For any non-terminating sequence of values $f(0), f(1), \ldots$, we can construct natural numbers $b_{k},\ c_{k}$ such that:

(i) $j_{k} = max(k, f(0), f(1), \ldots, f(k))$;

(ii) $c_{k} = j_{k}$!;

(iii) $\beta(b_{k}, c_{k}, i) = f(i)$ for $0 \leq i \leq k$.

Proof: This is a standard result[17]. $\Box$

Now we have the standard definition[18]:

Definition 4: A number-theoretic function $f(x_{1}, \ldots, x_{n})$ is said to be representable in the first order Peano Arithmetic PA if, and only if, there is a PA formula $[F(x_{1}, \dots, x_{n+1})]$[19] with the free variables $[x_{1}, \ldots, x_{n+1}]$, such that, for any given natural numbers $k_{1}, \ldots, k_{n+1}$:

(i) if $f(k_{1}, \ldots, k_{n}) = k_{n+1}$ then PA proves: $[F(k_{1}, \ldots, k_{n}, k_{n+1})]$;

(ii) PA proves: $[(\exists_{1} x_{n+1})F(k_{1}, \ldots, k_{n}, x_{n+1})]$.

The function $f(x_{1}, \ldots, x_{n})$ is said to be strongly representable in PA if we further have that:

(iii) PA proves: $[(\exists_{1} x_{n+1})F(x_{1}, \ldots, x_{n}, x_{n+1})]$

We also have that:

Lemma 3: $\beta(x_{1}, x_{2}, x_{3})$ is strongly represented in PA by $[Bt(x_{1}, x_{2}, x_{3}, x_{4})]$, which is defined as follows:

$[(\exists w)(x_{1} = ((1 + (x_{3} + 1)\star x_{2}) \star w + x_{4}) \wedge (x_{4} < 1 + (x_{3} + 1) \star x_{2}))]$.

Proof: This is a standard result[20]. $\Box$

An arithmetical perspective on the $PvNP$ 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 $\{r(n)\}$ be the denumerable sequence defined by the denumerable sequence of digits in the decimal expansion $\sum_{i=1}^{\infty}r(i).10^{-i}$ of a putatively given real number $\mathbb{R}$ in the interval $0 < \mathbb{R} \leq 1$.

By Lemma 2, for any given natural number $k$, there are natural numbers $b_{k}, c_{k}$ such that, for any $1 \leq n \leq k$:

$\beta(b_{k}, c_{k}, n) = r(n)$.

By Lemma 3, $\beta(x_{1}, x_{2}, x_{3})$ is strongly represented in PA by $[Bt(x_{1}, x_{2}, x_{3}, x_{4})]$ such that, for any $1 \leq n \leq k$:

If $\beta(b_{k}, c_{k}, n) = r(n)$ then PA proves $[Bt(b_{k}, c_{k}, n, r(n))]$.

We now define the arithmetical formula $[R(b_{k}, c_{k}, n)]$ for any $1 \leq n \leq k$ by:

$[R(b_{k}, c_{k}, n) = r(n)]$ if, and only if, PA proves $[Bt(b_{k}, c_{k}, n, r(n))]$.

Hence every putatively given real number $\mathbb{R}$ in the interval $0 < \mathbb{R} \leq 1$ uniquely corresponds to an algorithmically verifiable arithmetical formula $[R(x)]$ since:

For any $k$, the primitive recursivity of $\beta(b_{k}, c_{k}, n)$ yields a deterministic algorithm AL$_{(\beta, \mathbb{R}, k)}$ that can provide objective evidence for deciding the unique value of each formula in the finite sequence $\{[R(1), R(2), \ldots, R(k)]\}$ by evidencing the truth under a sound interpretation of PA for:

$[R(1) = R(b_{k}, c_{k}, 1)]$
$[R(b_{k}, c_{k}, 1) = r(1)]$

$[R(2) = R(b_{k}, c_{k}, 2)]$
$[R(b_{k}, c_{k}, 2) = r(2)]$

$[R(k) = R(b_{k}, c_{k}, k)]$
$[R(b_{k}, c_{k}, k) = r(k)]$.

The correspondence is unique because, if $\mathbb{R}$ and $\mathbb{S}$ are two different putatively given reals in the interval $0 < \mathbb{R},\ \mathbb{S} \leq 1$, then there is always some $m$ for which:

$r(m) \neq s(m)$.

Hence the corresponding arithmetical formulas $[R(n)]$ and $[S(n)]$ are such that:

$[R(n) = r(n)]$ for all $1 \leq n \leq m$.

$[S(n) = s(n)]$ for all $1 \leq n \leq m$.

$[R(m) \neq S(m)]$.

By Lemma 1, there is an algorithmically uncomputable real number $\mathbb{R}$ such that the corresponding PA formula $[(\exists y)(R(x) = y)]$ is also algorithmically uncomputable, but algorithmically verifiable, under a sound interpretation of PA.

The theorem follows. $\Box$

An arithmetical perspective on the $PvNP$ problem

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

Corollary 1: $NP \neq P\ (NS).$

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 $EPR$ 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 $\beta$-function to this distinction, see this post.

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 $F$ 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 $F$ 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 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 7: On the inductive assignment of satisfaction and truth values to the formulas of a formal language under an interpretation; Ta33.

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

Author’s working archives & abstracts of investigations

Use of square brackets

Unless otherwise obvious from the context, we use square brackets to indicate that the contents represent a symbol or a formula—of a formal theory—generally assumed to be well-formed unless otherwise indicated by the context.

In other words, expressions inside the square brackets are to be only viewed syntactically as juxtaposition of symbols that are to be formed and manipulated upon strictly in accordance with specific rules for such formation and manipulation—in the manner of a mechanical or electronic device—without any regards to what the symbolism might represent semantically under an interpretation that gives them meaning.

Use of an asterisk

Unless otherwise obvious from the context, we use an asterisk to indicate that the associated expression is to be interpreted semantically with respect to some well-defined interpretation.

We have taken some liberty in emphasising standard definitions selectively, and interspersing our arguments liberally with comments and references, generally of a foundational nature.

These are intended to reflect our underlying thesis that essentially arithmetical problems appear more natural when expressed—and viewed—within an arithmetical perspective of an interpretation of PA that appeals to the evidence provided by a deterministic algorithm.

Since a deterministic algorithm has only one possible move from a given configuration such a perspective, by its very nature, cannot appeal implicitly to transfinite concepts.

Evidence

“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 …”

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

Aristotle’s particularisation

This holds that from an assertion such as:

‘It is not the case that: For any given $x,\ P^{*}(x)$ does not hold’

usually denoted symbolically by ‘$\neg(\forall x)\neg P^{*}(x)$‘, we may always validly infer in the classical, Aristotlean, logic of predicates [1] that:

‘There exists an unspecified $x$ such that $P^{*}(x)$ holds’

usually denoted symbolically by ‘$(\exists x)P^{*}(x)$‘.

Aristotle’s particularisation (AP) is essentially the semantic postulation that from the negation of a universal we may always deduce the existence of a contrafactual. It is necessarily true over finite domains.

Expressed more formally:

Aristotle’s particularisation under an interpretation

If the formula $[\neg (\forall x) \neg F(x)]$ of a first order language $S$ interprets as true under a sound interpretation of $S$, then we may always conclude that there must be some object $s$ in the domain $D$ of the interpretation such that, if the formula $[F(x)]$ interprets as the unary relation $F^{*}(x)$ in $D$, then the proposition $F^{*}(s)$ is true under the interpretation.

The significance of Aristotle’s particularisation for the first-order predicate calculus

We note that in a formal language the formula ‘$[(\exists x)P(x)]$‘ is an abbreviation for the formula ‘$[\neg(\forall x)\neg P(x)]$‘.

The commonly accepted interpretation of this formula—and a fundamental tenet of classical logic unrestrictedly adopted as intuitively obvious by standard literature [2] that seeks to build upon the formal first-order predicate calculus—tacitly appeals to Aristotlean particularisation.

However, L. E. J. Brouwer had noted in his seminal 1908 paper on the unreliability of logical principles [3] that the commonly accepted interpretation of this formula is ambiguous if interpretation is intended over an infinite domain.

Brouwer essentially argued that, even supposing the formula ‘$[P(x)]$‘ of a formal Arithmetical language interprets as an arithmetical relation denoted by ‘$P^{*}(x)$‘, and the formula ‘$[\neg(\forall x)\neg P(x)]$‘ as the arithmetical proposition denoted by ‘$\neg(\forall x)\neg P^{*}(x)$‘, the formula ‘$[(\exists x)P(x)]$‘ need not interpret as the arithmetical proposition denoted by the usual abbreviation ‘$(\exists x)P^{*}(x)$‘; and that such postulation is invalid as a general logical principle in the absence of a means for constructing some putative object $a$ for which the proposition $P^{*}(a)$ holds in the domain of the interpretation.

Hence we shall follow the convention that the assumption that ‘$(\exists x)P^{*}(x)$‘ is the intended interpretation of the formula ‘$[(\exists x)P(x)]$‘—which is essentially the assumption that Aristotle’s particularisation holds over the domain of the interpretation—must always be explicit.

The significance of Aristotle’s particularisation for PA

In order to avoid intuitionistic objections to his reasoning, Kurt Gödel introduced the syntactic property of $\omega$-consistency [4] as an explicit assumption in his formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions [5].

Gödel explained at some length [6] that his reasons for introducing $\omega$-consistency explicitly was to avoid appealing to the semantic concept of classical arithmetical truth in Aristotle’s logic of predicates (which presumes Aristotle’s particularisation).

The two concepts are meta-mathematically equivalent in the sense that, if PA is consistent, then PA is $\omega$-consistent if, and only if, Aristotle’s particularisation holds under the standard interpretation of PA [7].

We note that Aristotle’s particularisation is a non-constructive—and logically fragile—semantic deduction rule. It is reflected in classical first order deduction either by some similarly non-constructive syntactic rule of natural deduction—such as Rosser’s Rule C [7.1]—or by the assumption that FOL is $\omega$-consistent.

The structure $\mathbb{N}$

The structure of the natural numbers—namely:

$N$ (the set of natural numbers);

$=$ (equality);

$S$ (the successor function);

$+$ (the addition function);

$\ast$ (the product function);

$0$ (the null element).

The axioms of the first-order Peano Arithmetic PA

$PA_{1}$: $[(x_{1} = x_{2}) \rightarrow ((x_{1} = x_{3}) \rightarrow (x_{2} = x_{3}))]$;

$PA_{2}$: $[(x_{1} = x_{2}) \rightarrow (x_{1}^{\prime} = x_{2}^{\prime})]$;

$PA_{3}$: $[0 \neq x_{1}^{\prime}]$;

$PA_{4}$: $[(x_{1}^{\prime} = x_{2}^{\prime}) \rightarrow (x_{1} = x_{2})]$;

$PA_{5}$: $[( x_{1} + 0) = x_{1}]$;

$PA_{6}$: $[(x_{1} + x_{2}^{\prime}) = (x_{1} + x_{2})^{\prime}]$;

$PA_{7}$: $[( x_{1} \star 0) = 0]$;

$PA_{8}$: $[( x_{1} \star x_{2}^{\prime}) = ((x_{1} \star x_{2}) + x_{1})]$;

$PA_{9}$: For any well-formed formula $[F(x)]$ of PA:

$[F(0) \rightarrow (((\forall x)(F(x) \rightarrow F(x^{\prime}))) \rightarrow (\forall x)F(x))]$.

Generalisation in PA

If $[A]$ is PA-provable, then so is $[(\forall x)A]$.

Modus Ponens in PA

If $[A]$ and $[A \rightarrow B]$ are PA-provable, then so is $[B]$.

The standard interpretation of PA

The standard interpretation $\mathcal{I}_{PA(\mathbb{N},\ Standard)}$ of PA over the structure $\mathbb{N}$ is the one in which the logical constants have their ‘usual’ interpretations [8] in Aristotle’s logic of predicates (which subsumes Aristotle’s particularisation), and [9]:

(a) the set of non-negative integers is the domain;

(b) the symbol $[0]$ interprets as the integer $0$;

(c) the symbol $[S]$ interprets as the successor operation (addition of $1$);

(d) the symbols $[+]$ and $[*]$ interpret as ordinary addition and multiplication;

(e) the symbol $[=]$ interprets as the identity relation.

Simple consistency

A formal system S is simply consistent if, and only if, there is no S-formula $[F(x)]$ for which both $[(\forall x)F(x)]$ and $[\neg(\forall x)F(x)]$ are S-provable.

$\omega$-consistency

A formal system S is $\omega$-consistent if, and only if, there is no S-formula $[F(x)]$ for which first $[\neg(\forall x)F(x)]$ is S-provable, and second $[F(a)]$ is S-provable for any given S-term $[a]$.

Soundness (formal system – non-standard)

A formal system S is sound under an interpretation $\mathcal{I}_{S}$ with respect to a domain $\mathbb{D}$ if, and only if, every theorem $[T]$ of S translates as ‘$[T]$ is true under $\mathcal{I}_{S}$ in $\mathbb{D}$‘.

Soundness (interpretation – non-standard)

An interpretation $\mathcal{I}_{S}$ of a formal system S is sound with respect to a domain $\mathbb{D}$ if, and only if, S is sound under the interpretation $\mathcal{I}_{S}$ over the domain $\mathbb{D}$.

Soundness in classical logic

In classical logic, a formal system $S$ is sometimes defined as ‘sound’ if, and only if, it has an interpretation; and an interpretation is defined as the assignment of meanings to the symbols, and truth-values to the sentences, of the formal system. Moreover, any such interpretation is defined as a model [10] of the formal system.

This definition suffers, however, from an implicit circularity: the formal logic $L$ underlying any interpretation of $S$ is implicitly assumed to be ‘sound’.

The above definitions seek to avoid this implicit circularity by delinking the defined ‘soundness’ of a formal system under an interpretation from the implicit ‘soundness’ of the formal logic underlying the interpretation.

This admits the case where, even if $L_{1}$ and $L_{2}$ are implicitly assumed to be sound, $S+L_{1}$ is sound, but $S+L_{2}$ is not.

Moreover, an interpretation of $S$ is now a model for $S$ if, and only if, it is sound.

Algorithmic verifiability

A number-theoretical relation $F(x)$ is algorithmically verifiable if, and only if, for any given natural number $n$, there is an algorithm $AL_{(F,\ n)}$ which can provide objective evidence for deciding the truth/falsity of each proposition in the finite sequence $\{F(1), F(2), \ldots, F(n)\}$.

Tarskian interpretation of an arithmetical language verifiably in terms of the computations of a simple functional language

We show in the Birmingham paper that 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; further, that the PA-formulas are decidable under the standard interpretation of PA over $\mathbb{N}$ if, and only if, they are algorithmically verifiable under the interpretation. [11]

Algorithmic computability

A number theoretical relation $F(x)$ is algorithmically computable if, and only if, there is an algorithm $AL_{F}$ that can provide objective evidence for deciding the truth/falsity of each proposition in the denumerable sequence $\{F(1), F(2), \ldots\}$.

Tarskian interpretation of an arithmetical language algorithmically in terms of the computations of a simple functional language

We show in the Birmingham paper that 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; further, that the PA-formulas are decidable under an algorithmic interpretation of PA over $\mathbb{N}$ if, and only if, they are algorithmically computable under the interpretation. [12]

Algorithmic verifiability vis à vis algorithmic computability

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

From the point of view of a finitary mathematical philosophy—which is the constraint within which an applied science ought to ideally operate—the significant difference between the two concepts could be expressed by saying that we may treat the decimal representation of a real number as corresponding to a physically measurable limit [14]—and not only to a mathematically definable limit—if and only if such representation is definable by an algorithmically computable function. [15]

We note that although every algorithmically computable relation is algorithmically verifiable, the converse is not true. [16]

References

Be59 Evert W. Beth. 1959. The Foundations of Mathematics. Studies in Logic and the Foundations of Mathematics. Edited by L. E. J. Brouwer, E. W. Beth, A. Heyting. 1959. North Holland Publishing Company, Amsterdam.

BBJ03 George S. Boolos, John P. Burgess, Richard C. Jeffrey. 2003. Computability and Logic. (4th ed). Cambridge University Press, Cambridge.

BF58 Paul Bernays and Abraham A. Fraenkel. 1958. Axiomatic Set Theory Studies in Logic and the Foundations of Mathematics. Edited by L. E. J. Brouwer, E. W. Beth, A. Heyting. 1959. North Holland Publishing Company, Amsterdam.

Br08 L. E. J. Brouwer. 1908. The Unreliability of the Logical Principles. English translation in A. Heyting, Ed. L. E. J. Brouwer: Collected Works 1: Philosophy and Foundations of Mathematics. Amsterdam: North Holland / New York: American Elsevier (1975): pp.107-111.

Co66 Paul J. Cohen. 1966. Set Theory and the Continuum Hypothesis. (Lecture notes given at Harvard University, Spring 1965) W. A. Benjamin, Inc., New York.

Da82 Martin Davis. 1958. Computability and Unsolvability. 1982 ed. Dover Publications, Inc., New York.

EC89 Richard L. Epstein, Walter A. Carnielli. 1989. Computability: Computable Functions, Logic, and the Foundations of Mathematics. Wadsworth & Brooks, California.

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. pp.5-38.

HA28 David Hilbert & Wilhelm Ackermann. 1928. Principles of Mathematical Logic. Translation of the second edition of the Grundzüge Der Theoretischen Logik> 1928. Springer, Berlin. 1950. Chelsea Publishing Company, New York.

Hi25 David Hilbert. 1925. On the Infinite. Text of an address delivered in Münster on 4th June 1925 at a meeting of the Westphalian Mathematical Society. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

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

Kn63 G. T. Kneebone. 1963. Mathematical Logic and the Foundations of Mathematics: An Introductory Survey. D. Van Norstrand Company Limited, London.

Li64 A. H. Lightstone. 1964. The Axiomatic Method. Prentice Hall, NJ.

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

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.

Nv64 P. S. Novikov. 1964. Elements of Mathematical Logic. Oliver & Boyd, Edinburgh and London.

Qu63 Willard Van Orman Quine. 1963. Set Theory and its Logic. Harvard University Press, Cambridge, Massachusette.

Rg87 Hartley Rogers Jr. 1987. Theory of Recursive Functions and Effective Computability. MIT Press, Cambridge, Massachusetts.

Ro53 J. Barkley Rosser. 1953. Logic for Mathematicians. McGraw Hill, New York.

Sh67 Joseph R. Shoenfield. 1967. Mathematical Logic. Reprinted 2001. A. K. Peters Ltd., Massachusetts.

Sk28 Thoralf Skolem. 1928. On Mathematical Logic. Text of a lecture delivered on 22nd October 1928 before the Norwegian Mathematical Association. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.

Sm92 Raymond M. Smullyan. 1992. Gödel’s Incompleteness Theorems. Oxford University Press, Inc., New York.

Su60 Patrick Suppes. 1960. Axiomatic Set Theory. Van Norstrand, Princeton.

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.

Wa63 Hao Wang. 1963. A survey of Mathematical Logic. North Holland Publishing Company, Amsterdam.

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 $EPR$ 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 2: Hi25, p.382; HA28, p.48; Sk28, p.515; Go31, p.32.; Kl52, p.169; Ro53, p.90; BF58, p.46; Be59, pp.178 & 218; Su60, p.3; Wa63, p.314-315; Qu63, pp.12-13; Kn63, p.60; Co66, p.4; Me64, p.52(ii); Nv64, p.92; Li64, p.33; Sh67, p.13; Da82, p.xxv; Rg87, p.xvii; EC89, p.174; Mu91; Sm92, p.18, Ex.3; BBJ03, p.102.

Return to 4: The significance of $\omega$-consistency for the formal system PA is highlighted in An12.

Return to 11: We show in An12 that the concept of Algorithmic verifiability is also well-defined under the standard interpretation of PA over $\mathbb{N}$.

Return to 12: We show in An12 that the concepts of Algorithmic verifiability and Algorithmic computability are both well-defined under the standard interpretation of PA over $\mathbb{N}$; moreover they identify distinctly different subsets of the well-defined PA formulas.

Return to 13: We note that the concept of ‘algorithmic computability’ is essentially an expression of the more rigorously defined concept of ‘realizability’ in Kl52, p.503.

Return to 14: In the sense of a physically ‘completable’ infinite sequence (as needed to resolve Zeno’s paradox).

Return to 16: See Appendix B of this preprint Is Gödel’s undecidable proposition an ‘ad hoc’ anomaly?.

Author’s working archives & abstracts of investigations