You are currently browsing the tag archive for the ‘para-consistency’ tag.

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

In this post I address two critical issues, as raised in private correspondence with researchers, which may illuminate some objections to Gödel’s reasoning and conclusions that have been raised elsewhere by Wittgenstein, Floyd, Putnam et al.:

(i) By Rosser’s reasoning, doesn’t simple consistency suffice for defining an undecidable arithmetical proposition?

(ii) Doesn’t Gödel’s undecidable formula assert its own unprovability?

NOTE: The following correspondence refers copiously to *this paper* that was *presented* in June 2015 at the workshop on *Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics*, University of Montpellier, France.

Subsequently, most of the cited results were detailed formally in *the following paper* due to appear in the December 2016 issue of ‘*Cognitive Systems Research*‘:

**A: Doesn’t simple consistency suffice for defining Rosser’s undecidable arithmetical proposition?**

“*You claim that the PA system is -inconsistent, and that Gödel’s first theorem holds vacuously. But by Rosser’s result, simple consistency suffices.*“

Well, it does seem surprising that Rosser’s claim—that his ‘undecidable’ proposition only assumes simple consistency—has not been addressed more extensively in the literature. Number-theoretic expositions of Rosser’s proof have generally remained either implicit or sketchy (see, for instance, *this post*).

Note that Rosser’s proposition and reasoning involve interpretation of an existential quantifier, whilst Gödel’s proposition and reasoning only involve interpretation of a universal quantifier.

The reason why Rosser’s claim is untenable is that—in order to interpret the existential quantifier as per Hilbert’s -calculus—Rosser’s argument needs to assume his Rule C (see Elliott Mendelson, *Introduction to Mathematical Logic*, 1964 ed., p.73), which implicitly implies that Gödel’s arithmetic P—in which Rosser’s argumentation is grounded—is -consistent .

See, for instance, *this analysis* of (a) *Wang’s* outline of Rosser’s argument on p.5, (b) *Beth’s outline* of Rosser’s argument on p.6, and (c) *Mendelson’s exposition* of Rosser’s argument in Section 4.2 on p.8.

Moreover, the assumption is foundationally fragile, because Rule C invalidly assumes that we can introduce an ‘unspecified’ formula denoting an ‘unspecified’ numeral into PA even if the formula has not been demonstrated to be algorithmically definable in terms of the alphabet of PA.

See Theorem 8.5 and following remarks in Section 8, pp.7-8 of *this paper* that was *presented* in June 2015 at the workshop on *Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics*, University of Montpellier, France.

**B: As I see it, rule C is only a shortcut.**

“*As I see it, rule C is only a shortcut; it is totally eliminable. Moreover, it is part of predicate logic, not of the Peano’s arithmetic.*“

Assuming that Rule C is a short cut which can always be eliminated is illusory, and is tantamount to invalidly (see Corollary 8.6, p.17 of *the Epsilon 2015 paper*) claiming that Hilbert’s calculus is a conservative extension of the first-order predicate calculus.

*Reason*: Application of Rule C invalidly (see Theorem 8.5 and following remarks in Section 8, pp.7-8 of *the Epsilon 2015 paper*) involves introduction of a new individual constant, say , in a first-order theory (see Mendelson 1964, p.74, I(iv)); ‘invalidly’ since Rule C does not qualify that must be algorithmically computable from the alphabet of —which is necessary if is first-order.

Notation: We use square brackets to indicate that the expression within the brackets denotes a well-formed formula of a formal system, say , that is to be viewed syntactically merely as a first-order string of —i.e, one which is finitarily constructed from the alphabet of the language of —without any reference to its meaning under any interpretation of .

Essentially, Rule C mirrors in the intuitionistically objectionable postulation that the formula of can always be interpreted as:

holds for some element

in the domain of the interpretation of under which the formula interprets as the relation .

*The Epsilon 2015 paper* shows that this is not a valid interpretation of the formula under any finitary, evidence-based, interpretation of .

That, incidentally, is a consequence of the proof that PA is not -consistent; which itself is a consequence of (Theorem 7.1, p.15, of *the Epsilon 2015 paper*):

**Provability Theorem for PA**: A PA formula is provable if, and only if, interprets as an arithmetical relation that is algorithmically computable as always true (see Definition 3, p.7, of *the Epsilon 2015 paper*) over the structure of the natural numbers.

Compare with what Gödel has essentially shown in his famous 1931 paper on formally undecidable arithmetical propositions, which is that (Lemma 8.1, p.16, of *the Epsilon 2015 paper*):

**Gödel**: There is a PA formula —which Gödel refers to by its Gödel number —which is not provable in PA, even though interprets as an arithmetical relation that is algorithmically verifiable as always true (see Definition 4, p.7, of *the Epsilon 2015 paper*) over the structure of the natural numbers.

**C: If you by-pass the intuitionist objections, would all logicist and post-formalist theories hold?**

“*If I have understood correctly, you claim that the PA system is -inconsistent from an intuitionistic point of view? If you by-pass the intuitionist objections, would all logicist and post-formalist theories hold?*“

There is nothing to bypass—the first-order Peano Arithmetic PA is a formal axiomatic system which is -inconsistent as much for an intuitionist, as it is for a realist, a finitist, a formalist, a logicist or a nominalist.

Philosophers may differ about beliefs that are essentially unverifiable; but the -incompleteness of PA is a verifiable logical meta-theorem that none of them would dispute.

**D: Isn’t Gödel’s undecidable formula —which Gödel refers to by its Gödel number —self-referential?**

*Isn’t Gödel’s undecidable formula —which Gödel refers to by its Gödel number —self-referential and covertly paradoxical?*

*According to Wittgenstein it interprets in any model as a sentence that is devoid of sense, or even meaning. I think a good reason for this is that the formula is simply syntactically wrongly formed: the provability of provability is not defined and can not be consistently defined.*

*What you propose may be correct, but for automation systems of deduction wouldn’t -inconsistency be much more problematic than undecidability? *

*How would you feel if a syntax rule is proposed, that formulas containing numerals are instantiations of open formulas that may not be part of the canonical language? Too daring, may be?*

Let me briefly respond to the interesting points that you have raised.

1. The -inconsistency of PA is a meta-theorem; it is a Corollary of the Provability Theorem of PA (Theorem 7.1, p.15, of *the Epsilon 2015 paper*).

2. Gödel’s PA-formula is not an undecidable formula of PA. It is merely unprovable in PA.

3. Moreover, Gödel’s PA-formula is provable in PA, which is why the PA formula is not an undecidable formula of PA.

4. Gödel’s PA-formula is not self-referential.

5. Wittgenstein correctly believed—albeit purely on the basis of philosophical considerations unrelated to whether or not Gödel’s formal reasoning was correct—that Gödel was wrong in stating that the PA formula asserts its own unprovability in PA.

*Reason*: We have for Gödel’s primitive recursive relation that:

is true if, and only if, the PA formula is provable in PA.

However, in order to conclude that the PA formula asserts its own unprovability in PA, Gödel’s argument must further imply—which it does not—that:

is true (and so, by Gödel’s definition of , the PA formula is not provable in PA) if, and only if, the PA formula is provable in PA.

In other words, for the PA formula to assert its own unprovability in PA, Gödel must show—which his own argument shows is impossible, since the PA formula is not provable in PA—that:

The primitive recursive relation is algorithmically computable as always true if, and only if, the arithmetical relation is algorithmically computable as always true (where is the arithmetical interpretation of the PA formula over the structure of the natural numbers).

6. Hence, Gödel’s PA-formula is not covertly paradoxical.

7. **IF** Wittgenstein believed that the PA formula is empty of meaning and has no valid interpretation, then he was wrong, and—as Gödel justifiably believed—he could not have properly grasped Gödel’s formal reasoning that:

(i) ‘ is not -provable’ is a valid meta-theorem if PA is consistent, which means that:

‘If PA is consistent and we assume that the PA formula is provable in PA, then the PA formula must also be provable in PA; from which we may conclude that the PA formula is not provable in PA’

(ii) ‘ is not -provable’ is a valid meta-theorem ONLY if PA is -consistent, which means that:

‘If PA is -consistent and we assume that the PA formula is provable in PA, then the PA formula must also be provable in PA; from which we may conclude that the PA formula is not provable in PA’.

8. In fact the PA formula has the following TWO meaningful interpretations (the first of which is a true arithmetical meta-statement—since the PA formula is provable in PA for any PA-numeral —but the second is not—since the PA formula is not provable in PA):

(i) For any given natural number , there is an algorithm which will verify that each of the arithmetical meta-statements ‘ is true’, ‘ is true’, …, ‘ is true’ holds under the standard, algorithmically verifiable, interpretation of PA (see \S 5, p.11 of *the Epsilon 2015 paper*);

(ii) There is an algorithm which will verify that, for any given natural number , the arithmetical statement ‘ is true’ holds under the finitary, algorithmically computable, interpretation of PA (see \S 6, p.13 of *the Epsilon 2015 paper*).

9. **IF** Wittgenstein believed that the PA formula is not a well-defined PA formula, then he was wrong.

Gödel’s definition of the PA formula yields a well-formed formula in PA, and cannot be treated as ‘syntactically wrongly formed’.

10. The Provability Theorem for PA shows that both ‘proving something in PA’ and ‘proving that something is provable in PA’ are finitarily well-defined meta-mathematical concepts.

11. The Provability Theorem for PA implies that PA is complete with respect to the concepts of satisfaction, truth and provability definable in automated deduction systems, which can only define algorithmically computable truth.

12. The Provability Theorem for PA implies that PA is categorical, so you can introduce your proposed syntax rule ONLY if it leads to a conservative extension of PA.

13. Whether ‘daring’ or not, why would you want to introduce such a rule?

**E: Consider these two statements of yours …**

