**The significance of Aristotle’s particularisation**

The logic underlying our current interpretations of all first-order formal languages—which are incidentally also intended to provide a firm finitary formal foundation for all computing languages—is Aristotle’s logic of predicates, a fundamental tenet of which is:

**Aristotlean particularisation**: This holds that an assertion such as:

`There exists an such that holds’

—usually denoted symbolically by `‘—can be validly inferred in the classical Aristotlean logic of predicates ^{[1]} from the assertion:

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

—usually denoted symbolically by `‘.

In this post we shall review various claims that Gödel’s reasoning—concerning the formal undecidability of some arithmetical propositions— can be recast using Rosser’s argument to arrive at Gödel’s intended conclusion without Gödel’s seemingly contrived assumption of -consistency.

We shall then argue that such claims do not stand up to logical scrutiny, since we show that Rosser’s argument appeals to Aristotlean particularisation, which implicitly implies -consistency.

**Gödel and formally undecidable arithmetical propositions**

Now, in his seminal 1931 paper, Kurt Gödel showed that ^{[1]}:

**Lemma** If a Peano Arithmetic P is -consistent, then there is a constructively definable P-formula ^{[3]} such that neither nor are P-provable.

Of course, since every -consistent system is necessarily simply consistent, Gödel’s conclusion is significant only if there is an -consistent language that seeks to formally express all our true propositions about the natural numbers.

The issue of whether there actually *is* an -consistent system of Arithmetic at all appears to have been treated as inconsequential ^{[4]} following J. Barkley Rosser’s 1936 paper ^{[5]}, in which he claimed that Gödel’s reasoning can be recast to arrive at Gödel’s intended result (i.e., construction of a formally undecidable arithmetical proposition in P) by assuming only that P is simply consistent (i.e., without assuming that P is -consistent).

In this paper, we shall analyse various authoritative expositions of Rosser’s argument (including that in Rosser’s original paper), and show first that they all implicitly appeal to Aristotle’s particularisation; and second that such appeal is valid only if P is -consistent.

**The significance of -consistency**

Now classically, under Tarski’s definitions of the satisfaction and truth of the formulas of a first-order language under an interpretation ^{[6]}, the formally defined logical constant `‘ in an occurrence such as `‘—which is formally defined in terms of the primitive (undefined) logical constant `‘ as `‘—may be assumed to *always* appeal to an interpretation such as `There is some such that …’ in any sound interpretation of *any* formal first-order mathematical language without inviting inconsistency ^{[7]}.

In other words:

**Lemma** If the first-order predicate calculus of a first-order mathematical language admits quantification, then any putative classical model of the language may—without inviting inconsistency— interpret existential quantification as Aristotle’s particularisation under Tarski’s definitions of the satisfaction, and truth, of the formulas of a first-order language under an interpretation.

We thus have:

**Lemma** If Aristotle’s particularisation is logically valid, then the standard interpretation of PA is sound (under Tarski’s definitions).

**Lemma** If is sound, then PA is -consistent.

**Expositions of Rosser’s argument are generally sketchy**

Although both Gödel’s proof and Rosser’s argument are complex, and not easy to unravel, the former has been extensively analysed, and its various steps formally validated ^{[8]}, in a number of expositions of Gödel’s number-theoretic reasoning ^{[9]}.

In sharp contrast, Rosser’s widely cited ^{[10]} argument does not appear to have received the same critical scrutiny, and its number-theoretic expositions generally remain either implicit or sketchy ^{[11]}.

**Wang’s outline of Rosser’s argument**

Wang, for instance, states that ^{[12]} from the formal provability of:

(i)

in his formal system of first-order Peano Arithmetic Z, we may infer the formal provability of:

(ii)

However, the inference (ii) from (i) appears to assume that the following deduction is valid for some :

Thus, Wang’s conclusion appears to implicitly assume that Aristotle’s particularisation holds under any sound interpretation of his Peano Arithmetic Z; and, ipso facto, that Z is therefore -consistent.

