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.