*Consider these two statements of yours:*

*“(iv): is the Gödel-number of the formula of PA” and*

*“D(4): Gödel’s PA-formula is not self-referential.”*

*If ‘‘ is the Gödel-number of the open formula in para (iv), and the second argument of the closed formula in para D(4) is ‘‘, then the second formula is obtained by instantiating the variable ‘‘ in the first with its own Gödel-number.*

*So how would you call, in one word, the relation between the entire formula (in D(4)) and its second argument?*

Para D(4) is an attempt to clarify precisely this point.

1. Apropos the first statement ‘(iv)’ cited by you:

From a pedantic perspective, the “relation between the entire formula (in D(4)) and its second argument” cannot be termed self-referential because the “second argument”, i.e., , is the Gödel-number of the PA formula , and not that of “the entire formula (in 4)”, i.e., of the formula itself (whose Gödel number is ).

Putting it crudely, is neither self-referential—nor circularly defined—because it is not defined in terms of , but in terms of .

2. Apropos the second statement ‘D(4)’ cited by you:

I would interpret:

Gödel’s PA-formula is self-referential

to mean, in this particular context, that—as Gödel wrongly claimed:

asserts its own unprovability in PA.

Now, if we were to accept the claim that is self-referential in the above sense, then (as various critics of Gödel’s reasoning have pointed out) we would have to conclude further that Gödel’s argument leads to the contradiction:

is true—and so, by Gödel’s definition of —the PA formula is not provable in PA—if, and only if, the PA formula is provable in PA.

However, in view of the Provability Theorem of PA (Theorem 7.1, p.15, of *the Epsilon 2015 paper*), this contradiction would only follow if Gödel’s argument were to establish (which it does not) that:

The primitive recursive relation is algorithmically computable as always true if, and only if, the arithmetical interpretation of the PA formula is algorithmically computable as always true over the structure of the natural numbers.

The reason Gödel cannot claim to have established the above is that his argument only proves the much weaker meta-statement:

The arithmetical interpretation of the PA formula is algorithmically verifiable as always true over the structure of the natural numbers.

Ergo—contrary to Gödel’s claim— Gödel’s PA-formula is not self-referential (and so, even though Gödel’s claimed interpretation of what his own reasoning proves is wrong, there is no paradox in Gödel’s reasoning per se)!

**F: Is the PA system -inconsistent without remedy?**

*Is the PA system -inconsistent without remedy? Is it possible to introduce a new axiom or new rule which by-passes the problematic unprovable statements of the Gödel-Rosser Theorems?*

1. Please note that the first-order Peano Arithmetic PA is:

(i) consistent (Theorem 7.3, p.15, of *the Epsilon 2015 paper*); which means that for any PA-formula , we cannot have that both and are Theorems of PA;

(ii) complete (Theorem 7.1, p.15, of *the Epsilon 2015 paper*); which means that we cannot add an axiom to PA which is not a Theorem of PA without inviting inconsistency;

(iii) categorical (Theorem 7.2, p.15, of *the Epsilon 2015 paper*); which means that if is an interpretation of PA over a structure , and is an interpretation of PA over a structure , then and are identical and denote the structure of the natural numbers defined by Dedekind’s axioms; and so PA has no model which contains an element that is not a natural number (see Footnote 54, p.16, of *the Epsilon 2015 paper*).

2. What this means with respect to Gödel’s reasoning is that:

(i) PA has no undecidable propositions, which is why it is not -consistent (Corollary 8.4, p.16, of *the Epsilon 2015 paper*);

(ii) The Gödel formula is not provable in PA; but it is algorithmically verifiable as true (Corollary 8.3, p.16, of *the Epsilon 2015 paper*) under the algorithmically verifiable standard interpretation of PA (see Section 5, p.11, of *the Epsilon 2015 paper*) over the structure of the natural numbers;

(iii) The Gödel formula is not provable in PA; and it is algorithmically computable as false (Corollary 8.3, p.16, of *the Epsilon 2015 paper*) under the algorithmically computable finitary interpretation of PA (see Section 6, p.13, of *the Epsilon 2015 paper*) over the structure of the natural numbers;

