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  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 :
Lemma If a Peano Arithmetic P is -consistent, then there is a constructively definable P-formula  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  following J. Barkley Rosser’s 1936 paper , 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 , 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 .
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 , in a number of expositions of Gödel’s number-theoretic reasoning .
In sharp contrast, Rosser’s widely cited  argument does not appear to have received the same critical scrutiny, and its number-theoretic expositions generally remain either implicit or sketchy .
Wang’s outline of Rosser’s argument
Wang, for instance, states that  from the formal provability of:
in his formal system of first-order Peano Arithmetic Z, we may infer the formal provability of:
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  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  that from the formal provability of:
in his formal system of first-order Peano Arithmetic P, we may infer the formal provability of:
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 …’ .
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
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  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  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  of Rosser’s argument and highlight where it too implicitly presumes that P is -consistent.
Now, Gödel  defines a primitive recursive relation that holds if, and only if, is the Gödel-number of a well-formed P-formula , 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  and VII  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 , 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 :
(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!
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.
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.