**Evidence-Based Interpretations of PA**

In July 2012 I presented a paper titled “Evidence-Based Interpretations of ” to the Symposium on Computational Philosophy at the AISB/IACAP World Congress 2012-Alan Turing 2012, held from to 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 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 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 formulas under any sound interpretation of 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 of does not address this issue, since it is silent on the methodology for such an assignment.

essentially asserts that, under Tarski’s inductive definitions of the satisfaction and truth of the formulas of under the interpretation, if there is a methodology for uniquely defining the satisfaction and truth of the *atomic* formulas of (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 mean that there is an assignment which provides objective evidence (o.e.) for . It seems breaks down in the general treatment of conditionals . In order to have , we need to have an assignment which, first of all decides whether and, if it verifies that, then verifies . But to decide whether we have to decide whether or not there is an assignment that provides o.e. for , and that can’t be done in general under in the absence of a methodology for assigning objective satisfaction and truth values to the atomic formulas of .

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 .

We then argued that if Tarski’s definitions are further accepted as inductively determining unique satisfaction and truth values for the *compound* formulas of , then we arrive at two interpretations of , say and .

We showed that is sound if, and only if, 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 is sound if, and only if, is -consistent; which illuminates Gödel’s undecidability Theorem (if is -consistent, it must have a formally undecidable proposition).

We then argued that the other interpretation is sound since the Axiom Schema of Finite Induction *is* justified finitarily under the interpretation.

However, what interpretation 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 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 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 of the first-order Peano Arithmetic PA ^{[3]} over the domain of the natural numbers:

(i) The atomic formulas of PA can be *assumed* as decidable under ;

(ii) The PA axioms can be *assumed* to interpret as satisfied/true under ;

(iii) the PA rules of inference—Generalisation and Modus Ponens—can be *assumed* to preserve such satisfaction/truth under .

**Standard interpretation of PA:** The standard interpretation of PA over the domain 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 interpret as ordinary addition and multiplication;

(e) the symbol interprets as the identity relation.

**The axioms of first-order Peano Arithmetic (PA)**

**PA** ;

**PA** ;

**PA** ;

**PA** ;

**PA** ;

**PA** ;

**PA** ;

**PA** ;

**PA** For any well-formed formula of PA:

.

**Generalisation in PA:** If is PA-provable, then so is .

**Modus Ponens in PA:** If and are PA-provable, then so is .

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 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 of PA over the domain of the PA *numerals*; and that this interpretation is sound if, and only if, PA is -consistent.

**Soundness (formal system):** We define a formal system S as sound under a Tarskian interpretation over a domain if, and only if, every theorem of S translates as ` is true under in ‘.

**Soundness (interpretation):** We define a Tarskian interpretation of a formal system S as sound over a domain if, and only if, S is sound under the interpretation over the domain .

**Simple consistency:** A formal system S is simply consistent if, and only if, there is no S-formula for which both and are S-provable.

**-consistency:** A formal system S is -consistent if, and only if, there is no S-formula for which, first, is S-provable and, second, is S-provable for any given S-term .

We further show that this interpretation can be viewed as a formalisation of the standard interpretation of PA over ; in the sense that—under Tarski’s definitions— is sound over if, and only if, is sound over (as postulated in (ii) and (iii) above).

Although the standard interpretation is *assumed* to be sound over (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 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 of PA over .

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

We conclude from the above that the interpretation is finitary, and hence sound over ^{[15]}.

We further conclude from the soundness of the interpretation over 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 , when this is explicitly defined as in Section 5.

We show, moreover, that we can further define `algorithmic truth’ and `algorithmic falsehood’ under such that the PA axioms interpret as always algorithmically true, and the rules of inference preserve algorithmic truth, over the domain of the natural numbers.

**2.1 The definitions of `algorithmic truth’ and `algorithmic falsehood’ under are not symmetric with respect to `truth’ and `falsehood’ under **

However, the definitions of `algorithmic truth’ and `algorithmic falsehood’ under are not symmetric with respect to classical (verifiable) `truth’ and `falsehood’ under .

For instance, if a formula of an arithmetic is algorithmically true under an interpretation (such as ), then we may conclude that there is an algorithm that, for any given numeral , provides evidence that the formula is algorithmically true under the interpretation.

In other words, there is an algorithm that provides evidence that the interpretation of *holds* in for any given natural number .

**Notation:** We use enclosing square brackets as in `‘ 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 `‘ to indicate the asterisked expression is to be treated as denoting the interpretation of the formula 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 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 , can provide evidence whether the interpretation holds or not in .

We cannot conclude that there is a numeral such that the formula is algorithmically false under the interpretation; nor can we conclude that there is a natural number such that does not hold in .

Such a conclusion would require:

(i) either some additional evidence that will verify for some assignment of numerical values to the free variables of that the corresponding interpretation 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 ) or, equivalently, that the arithmetic is -consistent ^{[23]}.

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

`It is not the case that: For any given , does not hold’,

usually denoted symbolically by `‘, we may always validly infer in the classical, Aristotlean, logic of predicates ^{[24]} that:

`There exists an unspecified such that holds’,

usually denoted symbolically by `‘.

**The significance of Aristotle’s particularisation for the first-order predicate calculus:** We note that in a formal language the formula `‘ is an abbreviation for the formula `‘. 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 `‘ of a formal Arithmetical language interprets as an arithmetical relation denoted by `‘, and the formula `‘ as the arithmetical proposition denoted by `‘, the formula `‘ need not interpret as the arithmetical proposition denoted by the usual abbreviation `‘; and that such postulation is invalid as a general logical principle in the absence of a means for constructing some putative object for which the proposition holds in the domain of the interpretation.

Hence we shall follow the convention that the assumption that `‘ is the intended interpretation of the formula `‘—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 -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 -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 -consistent if, and only if, Aristotle’s particularisation holds under the standard interpretation of PA over .

**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 is algorithmically verifiable as true under an interpretation if, and only if, for any given numeral , we can define an algorithm which provides evidence that 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 if, and only if, they are algorithmically verifiable under the interpretation (Corollary 2).

**Definition 2: Algorithmic computability:** An arithmetical formula is algorithmically computable as true under an interpretation if, and only if, we can define an algorithm that, for any given numeral , provides evidence that 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 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 .

**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 is an atomic formula of a formal language S, then the denumerable sequence in the domain of an interpretation of S satisfies if, and only if:

(i) interprets under as a unique relation in for any witness of ;

(ii) there is a Satisfaction Method, SM() that provides objective *evidence* ^{[30]} by which any witness of can objectively *define* for any atomic formula of S, and any given denumerable sequence of , whether the proposition holds or not in ;

(iii) holds in for any .

**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 is .

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 in terms of *only* the satisfiability of the atomic formulas of S over as usual ^{[31]}:

**Definition 4:** A denumerable sequence of satisfies under if, and only if, does not satisfy ;

**Definition 5:** A denumerable sequence of satisfies under if, and only if, either it is not the case that satisfies , or satisfies ;

**Definition 6:** A denumerable sequence of satisfies under if, and only if, given any denumerable sequence of which differs from in at most the ‘th component, satisfies ;

**Definition 7:** A well-formed formula of is true under if, and only if, given any denumerable sequence of , satisfies ;

**Definition 8:** A well-formed formula of is false under if, and only if, it is not the case that is true under .

It follows that ^{[32]}:

**Theorem 1:** (*Satisfaction Theorem*) If, for any interpretation of a first-order theory S, there is a Satisfaction Method SM() which holds for a witness of , then:

(i) The formulas of S are decidable as either true or false over under ;

(ii) If the formulas of S are decidable as either true or as false over under , then so are the formulas of S.

**Proof:** It follows from the above definitions that:

(a) If, for any given atomic formula of S, it is decidable by whether or not a given denumerable sequence of satisfies in under then, for any given compound formula of S containing any one of the logical constants , it is decidable by whether or not satisfies in under ;

(b) If, for any given compound formula of S containing of the logical constants , it is decidable by whether or not a given denumerable sequence of satisfies in under then, for any given compound formula of S containing of the logical constants , it is decidable by whether or not satisfies in under ;

We thus have that:

(c) The formulas of S are decidable by as either true or false over under ;

(d) If the formulas of S are decidable by as either true or as false over under , then so are the formulas of S.

In other words, if the atomic formulas of of S interpret under as decidable with respect to the Satisfaction Method SM() by a witness over some domain , then the propositions of S (i.e., the and formulas of S) also interpret as decidable with respect to SM() by the witness over .

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 of the natural numbers**

The standard interpretation of PA over the domain of the natural numbers is obtained if, in :

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

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

(c) for any atomic formula of PA and sequence of , we take SATCON() as:

holds in and, for any given sequence of , the proposition is decidable in ;

(d) we define the witness informally as the `mathematical intuition’ of a human intelligence for whom, classically, SATCON() has been *implicitly* accepted as *objectively* `decidable’ in ;

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

**Lemma 1:** is both algorithmically verifiable and algorithmically computable in by .

**Proof:** (i) It follows from the argument in Theorem 2 (below) that is algorithmically verifiable in by .

(ii) It follows from the argument in Theorem 3 (below) that is algorithmically computable in by . The lemma follows.

Now, although it is not immediately obvious from the standard interpretation of PA over which of (i) or (ii) may be taken for *explicitly* deciding SATCON() by the witness , 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 implicitly presumes (i).

(e) we postulate that Aristotle’s particularisation holds over ^{[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 extraneously non-finitary ^{[36]}.

We note further that if PA is –*in*consistent, then Aristotle’s particularisation does not hold over , and the interpretation is not sound over .

**4.2 An instantiational interpretation of PA over the domain of the PA numerals**

We next consider an instantiational interpretation of PA over the domain 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 as the set of PA numerals;

(c) for any atomic formula of PA and any sequence of PA numerals in , we take SATCON() as:

is provable in PA and, for any given sequence of numerals of PA, the formula is decidable as either provable or not provable in PA;

(d) we define the witness as the meta-theory of PA.

**Lemma 2:** is always algorithmically verifiable in PA by .

**Proof:** It follows from Gödel’s definition of the primitive recursive relation ^{[38]}—where is the Gödel number of a proof sequence in PA whose last term is the PA formula with Gödel-number —that, if is an atomic formula of PA, can algorithmically verify for any given sequence of PA numerals which one of the PA formulas and is necessarily PA-provable.

Now, if PA is consistent but not -consistent, then there is a Gödelian formula ^{[39]} such that:

(i) is not PA-provable;

(ii) is PA-provable;

(iii) for any given numeral , the formula is PA-provable.

However, if is sound over , then (ii) implies contradictorily that it is not the case that, for any given numeral , the formula is PA-provable.

It follows that if is sound over , then PA is -consistent and, ipso facto, Aristotle’s particularisation must hold over .

Moreover, if PA is consistent, then every PA-provable formula interprets as true under some sound interpretation of PA over . Hence can effectively decide whether, for any given sequence of natural numbers in , the proposition holds or not in .

It follows that can be viewed as a constructive formalisation of the `standard’ interpretation of PA in which we do not need to non-constructively assume that Aristotle’s particularisation holds over .

**4.3 An algorithmic interpretation of PA over the domain of the natural numbers**

We finally consider the purely algorithmic interpretation of PA over the domain of the natural numbers where:

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

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

(c) for any atomic formula of PA and any sequence of natural numbers in , we take SATCON() as:

holds in and, for any given sequence of , the proposition is decidable as either holding or not holding in ;

(d) we define the witness as any simple functional language that gives evidence that SATCON() is always *effectively* decidable in :

**Lemma 3:** is always algorithmically computable in by .

**Proof:** If is an atomic formula of PA then, for any given sequence of numerals , the PA formula is an atomic formula of the form , where and are atomic PA formulas that denote PA numerals. Since and are recursively defined formulas in the language of PA, it follows from a standard result ^{[40]} that, if PA is consistent, then is algorithmically computable as either true or false in . In other words, if PA is consistent, then is algorithmically computable (since there is an algorithm that, for any given sequence of numerals , will give evidence whether interprets as true or false in . The lemma follows.

It follows that is an algorithmic formulation of the `standard’ interpretation of PA over in which we do not extraneously assume either that Aristotle’s particularisation holds over or, equivalently, that PA is -consistent.

**5 Formally defining the standard interpretation of PA over 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 of PA *constructively* where:

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

(b) we define as ;

(c) we take SM() as any simple functional language.

We note that:

**Theorem 2:** The atomic formulas of PA are algorithmically verifiable under the standard interpretation .

**Proof:** If is an atomic formula of PA then, for any given denumerable sequence of numerals , the PA formula is an atomic formula of the form , where and are atomic PA formulas that denote PA numerals. Since and are recursively defined formulas in the language of PA, it follows from a standard result that, if PA is consistent, then interprets as the proposition which either holds or not for a witness in .

Hence, if PA is consistent, then is algorithmically verifiable since, for any given denumerable sequence of numerals , we can define an algorithm that provides evidence that the PA formula is decidable under the interpretation.

The theorem follows.

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 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 if, and only if, they are algorithmically verifiable under the interpretation.

**5.1 Defining `algorithmic truth’ under the standard interpretation of PA over **

Now we note that, in addition to Theorem 2:

**Theorem 3:** The atomic formulas of PA are algorithmically computable under the standard interpretation .

**Proof:** If is an atomic formula of PA then we can define an algorithm that, for any given denumerable sequence of numerals , provides evidence whether the PA formula is true or false under the interpretation.

The theorem follows.

This suggests the following definitions:

**Definition 9:** A well-formed formula of PA is algorithmically true under if, and only if, there is an algorithm which provides evidence that, given any denumerable sequence of , satisfies ;

**Definition 10:**A well-formed formula of PA is algorithmically false under if, and only if, it is not algorithmically true under .

**5.2 The PA axioms are algorithmically computable**

The significance of defining `algorithmic truth’ under as above is that:

**Lemma 4:** The PA axioms PA to PA are algorithmically computable as algorithmically true over under the interpretation .

**Proof:** Since , , , are defined recursively ^{[41]}, the PA axioms PA to PA 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.

**Lemma 5:** For any given PA formula , the Induction axiom schema interprets as algorithmically true under .

**Proof:** By Definitions 3 to 10:

(a) If interprets as algorithmically false under the lemma is proved.

Since interprets as algorithmically true if, and only if, either interprets as algorithmically false or interprets as algorithmically true.

(b) If interprets as algorithmically true and interprets as algorithmically false under , the lemma is proved.

(c) If and both interpret as algorithmically true under , then by Definition 9 there is an algorithm which, for any natural number , will give evidence that the formula is true under .

Since interprets as algorithmically true under , it follows that there is an algorithm which, for any natural number , will give evidence that the formula is true under the interpretation.

Hence is algorithmically true under .

Since the above cases are exhaustive, the lemma follows.

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

**Proof:** The two meta-assertions:

` interprets as algorithmically true under ^{[43]}‘

and

` interprets as algorithmically true under ‘

both mean:

is algorithmically computable as always true under .

It is also straightforward to see that:

Modus Ponens preserves algorithmic truth under .

We thus have that:

**Theorem 4:** The axioms of PA are always algorithmically true under the interpretation , and the rules of inference of PA preserve the properties of algorithmic satisfaction/truth under ^{[44]}.

**5.3 The interpretation of PA over is sound**

We conclude from Section 4.3 and Section 5.2 that there is an algorithmic interpretation of PA over such that:

**Theorem 5:** The interpretation of PA is sound over .

**Proof:** It follows immediately from Theorem 4 that the axioms of PA are always true under the interpretation , and the rules of inference of PA preserve the properties of satisfaction/truth under .

We thus have a finitary proof that:

**Theorem 6:** PA is consistent.

**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 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 in *two* essentially different ways.

*First* in terms of algorithmic verifiabilty. We show that this allows us to define a *formal instantiational* interpretation of PA over the domain of the PA numerals that is sound (i.e. PA theorems interpret as true in ) if, and only if, the standard interpretation of PA over —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 of PA over 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 2: As detailed in Section 4.

Return to 3: We take this to be the first-order theory S defined in Me64, p.102.

Return to 4: We essentially follow the definitions in Me64, p.49.

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 `[]’ of a formal language under an interpretation as `There exists an object in the domain of the interpretation such that ‘.

Return to 6: See Me64, p.107.

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 8: Section 3, Definition 1.

Return to 9: Section 3, Definition 2.

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 12: cf. Me64, p258.

Return to 13: See for instance http://en.wikipedia.org/wiki/Hilbert’s\_program.

Return to 14: Section 5.2, Theorem 4.

Return to 15: Section 5.3, Theorem 5.

Return to 16: Section 5.3, Theorem 6.

Return to 17: Formal definitions are given in Section 4.

Return to 18: Mu91.

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 20: Ta33.

Return to 21: As, for instance, in Go31.

Return to 22: Essentially reflecting Brouwer’s objection to the assumption of Aristotle’s particularisation over an infinite domain.

Return to 23: An assumption explicitly introduced by Gödel in Go31.

Return to 24: HA28, pp.58-59.

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 26: Br08.

Return to 27: Go31, p.23 and p.28.

Return to 28: In his introduction on p.9 of Go31.

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, 4.5) and uniformly continuous functions (Ru53, p.65, 4.13); or that between convergent sequences (Ru53, p.65, 7.1) and uniformly convergent sequences (Ru53, p.65, 7.7).}

Return to 30: cf. Me64, p.51.

Return to 31: In the sense of Mu91.

Return to 32: See Me64, p.51; Mu91.

Return to 33: cf. Me64, pp.51-53.

Return to 34: Where the string is defined as—and is to be treated as an abbreviation for—the string . We do not consider the case where the underlying logic is Hilbert’s formalisation of Aristotle’s logic of predicates in terms of his -operator (Hi27, pp.465-466).

Return to 35: Hence a PA formula such as interprets under as `There is some natural number such that holds in .

Return to 36: Br08.

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 38: Go31, p. 22(45).

Return to 39: Gödel constructively defines, and refers to, this formula by its Gödel number `‘: see Go31, p.25, Eqn.(12).

Return to 40: For any natural numbers , if , then PA proves (Me64, p.110, Proposition 3.6). The converse is obviously true.

Return to 41: cf. Go31, p.17.

Return to 42: See Hi27, p.472; also Br13, p.59; We27, p.482; Pa71, p.502-503.

Return to 43: See Definition 7.

Return to 44: Without appeal, moreover, to Aristotle’s particularisation.

## Leave a comment

Comments feed for this article