[FOM] Retraction

[A.P. Hazen]

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

    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 [1], which Burgess [2] showed could only derive a weaker 
fragment of arithmetic -- essentially I-Delta-0 + Exp -- from 
Infinity.)

    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.

Refs:
[1] 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.
[2] J.P. Burgess and A.P. Hazen, "Predicative logic and formal arithmetic,"
	NDJoFL v. 39 (1998), pp. 1-17
[3] 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).

--
Allen Hazen
Philosophy Department
University of Melbourne