Although Wang does not explicitly define the interpretation of the formal Z-formula `‘ as `There is some such that ‘, this interpretation appears implicit in his discussion and definition of `‘ in terms of Hilbert’s -function ^{[13]} as a property of the underlying logic of Wang’s Peano Arithmetic Z, and is obvious in the above argument.

In other words Wang implicitly implies that the interpretation of existential quantification cannot be specific to any particular interpretation of a formal mathematical language, but must necessarily be determined by the predicate calculus that is to be applied uniformly to all the mathematical languages in question.

**Beth’s outline of Rosser’s argument**

Similarly, in his outline of a formalisation of Rosser’s argument, Beth implicitly concludes ^{[14]} that from the formal provability of:

(i)

in his formal system of first-order Peano Arithmetic P, we may infer the formal provability of:

(ii)

However, again, the inference (ii) from (i) appears to assume that the following deduction is valid for some :

Thus, Beth’s conclusion, too, appears to implicitly assume that Aristotle’s particularisation is valid under any sound interpretation of his Peano Arithmetic P; and, ipso facto, that P is therefore -consistent.

In this case however, Beth explicitly defines the interpretation of the formal P-formula `‘ as `There is a value of such that …’ ^{[15]}.

Thus Beth, too, implies that the interpretation of existential quantification in formalised axiomatics cannot be specific to any particular interpretation of a formal mathematical language, but must necessarily be determined by the predicate calculus that is to be applied uniformly to all the mathematical languages in question.

**Where Rosser’s argument presumes -consistency**

Now, Rosser’s claim in his `extension’ ^{[16]} of Gödel’s 1931 argument ^{[17]} is that, whereas Gödel’s argument assumes -consistency, Rosser’s assumes only simple consistency.

However, we argue that Rosser’s original argument (also a sketch) implicitly appears to also presume that the system of Peano Arithmetic in question is -consistent.

For instance, the concluding deduction in Rosser’s reasoning ^{[18]} presumes that if, for any given natural number , the formula in Gödel’s Peano Arithmetic P whose Gödel-number is:

is P-provable ^{[19]} under the given premises, we may conclude that, if P is simply consistent, then the P-formula whose Gödel-number is:

is also P-provable.