(iv) The Gödel formula is provable in PA; and it is therefore also algorithmically verifiable as true under the algorithmically verifiable standard interpretation of PA over the structure of the natural numbers—which means that the logic by which the standard interpretation of PA assigns values of ‘satisfaction’ and ‘truth’ to the formulas of PA (under Tarski’s definitions) may be paraconsistent (see *http://plato.stanford.edu/entries/logic-paraconsistent*) since PA is consistent;

(v) The Gödel formula is provable in PA; and it is therefore algorithmically computable as true (Corollary 8.2, p.16, of *the Epsilon 2015 paper*) under the algorithmically computable finitary interpretation of PA over the structure of the natural numbers.

3. It also means that:

(a) The “Gödel-Rosser Theorem” is not a Theorem of PA;

(b) The “unprovable Gödel sentence” is not a “problematic statement”;

(c) The “PA system” does not require a “remedy” just because it is “-inconsistent”;

(d) No “new axiom or new rule” can “by-pass the unprovable sentence”.

4. Which raises the question:

Why do you see the “unprovable Gödel sentence” as a “problematic statement” that requires a “remedy” which must “by-pass the unprovable sentence”?

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

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

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

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

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

**Post-computationalist doctrine**

“It is by now folklore … that one can view the *values* of a simple functional language as specifying *evidence* for propositions in a constructive logic …” (cf. Mu91).

** Introduction**

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

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

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

.

Moreover, we shall argue that even though is algorithmically computable (Definition 2) as always true in the standard model (whence all of its instances are in ) we cannot conclude by the Compactness Theorem that:

is consistent and has a model which contains an `infinite’ integer ^{[4]}.

*Reason:* We shall argue that the condition in the above definition of requires, first of all, that we must be able to extend by the addition of a `relativised’ axiom (cf. Fe92; Me64, p.192) such as:

,

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

for all .

However, we shall further show that even this would not yield a model for since, by Theorem 1, we cannot introduce a `completed’ infinity such as into either or any model of !

** A post-computationalist doctrine**

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

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

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

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

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

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

** Standard arguments for non-standard models of PA**

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

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

(*ii*) If PA is consistent, then we obtain a non-standard model for PA which contains an `infinite’ integer by adding a constant to the language of PA and applying the Compactness Theorem to the theory **P**.

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

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

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

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

** Algorithmically verifiable formulas and algorithmically computable formulas**

We begin by distinguishing between:

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

The concept is well-defined in the sense that the `algorithmic verifiability’ of the formulas of a formal language which contain logical constants can be inductively defined under an interpretation in terms of the `algorithmic verifiability’ of the interpretations of the atomic formulas of the language (An12).

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

**Definition 2:** An atomic formula of PA is algorithmically computable under an interpretation if, and only if, there is an algorithm that can provide objective evidence for deciding the truth value of each formula in the denumerable sequence of PA formulas under the interpretation.

This concept too is well-defined in the sense that the `algorithmic computability’ of the formulas of a formal language which contain logical constants can also be inductively defined under an interpretation in terms of the `algorithmic computability’ of the interpretations of the atomic formulas of the language (An12).

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

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

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

**Proof:** Let denote the digit in the decimal expansion of a putatively given real number in the interval . By the definition of a real number as the limit of a Cauchy sequence of rationals, it follows that is an algorithmically verifiable number-theoretic function. Since every algorithmically computable real is countable (Tu36), Cantor’s diagonal argument (Kl52, pp.6-8) shows that there are real numbers that are not algorithmically computable. The Lemma follows.

** Making non-finitary assumptions explicit**

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

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

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

usually denoted symbolically by `‘, we may always validly infer in the classical, Aristotlean, logic of predicates (HA28, pp.58-59) that:

`There exists an unspecified such that holds’,

usually denoted symbolically by `‘.

** The significance of Aristotle’s particularisation for the first-order predicate calculus**

Now we note that in a formal language the formula `‘ is an abbreviation for the formula `‘; and that the commonly accepted interpretation of this formula tacitly appeals to Aristotlean particularisation.

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

Brouwer essentially argued that, even supposing the formula `‘ 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 ^{[18]} as an explicit assumption in his formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions (Go31, p.23 and p.28).

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

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

** The ambiguity in admitting an `infinite’ constant**

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

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

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

**P** n:

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

… BBJ03, p.306, Corollary 25.3.

** We cannot force PA to admit a transfinite ordinal**

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

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

**Proof:** Let [] denote the PA-formula:

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

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

Further, in every model of PA, if denotes the interpretation of []:

(a) is true;

(b) If is true, then is true.

Hence, by Gödel’s completeness theorem:

(c) PA proves ;

(d) PA proves .

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

Further, by Generalisation:

(e) PA proves ;

*Generalisation in PA:* [] follows from [].

Hence, by Induction:

(f) is provable in PA.

*Induction Axiom Schema of PA:* For any formula [] of PA:

[]

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

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

** Why we cannot force PA to admit a transfinite ordinal**

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

(*i*) []

yields the weaker PA theorem:

(*ii*) []

Now, if we interpret PA without relativisation in ZF ^{[23]}— i.e., numerals as finite ordinals, [] as [], etc.— then (*ii*) always translates in ZF as a theorem:

(*iii*) []

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

(*iv*) []

*Example:* Define [] as `[]’.

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

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

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

** Forcing PA to admit denumerable descending dense sequences**

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

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

** An argument for a non-standard model of PA**

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

1. Let (*the set of natural numbers*); (*equality*); (*the successor function*); (*the addition function*); (*the product function*); (*the null element*) be the structure that serves to define a model of PA, say .

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

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

4. Let be the countable set of all PA-formulas of the form , where the index is a natural number.

5. Let T be the union of and T[].

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

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

8. has an infinite descending sequence with respect to because it is a model of .

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

** Why the argument in is logically fragile**

However if—as claimed in above— is a model of T[] plus any finite set of members of , and the PA term is well-defined for any given natural number , then:

All PA-formulas of the form are PA-provable,

is a proper sub-set of the PA-provable formulas, and

T is identically T[].

*Reason:* The argument cannot be that some PA-formula of the form is true in , but not PA-provable, as this would imply that if PA is consistent then PA+ has a model other than ; in other words, it would presume that which is sought to be proved, namely that PA has a non-standard model ^{[28]}!

Consequently, the postulated model of T in by `Compactness’ is the model that defines T[]. However, has no infinite descending sequence with respect to , even though it is a model of .

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

** A formal argument for a non-standard model of PA**

The second is the more formal argument ^{[29]}:

“Let denote the complete -theory of the standard model, i.e. is the collection of all true -sentences. For each we let be the closed term of ; is just the constant symbol . We now expand our language by adding to it a new constant symbol , obtaining the new language , and consider the following -theory with axioms

(for each )

and

(for each )

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

for some , and clearly the -structure with domain and interpreted naturally, and interpreted by the integer , satisfies . Thus by the compactness theore is consistent and has a model . The first thing to note about is that

for all , and hence it contains an `infinite’ integer.”

** Why the argument in too is logically fragile**

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

Accordingly, from an arithmetical perspective we can only conclude by the Compactness Theorem that if is the -theory of the standard model (interpretation), then we may consistently add to it the following as an additional—not necessarily independent—axiom:

.

Moreover, even though is algorithmically computable as always true in the standard model—whence all instances of it are also therefore in —we cannot conclude by the Compactness Theorem that is consistent and has a model which contains an `infinite’ integer.

*Reason:* The condition `‘ in requires, first of all, that we must be able to extend by the addition of a `relativised’ axiom (cf. Fe92; Me64, p.192) such as:

,

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

for all .

However, even this would not yield a model for since, by Theorem 1, we cannot introduce a `completed’ infinity such as into any model of !

As the argument stands, it seeks to violate finitarity by adding a new constant to the language of PA that is not definable in and, ipso facto, adding an atomic formula to PA whose satisfaction under any interpretation of PA is not algorithmically verifiable!

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

Moreover, the postulation would be false if were categorical.

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

** Gödel’s argument for a non-standard model of PA**

We begin by considering the Gödelian formula ^{[30]} which is unprovable in PA if PA is consistent, even though the formula is provable in a consistent PA for any given PA numeral .

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

**Theorem 2:** If PA is consistent, then we may add the PA formula as an axiom to PA without inviting inconsistency.

**Theorem 3:** If PA is -consistent, then we may add the PA formula as an axiom to PA without inviting inconsistency.

Gödel concluded from this that:

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

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

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

** Why Gödel’s assumption is logically fragile**

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

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

(1) In terms of algorithmic verifiabilty (An12, ); and

(2) In terms of algorithmic computability (An12, ).

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

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

**(a) Any algorithmically verifiable model of PA is necessarily over **

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

However, such a putative model of PA over would not be finitary since, if the formula were to interpret as true in it, then we could only conclude that, for any numeral , there is an algorithm which will finitarily certify the formula as true under an algorithmically verifiable interpretation in .

We could not conclude that there is a single algorithm which, for any numeral , will finitarily certify the formula as true under the algorithmically verifiable interpretation in .

Consequently, the PA Axiom Schema of Finite Induction would not interpret as true finitarily under the algorithmically verifiable interpretation of PA over the domain of the PA numerals.

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

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

PA is necessarily -consistent;

Aristotle’s particularisation holds over ; and

The `standard’ interpretation of PA also defines a non-finitary model of PA over .

**(b) The algorithmically computable interpretation of PA is over **

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

The algorithmically computable model of PA is finitary since we can show that, if the formula interprets as true under it, then we may always conclude that there is a single algorithm which, for any numeral , will finitarily certify the formula as true in under the algorithmically computable interpretation.

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

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

PA is consistent (An12, , Theorem 6).

** Why we cannot conclude that PA is necessarily -consistent**

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

Now, if there is no algorithm that can provide such a truth certificate for the Gödelian formula in , then we would have by definition first that the PA formula is true in the model, and second by Gödel’s reasoning that the formula is true in the model for any given numeral . Hence Aristotle’s particularisation would not hold in the model.

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

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

**Conclusion**

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

**References**

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

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

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

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

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

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

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

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

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

**Go31** Kurt Gödel. 1931. *On formally undecidable propositions of Principia Mathematica and related systems I.* Translated by Elliott Mendelson. In M. Davis (ed.). 1965. *The Undecidable.* Raven Press, New York.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

**Tu36** Alan Turing. 1936. *On computable numbers, with an application to the Entscheidungsproblem* In M. Davis (ed.). 1965. *The Undecidable.* Raven Press, New York. Reprinted from the Proceedings of the London Mathematical Society, ser. 2. vol. 42 (1936-7), pp.230-265; corrections, Ibid, vol 43 (1937) pp. 544-546.

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

**An12** Bhupinder Singh Anand. 2012. *Evidence-Based Interpretations of PA.* In Proceedings of the Symposium on Computational Philosophy at the AISB/IACAP World Congress 2012-Alan Turing 2012, 2-6 July 2012, University of Birmingham, Birmingham, UK.

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

**Notes**

Return to 1: By which we mean arguments such as in Ka91 (see pg.1), where the meta-theory is taken to be a set-theory such as ZF or ZFC, and the logical consistency of the meta-theory is not considered relevant to the argumentation.

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

Return to 3: eg. Ka91; Bo00; BBJ03,\ ch.25,\ p.302; Ko06; Ka11.

Return to 4: As argued in Ka91, p.10-11.

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

Return to 6: An12, Corollary 2; `non-finitary’ because the Axiom Schema of Finite Induction *cannot* be finitarily verified as true under the standard interpretation of PA with respect to `truth’ as defined by the algorithmically verifiable formulas of PA.

Return to 7: eg., BBJ03, p.155, Lemma 13.3 (Model existence lemma).

Return to 8: cf. The standard non-constructive set-theoretical assignment-by-postulation **(S5)** of the satisfaction properties **(S1)** to **(S8)** in BBJ03, p.153, Lemma 13.1 (Satisfaction properties lemma), which appeals critically to Aristotle’s particularisation.

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

Return to 10: In his seminal 1931 paper Go31, Kurt Gödel defines, and refers to, the formula corresponding to only by its `Gödel’ number (op. cit., p.25, Eqn.(12)), and to the formula corresponding to only by its `Gödel’ number .

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

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

Return to 13: However, as noted earlier, the Axiom Schema of Finite Induction *cannot* be finitarily verified as true under the standard interpretation of PA with respect to `truth’ as defined by the algorithmically verifiable formulas of PA .

Return to 14: In this case however, the Axiom Schema of Finite Induction *can* be finitarily verified as true under the standard interpretation of PA with respect to `truth’ as defined by the algorithmically computable formulas of PA (An12, Theorem 4).

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

Return to 16: We note that algorithmic computability implies the existence of an algorithm that can decide the truth/falsity of each proposition in a well-defined denumerable sequence of propositions, whereas algorithmic verifiability does not imply the existence of an algorithm that can decide the truth/falsity of each proposition in a well-defined denumerable sequence of propositions. From the point of view of a finitary mathematical philosophy, the significant difference between the two concepts could be expressed (An13) by saying that we may treat the decimal representation of a real number as corresponding to a physically measurable limit—and not only to a mathematically definable limit—if and only if such representation is definable by an algorithmically computable function.

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

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

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

Return to 20: For details see An12.

Return to 21: cf. HP98, p.13, ; Me64, p.112, Ex. 2.

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

Return to 23: In the sense indicated by Feferman Fe92.

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

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

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

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

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

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

Return to 30: In his seminal 1931 paper Go31, Kurt Gödel defines, and refers to, the formula corresponding to only by its `Gödel’ number (op. cit., p.25, Eqn.(12)), and to the formula corresponding to only by its `Gödel’ number .

Return to 31: Go31, p.25(1) & p.25(2).

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

*See also (i) this later publication by Sebastian Grève, where he concludes that “… while Gödel indeed showed some significant understanding of Wittgenstein here, ultimately, Wittgenstein perhaps understood Gödel better than Gödel understood himself”; and (ii) this note on Rosser’s Rule C and Wittgenstein’s objections on purely philosophical considerations to Gödel’s reasoning and conclusions, where we show that, although not at all obvious (perhaps due to Gödel’s overpoweringly plausible presentation of his interpretation of his own formal reasoning over the years) what Gödel claimed to have proven is not—as suspected and held by Wittgenstein—supported by Gödel’s formal argumentation.*

**A: Misunderstanding Gödel’s Theorems VI and XI: Incompleteness and Undecidability**

In an informal essay, “*Misunderstanding Gödel’s Theorems VI and XI: Incompleteness and Undecidability*“, DPhil candidate Sebastian Grève at The Queen’s College, Oxford, attempts to come to terms with what he subjectively considers:

*“… has not been properly addressed as such by philosophers hitherto as of great philosophical importance in our understanding of Gödel’s Incompleteness Theorems.”*

Grève’s is an unusual iconoclastic perspective:

*“This essay is an open enquiry towards a better understanding of the philosophical significance of Gödel’s two most famous theorems. I proceed by a discussion of several common misunderstandings, led by the following four questions:*

*1) Is the Gödel sentence true?*

*2) Is the Gödel sentence undecidable?*

*3) Is the Gödel sentence a statement?*

*4) Is the Gödel sentence a sentence?*

*Asking these questions in this order means to trace back the steps of Gödel’s basic philosophical interpretation of his formal results. What I call the basic philosophical interpretation is usually just taken for granted by philosopher’s writing about Gödel’s theorems.”*

In a footnote Grève acknowledges Wittgenstein’s influence by suggesting that:

*“This essay can be read as something like a free-floating interpretation of the theme of Wittgenstein’s remarks on Gödel’s Incompleteness Theorems in Wittgenstein: 1978[RFM], I-(III), partly following Floyd: 1995 but especially Kienzler: 2008, and constituting a reply to inter alia Rodych: 2003”.*

**B: Why we may see the trees, but not the forest**

We note that Grève’s four points are both overdue and well-made:

1. *Is the Gödel sentence true?*

Grève’s objection that standard interpretations are obscure when they hold the Gödel sentence as being intuitively true deserves consideration (see this post).

The ‘truth’ of the sentence should and does—as Wittgenstein stressed and suggested—follow objectively from the axioms and rules of inference of arithmetic.

2. *Is the Gödel sentence undecidable?*

Grève’s observation that the ‘undecidability’ of the Gödel sentence conceals a philosophically questionable assumption is well-founded.

The undecidability in question follows only on the assumption of ‘-consistency’ made explicitly by Gödel.

This assumption is actually logically equivalent to the philosophically questionable assertion that from the provability of we may conclude the existence of some numeral for which is provable.

Since Rosser’s proof implicitly makes this assumption by means of his logically questionable Rule C, his claim of avoiding omega-consistency for arithmetic is illusory.

3. *Is the Gödel sentence a statement?*

Grève rightly holds that the Gödel sentence should be treated as a valid statement within the formal arithmetic S, since it is structurally defined as a well-formed formula of S.

4. *Is the Gödel sentence a sentence?*

Grève’s concern about whether the Gödel sentence of S is a valid arithmetical proposition under interpretation also seems to need serious philosophical consideration.

It can be argued (see the comment following the proof of Lemma 9 of this preprint) that the way the sentence is formally defined as the universal quantification of an instantiationally (but not algorithmically) defined arithmetical predicate does not yield an unequivocally defined arithmetical proposition in the usual sense under interpretation.

In this post ^{[*]} we shall not only echo Grève’s disquietitude, but argue further that Gödel’s interpretation and assessment of his own formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions is, essentially, a post-facto imposition that continues to influence standard expositions of Gödel’s reasoning misleadingly.

**Feynman’s cover-up factor**

Our thesis is influenced by physicist Richard P. Feynman, who started his 1965 Nobel Lecture with a penetrating observation:

*We have a habit in writing articles published in scientific journals to make the work as finished as possible, to cover up all the tracks, to not worry about the blind alleys or describe how you had the wrong idea first, and so on. So there isn’t any place to publish, in a dignified manner, what you actually did in order to get to do the work.*

That such `cover up’ may have unintended—and severely limiting—consequences on a discipline is suggested by Gödel’s interpretation, and assessment, of his own formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions (Go31).

Thus, in his informal preamble to the result that he intended to prove formally, Gödel wrote (cf. Go31, p.9):

*The analogy of this result with Richard’s antinomy is immediately evident; there is also a close relationship with the Liar Paradox … Thus we have a proposition before us which asserts its own unprovability.*

Further, interpreting the significance of his formal reasoning as having established the existence of a formally undecidable arithmetical proposition that is, however, decidable by meta-mathematical arguments, Gödel noted that:

*The precise analysis of this remarkable circumstance leads to surprising results concerning consistency proofs of formal systems … (Go31, p.9)*

*The true reason for the incompleteness which attaches to all formal systems of mathematics lies, as will be shown in Part II of this paper, in the fact that the formation of higher and higher types can be continued into the transfinite (c.f., D. Hilbert, `Über das Unendliche’, Math. Ann. 95, p. 184), while, in every formal system, only countable many are available. Namely, one can show that the undecidable sentences which have been constructed here always become decidable through adjunction of suitable high types (e.g. of the type to the system . A similar result also holds for the axiom systems of set theory. (Go31, p.28, footnote 48a)*

The explicit thesis of this foundational paper is that the above interpretation is an instance of a `cover up’—in Feynman’s sense—which appears to be a post-facto imposition that, first, continues to echo in and misleadingly ^{[1]} influence standard expositions of Gödel’s reasoning when applied to a first-order Peano Arithmetic, PA, and, second, that it obscures the larger significance of the genesis of Gödel’s reasoning.

As Gödel’s various remarks in Go31 suggest, this possibly lay in efforts made at the dawn of the twentieth century—largely as a result of Brouwer’s objections (Br08)—to define unambiguously the role that the universal and existential quantifiers played in formal mathematical reasoning.

That this issue is critical to Gödel’s reasoning in Go31, but remains unresolved in it, is obscured by his powerful presentation and interpretation.

So, to grasp the underlying mathematical significance of Gödel’s reasoning, and of what he has actually achieved, one may need to avoid focusing (as detailed in the previous posts on *A foundational perspective on the semantic and logical paradoxes*; in this post on undecidable Gödelian propositions, and in this preprint on undecidable Gödelian propositions):

on the analogy of the so-called `Liar paradox’;

on Gödel’s interpretation of his arithmetical proposition as asserting its own formal unprovability in his formal Peano Arithmetic P (Go31, pp.9-13);

on his interpretation of the reasons for the `incompleteness’ of P; and

on his assessment and interpretation of the formal consequences of such `incompleteness’.

We show in this paper that, when applied to PA ^{[2]}, all of these obscure the deeper significance of what Gödel actually achieved in Go31.

**C: Hilbert: If the -Rule is true, can P be completed?**

Instead, Gödel’s reasoning may need to be located specifically in the context of Hilbert’s Program (cf. Hi30, pp.485-494) in which he proposed an -rule as a finitary means of extending a Peano Arithmetic—such as his formal system P in Go31—to a possible completion (*i.e. to logically showing that, given any arithmetical proposition, either the proposition, or its negation, is formally provable from the axioms and rules of inference of the extended Arithmetic*).

*Hilbert’s -Rule:* If it is proved that the P-formula [] interprets as a true numerical formula for each given P-numeral [], then the P-formula may be admitted as an initial formula (*axiom*) in P.

It is likely that Gödel’s 1931 paper evolved out of attempts to prove Hilbert’s -rule in the limited—and more precise—sense that if a formula [] is provable in P for each given numeral [], then the formula [] must be provable in P.

Now, if we meta-assume Hilbert’s -rule for P, then it follows that, if P is consistent, then there is no P-formula [] for which, first, [] is P-provable and, second, [] is P-provable for any given P-numeral [].

Gödel defined a consistent Peano Arithmetic with the above property as additionally -consistent (Go31, pp.23-24).

**D: The significance of -consistency**

To place the significance of -consistency in a current perspective, we note that the standard model of the first order Peano Arithmetic PA (cf. Me64, p.107; Sc67, p.23, p.209; BBJ03, p.104) *presumes* ^{[3]} that the standard interpretation * M* of PA (under which the PA-formula [], which is merely an abbreviation for , interprets as true if, and only if, holds for some natural number under

*) is*

**M***sound*(cf. BBJ03, p.174).

Clearly, if such an interpretation of the existential quantifier is sound, it immediately implies that PA is necessarily -consistent ^{[4]}.

Since Brouwer’s main objection was to Hilbert’s presumption that such an interpretation of the existential quantifier is sound, Gödel explicitly avoided this assumption in his seminal 1931 paper (Go31, p.9) in order to ensure that his reasoning was acceptable as “constructive” and “intuitionistically unobjectionable” (Go31, p.26).

He chose, instead, to present the formal undecidability of his arithmetical proposition—and the consequences arising from it—as explicitly conditional on the assumption of the formal property of -consistency for his Peano Arithmetic P under the unqualified—and, as we show below, mistaken—belief that:

*PA is -consistent (Go31, p.28, footnote 48a).*

**E: Gödel: If the -Rule is true, P cannot be completed**

Now, Gödel’s significant achievement in Go31 was the discovery that, if P is consistent, then it was possible to construct a P-formula, [] ^{[5]}, such that is P-provable for any given P-numeral [] (Go31, p.25(2)), but [] is P-unprovable (Go31, p.25(1)).

However, it becomes apparent from his remarks in Go31 that Gödel considered his more significant achievement the further argument that, if P is assumed -consistent, then both [] and [] ^{[6]} are P-unprovable, and so P is incomplete!

This is the substance of Gödel’s Theorem VI (Go31, p.24).

Although this Theorem neither validated nor invalidated Hilbert’s -rule, it did imply that assuming the rule led not to the completion of a Peano Arithmetic as desired by Hilbert, but to its essential incompletability!

**F: The -Rule is inconsistent with PA**

Now, apparently, the possibility neither considered by Gödel in 1931, nor seriously since, is that a formal sytem of Peano Arithmetic—such as PA—may be consistent *and* –*in*consistent.

If so, one would ascribe this omission to the `cover up’ factor mentioned by Feynman, since a significant consequence of Gödel’s reasoning—in the first half of his proof of his Theorem VI—is that it actually establishes PA as –*in*consistent (as detailed in Corollary 9 of this preprint and Corollary 4 of this post).

In other words, we can logically show for Gödel’s formula [] that [ ] is PA-provable, and that [] is PA-provable for any given PA-numeral [].

Consequently, Gödel’s Theorem VI is vacuously true for PA, and it also follows that Hilbert’s -Rule is inconsistent with PA!

**G: Need: A paradigm shift in interpreting the quantifiers**

Thus Gödel’s unqualified belief that:

“*PA is -consistent*“

was misplaced, and Brouwer’s objection to Hilbert’s presumption—that the above interpretation of the existential quantifier is sound—was justified; since, if PA is consistent, then it is provably –*in*consistent, from which it follows that the standard interpretation * M* of PA is

*not*sound.

Hence we can no longer interpret `[] is true’ maximally under the standard interpretation of PA as:

(i) The arithmetical relation is not always ^{[7]} true.

However, since the theorems of PA—when treated as Boolean functions—are Turing-computable as always true under a *sound* finitary interpretation of PA, we *can* interpret `[] is true’ minimally as:

(ii) The arithmetical relation is not Turing-computable as always true.

This interpretation allows us to conclude from Gödel’s meta-mathematical argument that we can construct a PA-formula [] that is unprovable in PA, but which is true under a sound interpretation of PA ^{[8]} although we may now no longer conclude from Gödel’s reasoning that there is an undecidable arithmetical PA-proposition.

Moreover, the interpretation admits an affirmative answer to Hilbert’s query: Is PA complete or completeable?

**H: PA is algorithmically complete**

In outline, the basis from which this conclusion follows formally is that:

(i) Gödel’s proof of the essential incompleteness of any formal system of Peano Arithmetic (Go31, Theorem VI, p.24) *explicitly* assumes that the arithmetic is -consistent;

(ii) Rosser’s extension of Gödel’s proof of the essential incompleteness of any formal system of Peano Arithmetic (cf. Ro36, Theorem II, p.233) *implicitly* presumes that the Arithmetic is -consistent (as detailed in this post);

(iii) PA is –*in*consistent (as detailed in Corollary 9 of this preprint);

(iv) The classical `standard’ interpretation of PA (cf. Me64, section \S 2, pp.49-53; p107) over the structure []—defined as { (*the set of natural numbers*); (*equality*); (*the successor function*); (*the addition function*); (*the product function*); (*the null element*)}— does *not* define a finitary model of PA (as detailed in the paper titled *Evidence-Based Interpretations of PA* presented at IACAP/AISB Turing 2012, Birmingham, UK in July 2012);

(v) We can define a sound interpretation of PA—in terms of Turing-computability—which yields a finitary model of PA, but which does not admit a non-standard model for PA (as detailed in this paper);

(vi) PA is algorithmically complete in the sense that an arithmetical proposition defines a Turing-machine TM which computes as true under if, and only if, the corresponding PA-formula [] is PA-provable (as detailed in Section 8 of this preprint).

**I: Gödel’s proof of his Theorem XI does not withstand scrutiny**

Since Gödel’s proof of his Theorem XI (Go31, p.36)—in which he claims to show that the consistency of his formal system of Peano Arithmetic P can be expressed as a P-formula which is not provable in P—appeals critically to his Theorem VI, it follows that this proof cannot be applied to PA.

However, we show below that there are other, significant, reasons why Gödel’s reasoning in this proof must be treated as classically objectionable per se.

**J: Why Gödel’s interpretation of the significance of his Theorem XI is classically objectionable**

Now, in his Theorem XI, Gödel constructs a formula [] ^{[9]} in P and assumes that [] translates—under a sound interpretation of P—as an arithmetical proposition that is true if, and only if, a specified formula of P is unprovable in P.

Now, if there were such a P-formula, then, since an inconsistent system necessarily proves every well-formed formula of the system, it would follow that a proof sequence within P proves that P is consistent.

However, Gödel shows that his formula [] is not P-provable (Go31, p.37).

He concludes that the consistency of any formal system of Peano Arithmetic is not provable within the Arithmetic. ^{[10]}

**K: Defining meta-propositions of P arithmetically**

Specifically, Gödel first shows how 46 meta-propositions of P can be defined by means of primitive recursive functions and relations (Go31, pp.17-22).

These include:

() A primitive recursive relation, *Form*(), which is true if, and only if, is the Gödel-number of a formula of P;

() A primitive recursive relation, , which is true if, and only if, is the Gödel-number of a proof sequence of P whose last formula has the Gödel-number .

Gödel assures the constructive nature of the first 45 definitions by specifying (cf. Go31, p.17, footnote 34):

*Everywhere in the following definitions where one of the expressions `‘, `‘, ` (There is a unique )’ occurs it is followed by a bound for . This bound serves only to assure the recursive nature of the defined concept.*

Gödel then defines a meta-mathematical proposition that is not recursive:

() A proposition, , which is true if, and only if, is true.

Thus is true if, and only if, is the Gödel-number of a provable formula of P.

**L: Expressing arithmetical functions and relations in P**

Now, by Gödel’s Theorem VII (Go31, p.29), any recursive relation, say , can be represented in P by some, corresponding, arithmetical formula, say [], such that, for any natural number :

If is true, then [] is P-provable;

If is false, then [] is P-provable.

However, Gödel’s reasoning in the first half of his Theorem VI (Go31, p.25(1)) establishes that the above representation does not extend to the closure of a recursive relation, in the sense that we cannot assume:

If is true (i.e, is true for any given natural number), then is P-provable.

In other words, we cannot assume that, even though the recursive relation is instantiationally equivalent to a sound interpretation of the P-formula [], the number-theoretic proposition must, necessarily, be logically equivalent to the—correspondingly sound—interpretation of the P-formula [].

The reason: In recursive arithmetic, the expression `‘ is an abbreviation for the assertion:

(*) There is some (at least one) natural number such that holds.

In a formal Peano Arithmetic, however, the formula `[]’ is simply an abbreviation for `[]’, which, under a sound finitary interpretation of the Arithmetic can have the verifiable translation:

(**) The relation is not Turing-computable as always true.

Moreover, Gödel’s Theorem VI establishes that we cannot conclude (*) from (**) without risking inconsistency.

Consequently, although a primitive recursive relation may be instantiationally equivalent to a sound interpretation of a P-formula, we cannot assume that the existential closure of the relation must have the same meaning as the interpretation of the existential closure of the corresponding P-formula.

However this, precisely, is the presumption made by Gödel in the proof of Theorem XI, from which he concludes that the consistency of P can be expressed in P, but is not P-provable.

**M: Ambiguity in the interpreted `meaning’ of formal mathematical expressions**

The ambiguity in the `meaning’ of formal mathematical expressions containing unrestricted universal and existential closure under an interpretation was emphasised by Wittgenstein (Wi56):

*Do I understand the proposition “There is . . .” when I have no possibility of finding where it exists? And in so far as what I can do with the proposition is the criterion of understanding it … it is not clear in advance whether and to what extent I understand it.*

**N: Expressing “P is consistent” arithmetically**

Specifically, Gödel defines the notion of “P is consistent” classically as follows:

P is consistent if, and only if, *Wid*(P) is true

where *Wid*(P) is defined as:

This translates as:

There is a natural number which is the Gödel-number of a formula of P, and this formula is not P-provable.

Thus, *Wid*(P) is true if, and only if, P is consistent.

**O: Gödel: “P is consistent” is always expressible in P**

However, Gödel, then, presumes that:

(i) *Wid*(P) can be represented by some formula [] of P such that “[] is true” and “*Wid*(P) is true” are logically equivalent (i.e., have the same meaning) under a sound interpretation of P;

(ii) if the recursive relation, (1931, p24(8.1)), is represented by the P-formula [], then the proposition “[] is true” is logically equivalent to (i.e., has the same meaning as) “ is true” under a sound interpretation of P.

**P: The loophole in Gödel’s presumption**

Although, (ii), for instance, does follow if “[] is true” translates as “ is Turing-computable as always true”, it does not if “[] is true” translates as “ is constructively computable as true for any given natural number , but it is not Turing-computable as true for any given natural number “.

So, if [], too, interprets as an arithmetical proposition that is constructively computable as true, but not Turing-computable as true, then the consistency of P may be provable instantiationally in P ^{[11]}.

Hence, at best, Gödel’s reasoning can only be taken to establish that the consistency of P is not provable algorithmically in P.

Gödel’s broader conclusion only follows if P purports to prove its own consistency algorithmically.

However, Gödel’s particular argument, based on his definition of *Wid*(P), does not support this claim.

**Bibliography**

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

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

**Go31** Kurt Gödel. 1931. *On formally undecidable propositions of Principia Mathematica and related systems I.* Translated by Elliott Mendelson. In M. Davis (ed.). 1965. *The Undecidable.* Raven Press, New York.

**Hi27** David Hilbert. 1927. *The Foundations of Mathematics.* In *The Emergence of Logical Empiricism.* 1996. Garland Publishing Inc.

**Hi30** David Hilbert. 1930. *Die Grundlegung der elementaren Zahlenlehre.* Mathematische Annalen. Vol. 104 (1930), pp. 485-494.

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

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

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

**Tu36** Alan Turing. 1936. *On computable numbers, with an application to the Entscheidungsproblem.* Proceedings of the London Mathematical Society, ser. 2. vol. 42 (1936-7), pp.230-265; corrections, Ibid, vol 43 (1937) pp. 544-546.

**Wi56** Ludwig Wittgenstein. 1956. *Remarks on the Foundations of Mathematics.* Edited by G. H. von Wright and R. Rhees. Translated by G. E. M. Anscombe. Basil Blackwell, Oxford.

**Notes**

Return to *: Edited and transcribed from this 2010 preprint. Some of its pedantic conclusions regarding the `soundness’ of the standard interpretation of PA (and consequences thereof) should, however, be treated as qualified by the broader philosophical perspective that treats the standard and algorithmic interpretations of PA as complementary—rather than contradictory—interpretations (as detailed in this post).

Return to 1: We show in this paper that, from a finitary perspective (such as that of this preprint) the proofs of both of Gödel’s celebrated theorems in Go31—his Theorem VI postulating the existence of an undecidable proposition in his formal Peano Arithmetic, P, and his Theorem XI postulating that the consistency of P can be expressed, but not proven, within P—hold vacuously for first order Peano Arithmetic, PA.

Return to 2: Although we have restricted ourselves in this paper to considering only PA, the arguments would—prima facie—apply equally to any first-order theory that contains sufficient Peano Arithmetic in Gödel’s sense (cf. Go31, p.28(2)), by which we mean that every primitive recursive relation is definable within the theory in the sense of Gödel’s Theorems V (Go31, p.22) and VII (Go31, p.29).

Return to 3: Following Hilbert.

Return to 4: Since we cannot, then, have that is PA-provable and that is also PA-provable for any given numeral .

Return to 5: This corresponds to the P-formula of his paper that Gödel defines, and refers to, only by its Gödel-number (cf. Go31, p.25, eqn.(12)).

Return to 6: Gödel refers to these P-formulas only by their Gödel-numbers and respectively (cf. Go31, p.25, eqn.13).

Return to 7: i.e., for any given natural number .

Return to 8: Because the arithmetical relation is a Halting-type of relation (cf.Tu36, ) that is constructively computable as true for any given natural number , although it is not Turing-computable as true for any given natural number (as detailed in this post).

Return to 9: Gödel refers to it only by its Gödel-number (Go31, p.37).

Return to 10: Gödel’s broader conclusion—unchallenged so far but questionable—was that his reasoning could be validly “… carried over, word for word, to the axiom systems of set theory M and of classical mathematics A”.

Return to 11: That Gödel was open to such a possibility in 1931 is evidenced by his remark (Go31, p37) that “… it is conceivable that there might be finitary proofs which cannot be represented in P (or in M or A)”.

**Use of square brackets**

Unless otherwise obvious from the context, we use square brackets to indicate that the contents represent a symbol or a formula—of a formal theory—generally assumed to be well-formed unless otherwise indicated by the context.

In other words, expressions inside the square brackets are to be only viewed syntactically as juxtaposition of symbols that are to be formed and manipulated upon strictly in accordance with specific rules for such formation and manipulation—in the manner of a mechanical or electronic device—without any regards to what the symbolism might represent semantically under an interpretation that gives them meaning.

**Use of an asterisk**

Unless otherwise obvious from the context, we use an asterisk to indicate that the associated expression is to be interpreted semantically with respect to some well-defined interpretation.

**Explanatory comments**

We have taken some liberty in emphasising standard definitions selectively, and interspersing our arguments liberally with comments and references, generally of a foundational nature.

These are intended to reflect our underlying thesis that essentially arithmetical problems appear more natural when expressed—and viewed—within an arithmetical perspective of an interpretation of PA that appeals to the evidence provided by a deterministic algorithm.

Since a deterministic algorithm has only one possible move from a given configuration such a perspective, by its very nature, cannot appeal implicitly to transfinite concepts.

**Evidence**

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

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

**Aristotle’s particularisation**

This holds that from an assertion such as:

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

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

‘There exists an unspecified such that holds’

usually denoted symbolically by ‘‘.

Aristotle’s particularisation (AP) is essentially the semantic postulation that from the negation of a universal we may always deduce the existence of a contrafactual. It is necessarily true over finite domains.

Expressed more formally:

**Aristotle’s particularisation under an interpretation**

If the formula of a first order language interprets as true under a sound interpretation of , then we may always conclude that there must be some object in the domain of the interpretation such that, if the formula interprets as the unary relation in , then the proposition is true under the interpretation.

**The significance of Aristotle’s particularisation for the first-order predicate calculus**

We note that in a formal language the formula ‘‘ 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 ^{[2]} that seeks to build upon the formal first-order predicate calculus—tacitly appeals to Aristotlean particularisation.

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

Brouwer essentially argued that, even supposing the formula ‘‘ 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 ^{[4]} as an explicit assumption in his formal reasoning in his seminal 1931 paper on formally undecidable arithmetical propositions ^{[5]}.

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

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

We note that Aristotle’s particularisation is a non-constructive—and logically fragile—semantic deduction rule. It is reflected in classical first order deduction either by some similarly non-constructive syntactic rule of natural deduction—such as Rosser’s *Rule C* ^{[7.1]}—or by the assumption that FOL is -consistent.

**The structure **

The structure of the natural numbers—namely:

(*the set of natural numbers*);

(*equality*);

(*the successor function*);

(*the addition function*);

(*the product function*);

(*the null element*).

**The axioms of the first-order Peano Arithmetic 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 .

**The standard interpretation of PA**

The standard interpretation of PA over the structure is the one in which the logical constants have their ‘usual’ interpretations ^{[8]} in Aristotle’s logic of predicates (which subsumes Aristotle’s particularisation), and ^{[9]}:

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

(b) the symbol interprets as the integer ;

(c) the symbol interprets as the successor operation (addition of );

(d) the symbols and interpret as ordinary addition and multiplication;

(e) the symbol interprets as the identity relation.

**Simple consistency**

A formal system S is simply consistent if, and only if, there is no S-formula 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 .

**Soundness (formal system – non-standard)**

A formal system S is sound under an interpretation with respect to a domain if, and only if, every theorem of S translates as ‘ is true under in ‘.

**Soundness (interpretation – non-standard)**

An interpretation of a formal system S is sound with respect to a domain if, and only if, S is sound under the interpretation over the domain .

**Soundness in classical logic**

In classical logic, a formal system is sometimes defined as ‘sound’ if, and only if, it has an interpretation; and an interpretation is defined as the assignment of meanings to the symbols, and truth-values to the sentences, of the formal system. Moreover, any such interpretation is defined as a model ^{[10]} of the formal system.

This definition suffers, however, from an implicit circularity: the formal logic underlying any interpretation of is implicitly assumed to be ‘sound’.

The above definitions seek to avoid this implicit circularity by delinking the defined ‘soundness’ of a formal system under an interpretation from the implicit ‘soundness’ of the formal logic underlying the interpretation.

This admits the case where, even if and are implicitly assumed to be sound, is sound, but is not.

Moreover, an interpretation of is now a model for if, and only if, it is sound.

**Algorithmic verifiability**

A number-theoretical relation is algorithmically verifiable if, and only if, for any given natural number , there is an algorithm which can provide objective evidence for deciding the truth/falsity of each proposition in the finite sequence .

**Tarskian interpretation of an arithmetical language verifiably in terms of the computations of a simple functional language**

We show in the Birmingham paper that the ‘algorithmic verifiability’ of the formulas of a formal language which contain logical constants can be inductively defined under an interpretation in terms of the ‘algorithmic verifiability’ of the interpretations of the atomic formulas of the language; further, that the PA-formulas are decidable under the standard interpretation of PA over if, and only if, they are algorithmically verifiable under the interpretation. ^{[11]}

**Algorithmic computability**

A number theoretical relation is algorithmically computable if, and only if, there is an algorithm that can provide objective evidence for deciding the truth/falsity of each proposition in the denumerable sequence .

**Tarskian interpretation of an arithmetical language algorithmically in terms of the computations of a simple functional language**

We show in the Birmingham paper that the ‘algorithmic computability’ of the formulas of a formal language which contain logical constants can also be inductively defined under an interpretation in terms of the ‘algorithmic computability’ of the interpretations of the atomic formulas of the language; further, that the PA-formulas are decidable under an algorithmic interpretation of PA over if, and only if, they are algorithmically computable under the interpretation. ^{[12]}

**Algorithmic verifiability vis à vis algorithmic computability**

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

From the point of view of a finitary mathematical philosophy—which is the constraint within which an applied science ought to ideally operate—the significant difference between the two concepts could be expressed by saying that we may treat the decimal representation of a real number as corresponding to a physically measurable limit ^{[14]}—and not only to a mathematically definable limit—if and only if such representation is definable by an algorithmically computable function. ^{[15]}

We note that although every algorithmically computable relation is algorithmically verifiable, the converse is not true. ^{[16]}

**References**

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

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

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

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

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

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

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

**Go31** Kurt Gödel. 1931. *On formally undecidable propositions of Principia Mathematica and related systems I.* Translated by Elliott Mendelson. In M. Davis (ed.). 1965. *The Undecidable.* Raven Press, New York. pp.5-38.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

**Tu36** Alan Turing. 1936. *On computable numbers, with an application to the Entscheidungsproblem.* In M. Davis (ed.). 1965. *The Undecidable.* Raven Press, New York. Reprinted from the Proceedings of the London Mathematical Society, ser. 2. vol. 42 (1936-7), pp.230-265; corrections, Ibid, vol 43 (1937) pp. 544-546.

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

**An12** Bhupinder Singh Anand. 2012. *Evidence-Based Interpretations of PA.* In Proceedings of the Symposium on Computational Philosophy at the AISB/IACAP World Congress 2012-Alan Turing 2012, 2-6 July 2012, University of Birmingham, Birmingham, UK.

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

**Notes**

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

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

Return to 3: Br08.

Return to 4: The significance of -consistency for the formal system PA is highlighted in An12.

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

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

Return to 7: For details see An12.

Return to 7.1: See Ro53, pp.127-136.

Return to 8: See Me64, p.49.

Return to 9: See Me64, p.107.

Return to 10: We follow the definition in Me64, p.51.

Return to 11: We show in An12 that the concept of Algorithmic verifiability is also well-defined under the standard interpretation of PA over .

Return to 12: We show in An12 that the concepts of Algorithmic verifiability and Algorithmic computability are both well-defined under the standard interpretation of PA over ; moreover they identify distinctly different subsets of the well-defined PA formulas.

Return to 13: We note that the concept of ‘algorithmic computability’ is essentially an expression of the more rigorously defined concept of ‘realizability’ in Kl52, p.503.

Return to 14: In the sense of a physically ‘completable’ infinite sequence (as needed to resolve Zeno’s paradox).

Return to 15: This point is addressed in more detail in An13.

Return to 16: See Appendix B of this preprint *Is Gödel’s undecidable proposition an ‘ad hoc’ anomaly?*.

**Two perspectives on Hilbert’s First and Second Problems**

In the Birmingham paper ‘Evidence-Based Interpretations of PA’, we introduced the distinction between algorithmic verifiability and algorithmic computability.

We showed how the distinction naturally helped distinguish between a finitary algorithmic interpretation of PA, and the non-finitary standard interpretation of PA.

We then showed how the former yielded a finitary proof of consistency for PA, as demanded by the second of Hilbert’s celebrated 23 problems.

In the previous post, we also highlighted why the the non-finitary standard interpretation of PA does not yield a finitary proof of consistency for PA.

We now show that the difference between the conclusions suggested by finitary reasoning and those suggested by non-finitary reasoning in the previous pages (as in the case of Goodstein’s argument) is reflected further in the differing status of the Continuum Hypothesis (the first of Hilbert’s 23 problems) when viewed from finitary and non-finitary perspectives as detailed below.

**The non-finitary set-theoretical perspective**

The non-finitary set-theoretical perspective on the Continuum Hypothesis is well-known, and described succintly by Topologist Peter Nyikos in a short expository lecture given at the University of Auckland in May, 2000:

“In 1900, David Hilbert gave a seminal lecture in which he spoke about a list of unsolved problems in mathematics that he deemed to be of outstanding importance. The first of these was Cantor’s continuum problem, which has to do with infinite numbers with which Cantor revolutionised set theory. The smallest infinite number, , `aleph-nought,’ gives the number of positive whole numbers. A set is of this cardinality if it is possible to list its members in an arrangement such that each one is encountered after a finite number (however large) of steps. Cantor’s revolutionary discovery was that the points on a line cannot be so listed, and so the number of points on a line is a strictly higher infinite number (, `the cardinality of the continuum’) than . Hilbert’s First Problem asks whether any infinite subset of the real line is of one of these two cardinalities. The axiom that this is indeed the case is known as the Continuum Hypothesis (CH). …

Gödel [1940] also gave a partial solution to Hilbert’s First Problem by showing that the Continuum Hypothesis (CH) is consistent if the usual Zermelo-Fraenkel (ZF) axioms for set theory are consistent. He produced a model, known as the Constructible Universe, of the ZF axioms in which both the Axiom of Choice (AC) and the CH hold. Then Cohen showed in 1963 that the negations of these axioms are also consistent with ZF; in particular, CH can fail while AC holds in a model of ZF.”

… *Hilbert’s First and Second Problems and the foundations of mathematics*, Topology Atlas Document # taic-52, Topology Atlas Invited Contributions vol. 9, no. 3 (2004) 6 pp.

**Is CH a Deﬁnite Mathematical Problem?**

Well, the non-finitary set-theoretical formulation of the Continuum Hypothesis isn’t, according to Solomon Feferman who, in a presentation at the inaugural Paul Bernays Lectures, ETH, Zurich, Sept. 12, 2012, restated in his presentation that:

My view: No; in fact it is essentially indeﬁnite (“inherently vague”).

That is, the concepts of arbitrary set and function as used in its formulation even at the level of P(N) are essentially indeﬁnite.

… *Why isn’t the Continuum Problem on the Millennium ($1,000,000) Prize List?* CSLI Workshop on *Logic, Rationality and Intelligent Interaction*, Stanford, June 1, 2013.

Feferman sought to place in perspective the anti-Platonistic basis for his belief by quoting:

“Those who argue that the concept of set is not sufﬁciently clear to ﬁx the truth-value of CH have a position which is at present difﬁcult to assail. As long as no new axiom is found which decides CH, their case will continue to grow stronger, and our assertion that the meaning of CH is clear will sound more and more empty.”

… D. A. Martin, *Hilbert’s ﬁrst problem: The Continuum Hypothesis,* in *Mathematical Developments arising from Hilbert Problems,* Felix E. Browder, Rutgers University, Editor – American Mathematical Society, 1976, 628 pp.

**A finitary arithmetical perspective**

However a possible candidate for a finitary arithmetical perspective (as proposed in the previous pages of these investigations) is reflected in the following:

**Theorem:** There is no set whose cardinality is strictly between the cardinality of the integers and the cardinality of the real numbers.

**Proof:** By means of Gödel’s -function , we can show that if denotes the digit in the decimal expansion of a putatively given real number R in the interval then, for any given natural number , we can define an arithmetical function such that:

for all .

Since Gödel’s -function is primitive recursive, it follows that every putatively given real number R can be uniquely corresponded to an algorithmically verifiable arithmetical function within the first order Peano Arithmetic PA, where we define by:

for all ,

and is selected such that:

for all .

(*For the purist, the above conclusion can be justified by the argument in this preprint.*)

**Definition: Algorithmically verifiable function**

A number-theoretical function is algorithmically verifiable if, and only if, for any given natural number , there is an algorithm which can provide objective evidence for deciding the value of each formula in the finite sequence .

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

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

**Definition: Algorithmically computable function**

A number theoretical function is algorithmically computable if, and only if, there is an algorithm that can provide objective evidence for deciding the value of each formula in the denumerable sequence .

**Cantor’s diagonal argument**

From a finitary arithmetical perspective, Cantor’s diagonal argument simply shows that there are algorithmically verifiable functions which are not algorithmically computable.

The correspondence is unique because, if R and S are two different putatively given reals in the interval , then there is always some for which . Hence we can always find corresponding arithmetical functions and such that:

for all .

for all .

.

Since PA is first order, the cardinality of the reals in the interval cannot, therefore, exceed that of the integers. The theorem follows.

In other words, the Continuum Hypothesis is trivially true from a finitary perspective because of the seemingly heretical conclusion that: , an answer that Hilbert would probably never have envisaged for the first of the celebrated twenty three problems that he bequethed to posterity!

**Skolem’s (apparent) paradox**

It is an answer that should, however, give comfort to the shades of Thoralf Skolem. In his 1922 address delivered in Helsinki before the Fifth Congress of Scandinavian Mathematicians, Skolem improved upon both the argument and statement of Löwenheim’s 1915 theorem—subsequently labelled as the:

**(Downwards) Löwenheim-Skolem Theorem**

If a first-order proposition is satisfied in any domain at all, then it is already satisfied in a denumerably infinite domain.

Skolem then cautioned about unrestrictedly (and meta-mathematically) corresponding putative mathematical entities across domains of different axiom systems, and drew attention to a:

“… peculiar and apparently paradoxical state of affairs. By virtue of the axioms we can prove the existence of higher cardinalities, of higher number classes, and so forth. How can it be, then, that the entire domain can already be enumerated by means of the finite positive integers? The explanation is not difficult to find. In the axiomatization, ‘set’ does not mean an arbitrarily defined collection; the sets are nothing but objects that are connected with one another through certain relations expressed by the axioms. Hence there is no contradiction at all if a set of the domain is non-denumerable in the sense of the axiomatization; for this means merely that *within* there occurs no one-to-one mapping of onto (Zermelo’s number sequence). Nevertheless there exists the possibility of numbering all objects in , and therefore also the elements of , by means of the positive integers; of course such an enumeration too is a collection of certain pairs, but this collection is not a ‘set’ (that is, it does not occur in the domain ).”

… Thoralf Skolem. 1922. *Some remarks on axiomatized set theory.* Text of an address delivered in Helsinki before the Fifth Congress of Scandinavian Mathematicians, 4-7 August 1922. In Jean van Heijenoort. 1967. Ed. *From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931.* Harvard University Press, Cambridge, Massachusetts, p.295.

**What do you think?** Does the above argument apply to the finite ordinals? If so, is ZF inconsistent, or is it -consistent?

**Finitarily consistent mechanist reasoning and non-finitarily consistent human reasoning: Mutually inconsistent yet complementary!**

We now consider the following (tentatively expressed) conclusions suggested by our previous post, which we shall aim to investigate from various perspectives in these pages.

**Structures**

The Birmingham paper suggests that we may need to distinguish much more sharply than we do at present between:

Mathematical structures that are built upon only finitary reasoning, and

Mathematical structures that admit non-finitary reasoning.

**Interpretations**

For instance the Birmingham paper provides:

An example of a mathematical structure based on finitary reasoning, namely the finitarily sound algorithmic interpretation of the first order Peano Arithmetic PA.

An example of a mathematical structure based on non-finitary reasoning, namely the non-finitarily sound standard interpretation of the first order Peano Arithmetic PA.

The Birmingham paper suggests that the roots of the distinction between these two structures lies in the fact that:

Finitary reasoning does not assume that Aristotle’s particularisation is always true over infinite domains.

Non-finitary reasoning assumes that Aristotle’s particularisation is always true over infinite domains.

**Consistency of Arithmetic**

In the Birmingham paper we also show that:

Finitary reasoning proves that PA is consistent finitarily (as demanded by the second of Hilbert’s celebrated twenty three problems).

Non-finitary reasoning proves that PA is consistent non-finitarily (a consequence of Gentzen’s non-finitary proof of consistency for PA).

**FOL is consistent; FOL+AP is -consistent**

This suggests that:

Finitary reasoning as formalised in first order logic (FOL) is consistent.

Non-finitary reasoning as formalised in Hilbert’s -calculus (FOL+AP) is -consistent.

**-consistency**

Since the Birmingham paper shows that Aristotle’s particularisation holds over the structure of the natural numbers if, and only if, PA is -consistent, it suggests that:

Finitary reasoning does not admit that PA can be -consistent (see Corollary 4 of this post).

Non-finitary reasoning admits that PA can be -consistent.

**Arithmetical undecidability**

Since proofs of arithmetical undecidability implicitly assume Aristotle’s particularisation, this further suggests that:

Finitary reasoning does not admit undecidable arithmetical propositions (see Corollary 3 of this post).

Non-finitary reasoning admits undecidable arithmetical propositions.

**Completed Infinity**

A significant consequence is that:

Finitary reasoning does not admit an axiom of infinity.

Non-finitary reasoning admits an axiom of infinity.

**Non-standard models of PA**

A further consequence of this is that:

Finitary reasoning does not admit non-standard models of PA.

Non-finitary reasoning too does not admit non-standard models of PA.

**Algorithmically computable truth and algorithmically verifiable truth**

The Birmingham paper also suggests that:

The truths of finitary reasoning are algorithmically computable.

The truths of non-finitary reasoning are algorithmically verifiable, but not necessarily algorithmically computable.

**Categoricity and incompleteness of Arithmetic**

We show in Corollary 1 of this post that it also follows from the Birmingham paper that:

Finitary reasoning proves that PA is categorical with respect to algorithmically computable truth.

Non-finitary reasoning proves that PA is incomplete with respect to algorithmically verifiable truth (a consequence of Gödel’s proof of of the undecidability of some arithmetical propositions in any -consistent system of arithmetic).

**How intelligences reason**

This suggests that:

Finitary reasoning is a shared characteristic of all intelligences, human or non-human.

Non-finitary reasoning is a characteristic of human intelligence that may not be shared by any other intelligence.

**Communication between intelligences: SETI**

It further suggests that the search for extra-terrestrial intelligence may benefit from the argument that:

Finitary reasoning admits effective and unambiguous communication between two intelligences with respect to its (algorithmically computable) arithmetical truths.

Non-finitary reasoning does not admit effective and unambiguous communication between two intelligences with respect to its (algorithmically verifiable) arithmetical truths.

**Determinism, Unpredictability and the EPR paradox**

An unexpected consequence of the arguments of the Birmingham paper is that our perspectives on the relation between determinism and predictability may benefit from the paradigm shift demanded by the argument that:

Finitary reasoning admits the EPR paradox.

Non-finitary reasoning does not admit the EPR paradox.

The arguments of the Birmingham paper also suggest a fresh perspective on the issue of computationalism since:

Finitary reasoning does not admit Lucas’ Gödelian argument.

Non-finitary reasoning admits Lucas’ Gödelian argument.

**Effective computability**

It further suggests that the nature and status of ‘effective computability’ may also need to be assessed afresh since:

Finitary reasoning naturally equates algorithmic computability with effective computability.

Non-finitary reasoning naturally equates algorithmic verifiability with effective computability.

**Church Turing Thesis**

As also the nature of CT, since:

Finitary reasoning admits the Church-Turing Thesis.

Non-finitary reasoning does not admit the Church-Turing Thesis.

Broadly speaking, the two conflicting-but-complementary structures defined in the Birmingham paper suggest that we should be more explicit—in our argumentation—of the structure to which a particular assertion about the natural numbers pertains, since:

Both finitary and non-finitary reasoning do not admit the proof of Goodstein’s Theorem as neither admits a completed infinity.

Set-theoretical reasoning admits the proof of Goodstein’s Theorem as it admits a completed infinity.

**There’s more …**

In the next post we shall consider some further intriguing consequences suggested by the Birmingham paper.

**What do you think?**

Does Goodstein’s sequence over the natural numbers always terminate or not?

**Aristotle’s particularisation: A grey area in our accepted foundational concepts**

We shall now argue that what mathematics needs is not a new foundation, but a greater awareness of the nature of its existing foundations.

In particular, it is the thesis of these investigations that almost all of the unresolved philosophical issues in the foundations of mathematics reflect the fact that the nature and role of Aristotle’s particularisation is left implicit when it is postulated over infinite domains.

Perhaps that is the unintended consequence of ignoring Hilbert’s efforts to integrate the concept formally into first order logic by formally defining universal and existential quantification through the introduction of his -operator.

**Semantic postulation of Aristotle’s particularisation **

Aristotle’s particularisation (AP) is the postulation that from the negation of a universal we may always deduce the existence of a contrafactual.

(*It is necessarily true over finite domains.*)

More formally:

**Aristotle’s particularisation under an interpretation**

If the formula of a first order language interprets as true under a sound interpretation of , then we may always conclude that there must be some object in the domain of the interpretation such that, if the formula interprets as the unary relation in , then the proposition is true under the interpretation.

(*We note that Aristotle’s particularisation is a non-constructive—and logically fragile—semantic deduction rule. It is reflected in classical first order deduction either by some similarly non-constructive syntactic rule of natural deduction—such as Rosser’s Rule C—or by the assumption that FOL is -consistent.*)

**Is the price of Aristotle’s particularisation too high?**

If so, we shall argue that the price being asked for assuming AP implicitly—instead of explicitly as Hilbert had proposed—may be too high!

Partially because the assumption seems to effectively obscure the far-reaching consequences of the non-finitary nature of AP from immediate view in natural and formal deductive chains.

(*And therefore of the first order logic FOL under the implicit assumption of Aristotle’s particularisation.*)

For instance, as Carnap’s deduction of the Axiom of Choice in ZF illustrates, the non-finitary consequences of assuming AP over infinite domains becomes apparent when the underlying logic is taken as Hilbert’s -calculus instead of the classical first order logic FOL.

However, formal deductions apparently prefer to substitute—seemingly arbitrarily—the implicit assumption of AP in the underlying logic by the introduction of `contrived’ formal assumptions such as Gödel’s -consistency or Rosser’s Rule C.

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

**Rosser’s Rule C**

“Since the rule ‘If , then ‘ corresponds to a hypothetical act of choice, we shall call it the rule of choice, or more briefly, Rule C.”

… J. Barkley Rosser. *Logic for Mathematicians.* 1953. McGraw Hill Book Company Inc., New York.

Similarly natural deduction chains apparently prefer to substitute—again seemingly arbitrarily—the implicit assumption of AP in the underlying logic by admitting a Rule of Infinite Induction (transfinite induction).

More importantly, the price may be too high because the implicit assumption of Aristotle’s particularisation in the underlying logic has masked the fact that, without such assumption, FOL is finitarily consistent; and—as we note below—that mathematically significant finitary structures can be built upon it without assuming AP.

**Evidence-Based Interpretations of PA**

Some consequences of making the assumption of Aristotle’s particularisation explicit are highlighted in `Evidence-Based Interpretations of PA’ that was presented at the AISB/IACAP Turing 2012 conference in Birmingham last year.

We showed there that Tarski’s inductive definitions admit evidence-based interpretations of the first-order Peano Arithmetic PA which 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:

In terms of algorithmic verifiabilty; and

In terms of algorithmic computability.

That there can be even *one*, let alone *two*, logically sound (one finitary and one non-finitary) assignments of satisfaction and truth certificates to both the atomic and compound formulas of PA had hitherto been unsuspected!

**Definition: Algorithmically verifiable arithmetical truth**

A number-theoretical relation is algorithmically verifiable if, and only if, for any given natural number , there is an algorithm which can provide objective evidence for deciding the truth/falsity of each proposition in the finite sequence .

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

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

We show in the Birmingham paper (as we shall refer to it hereafter) 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.

**Definition: Algorithmically computable arithmetical truth**

A number theoretical relation is algorithmically computable if, and only if, there is an algorithm that can provide objective evidence for deciding the truth/falsity of each proposition in the denumerable sequence .

We show in the Birmingham paper that the `algorithmic computability’ of the formulas of a formal language which contain logical constants can also be inductively defined under an interpretation in terms of the `algorithmic computability’ of the interpretations of the atomic formulas of the language; further, that the PA-formulas are decidable under an algorithmic interpretation of PA over if, and only if, they are algorithmically computable under the interpretation.

**Algorithmic verifiability vis à vis algorithmic computability**

We show in the Birmingham paper that the concepts of Algorithmic verifiability and Algorithmic computability are both well-defined under the standard interpretation of PA over ; moreover they identify distinctly different subsets of the well-defined PA formulas.

We show in this paper that although every algorithmically computable relation is algorithmically verifiable, the converse is not true.

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

From the point of view of a finitary mathematical philosophy—which is the constraint within which an applied science ought to ideally operate—the significant difference between the two concepts could be expressed (as addressed in more detail in this paper) by saying that we may treat the decimal representation of a real number as corresponding to a physically measurable limit—and not only to a mathematically definable limit—if and only if such representation is definable by an algorithmically computable function.

**The finitarily sound algorithmic interpretation of PA over **

We argued from the above distinction that the algorithmically computable PA-formulas *can* provide a finitarily sound algorithmic interpretation of PA over the domain of the natural numbers.

We showed, moreover, that this yields a finitary proof of consistency for PA—as demanded by the Second of Hilbert’s celebrated Twenty Three Problems.

**The non-finitarily sound standard interpretation of PA over **

On the other hand, the distinction also suggests that Gerhard Gentzen’s transfinite proof of consistency for PA corresponds to the argument that the algorithmically verifiable PA-formulas of PA provide a non-finitarily sound standard interpretation of PA over .

Moreover—as has been generally suspected (perhaps for the reason noted towards the end of this post)—the distinction also suggests why the standard interpretation cannot yield the finitary proof of consistency for PA as demanded by Hilbert.

**The distinction between finitary and non-finitary arithmetical reasoning introduced in the Birmingham paper has far reaching consequences**

In these pages we shall argue that the power of this simple distinction actually goes far beyond the immediate conclusions drawn in the Birmingham paper.

Reason: We can further constructively define an unambiguous distinction between finitary and non-finitary reasoning, at the level of first order logic itself, which shows that the two are both mutually inconsistent yet complementary!

As can be expected, such a distinction could have far-reaching consequences for the foundations of mathematics, logic and computabiity (which form the focus of the investigations in these pages).

We shall consider some of these in the next post.

## Recent comments