a.hazen at philosophy.unimelb.edu.au
Sun Sep 19 05:23:37 EDT 2004
De Gruyter has just (a few weeks ago) published "One Hundred
years of Russell's Paradox," edited by Godehard Link. (ISBN
3-11-017438-3. It's basically the book of the "Russell 01"
conference in Munich three years ago, but not all the conference
talks are in it (Alasdair Urquhart's and Charles Parsons's were two
that I miss), and there are other papers in it (notably by Solomon
Feferman and Hartry Field) that weren't given at the conference.)
One of the papers in it is my "A 'constructive' proper extension
of Ramified Type Theory (the logic of 'Principia Mathematica," second
edition, Appendix B)." Over all, I'm quite proud of this paper,
but I made (at least) one mistaken claim. In the final section,
discussing the mathematical strength of Russell's 1925 logic, I say
that "it seems that an argument like that for [Russell's lemma
*89.12]" could establish a general form of the Pigeon-Hole Principle.
It would be nice if it did work: given the Pigeon-Hole Principle
for arbitrary mappings, we could show that Russell's logic suffices
to derive Primitive Recursive Arithmetic from a weak axiom of
Infinity. (This would contrast with ordinary Ramified Type Theory,
as in , which Burgess  showed could only derive a weaker
fragment of arithmetic -- essentially I-Delta-0 + Exp -- from
I still think Russell's 1925 logic is an interesting system. It
DOES properly extend standard Ramified Type Theory: the general form
of Russell's *89.12, which I discuss, is an example (my mistake was
in thinking the Pigeon-Holde Principle had an analogous proof).
Asked to bet, I think it highly likely that it can derive a stronger
fragment of arithmetic than Ramified Type Theory: a straightforward
imitation of Burgess's proof that I-Delta-0 + Exp is an upper bound
on the strength of standard R.T.T. appears to give P.R.A. as an upper
bound for the 1925 logic (cf. my discussion of the ordinals needed
for cut elimination proofs for the two logics).
But the proof I thought I had fails. Russell's
"constructionalistic" logic does not allow you to infer, from the
premise that a function has a finite set as its domain, that the
function itself (considered as a set of ordered pairs) is finite.
 Alonzo Church, "A comparison of...," JSL v. 41 (1976), pp. 747-760;
repr. in R.L. Martin, ed., "Recent Essays on Truth and the Liar
Paradox," Oxford U.P., 1983.
 J.P. Burgess and A.P. Hazen, "Predicative logic and formal arithmetic,"
NDJoFL v. 39 (1998), pp. 1-17
 A.P. Hazen & J.M. Davoren, "Russell's 1925 logic," Australasian Journal
of Philosophy, v. 78 (2000), pp. 534-556 (this is a drastically
shortened version of the paper in the Link volume, not including the
erroneous claim retracted above).
University of Melbourne
More information about the FOM