Rosser essentially seems to reason here that since the P-formula —where is a specific P-numeral—is P-provable for any given P-numeral , we may conclude in this case that—unlike Gödel’s argument concerning a similar conclusion for his `undecidable’ proposition—the P-formula is P-provable.

It is difficult to see how Rosser can make this inference without implicitly presuming either Aristotle’s particularisation or that P is -consistent.

**Mendelson’s formal espression of Rosser’s argument**

I consider next Mendelson’s more rigorous proof ^{[20]} of Rosser’s argument and highlight where it too implicitly presumes that P is -consistent.

Now, Gödel ^{[21]} defines a primitive recursive relation that holds if, and only if, is the Gödel-number of a well-formed P-formula ^{[22]}, say , which has a single free variable and where is the Gödel-number of a P-proof of .

So, for any natural numbers :

(a) holds if, and only if, is the Gödel-number of a P-proof of .

Rosser’s argument defines an additional primitive recursive relation, , which holds if, and only if, is the Gödel-number of , and is the Gödel-number of a P-proof of .

Hence, for any natural numbers :

(b) holds if, and only if, is the Gödel-number of a P-proof of .

Further, it follows from Gödel’s Theorems V ^{[23]} and VII ^{[24]} that the primitive recursive relations and are instantiationally equivalent to some arithmetical relations, and , such that, for any natural numbers :

(c) If holds, then is P-provable;

(d) If holds, then is P-provable;

(e) If holds, then is P-provable;

(f) If holds, then is P-provable;

Now, whilst Gödel defines as , Rosser’s argument defines as .

Further, whereas Gödel considers the P-provability of the Gödelian proposition, , Rosser’s argument considers the P-provability of the proposition .

(We note that it is the occurence of the existential quantifier in Rosser’s formula that distinguishes it from Gödel’s. Consequently whereas Gödel’s argument can be expressed entirely within a formal arithmetic that can be presumed -consistent—without appeal to any particular interpretation of quantification—Rosser’s argument must of necessity appeal either to some non-constructive syntactic meta-rule such as Mendelson’s Rule C ^{[25]}, or to the non-constructive semantic Aristotle’s particularisation, for deriving logical consequences from an existentially quantified formula.)

We also note that, by definition:

(i) holds if, and only if, is the Gödel-number of a P-proof of:

;

(ii) holds if, and only if, is the Gödel-number of a P-proof of:

.

**Mendelson’s formal proof of Rosser’s argument**

(a) We assume, first, that is the Gödel-number of some proof sequence in P for the proposition .

Hence is true, and is P-provable.

However, we then have that is P-provable.

Further, by Modus Ponens, we have that is P-provable.

Now, if P is simply consistent, then is not P-provable.

Hence, does not hold for any natural number , and so holds for every natural number .

It follows that is P-provable for every P-numeral .

Hence, is also P-provable—a contradiction.

Hence, is not P-provable if P is simply consistent.

(b) We assume next that is the Gödel-number of some proof-sequence in P for the proposition .

Hence holds, and is P-provable.

However, if P is simply consistent, is not P-provable.

Hence, holds for every natural number , and is P-provable for all P-numerals .

(i) The foregoing implies is P-provable, and we consider the following deduction ^{[26]}:

(1) … *Hypothesis*

(2) … *By 3(b)*

(3) … *From (1), (2)*

(4) … *From (3)*

(ii) From (1)-(4), by the Deduction Theorem, we have that is provable in P for any P-numeral ;

(iii) Now, is P-provable for any P-numeral ;

(iv) Also, is P-provable for any P-numeral .

(v) Hence is P-provable for any P-numeral .

(vi) Hence is P-provable for any P-numeral .

(vii) Hence is P-provable for any P-numeral .

(viii) Now, (vii) contradicts our assumption that is P-provable.

(ix) Hence is not P-provable if P is simply consistent.

However, the claimed contradiction in (viii) *only* follows if we assume that P is -consistent, and *not* if we assume only that P is simply consistent!

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

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

**Ca62** Rudolf Carnap. 1962. *On the use of Hilbert’s -operator in scientific theories.* In *Essays on the Foundations of Mathematics.* Edited by Y. Bar-Hillel, E. I. J. Posnanski, M. O. Rabin, and A. Robinson for The Hebrew University of Jerusalem. 1962. North Holland Publishing Company, Amsterdam: pp.156-164.

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

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

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

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

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

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

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

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

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

**Notes**

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

Return to 2: Go31, Theorem VI, p.24, p.25(1) & p.26(2).

Return to 3: In his argument, Gödel refers to this formula only by its `Gödel’ number `‘; Go31, p.25, Eqn.(12).

Return to 4: See, for instance, Be59, p.595; Wa63, p.19 (Theorem 3) & p.25; Me64, p.144; Sh67, p.132 (Incompleteness Theorem); EC89, p.215; BBJ03, p.224 (Gödel’s first incompleteness theorem).

Return to 5: Ro36.

Return to 6: Ta33.

Return to 7: See, for instance, Me64, p.52(ii).

Return to 8: Possibly because Gödel’s remarkably self-contained 1931 paper—it neither contained, nor needed, any formal citations—remains unsurpassed in mathematical literature for thoroughness, clarity, transparency and soundness of exposition.

Return to 9: For instance Me64, p.143; EC89, p.210-211.

Return to 10: Be59, pp.393-395 (which focuses on Rosser’s argument, and treats Gödel’s proof of his Theorem VI (Go31, p.24) as a secondary, weaker result); Wa63, p.337; Me64, pp.144-147; Sh67, p.232 (interestingly, this introductory text contains *no* reference to Gödel or to his 1931 paper!); EC89, p.215; Sm92, p.81; BBJ03, p.226 (this introductory text, too, focuses on Rosser’s argument, and treats Gödel’s argument as more of a historical curiosity!).

Return to 11: See Be59, p.593-595; Wa63, p.337; Sh67, p.232; Rg87, p.98; EC89, p.217, Ex.2; Sm92, p.81; BBJ03, p.226.

Return to 12: Wa63, p.337.

Return to 13: Wa63, p.315(2.31); see also p.10 & pp.443-445.

Return to 14: Be59, p.594 (ij).

Return to 15: Be59, p.178.

Return to 16: Ro36.

Return to 17: Go31.

Return to 18: Ro36, p.234.

Return to 19: Notation (due to Gödel): By `P-provable’ we mean provable from the axioms of P and an arbitrary class, , of P-formulas—including the case where is empty—by the rules of deduction of P.

Return to 20: Me64, p.145, Proposition 3.32.

Return to 21: Go31, p.24, 8.1.

Return to 22: Of his formally defined Peano Arithmetic P.

Return to 23: Go31, p.22.

Return to 24: Go31, p.29.

Return to 25: Me64, p.73, §7.

Return to 26: cf. Me64, p.146.

## Leave a comment

Comments feed for this article