[FOM] seeking information about the ramified theory of types

[Allen Hazen]

Rupert McCallum has asked about Russell's revised (1925: second edition of
"Principia Mathematica") version of Ramified Type Theory.

(1) The exposition in "Principia Mathematica" isn't as formal as it could
be, so there can be some dispute as to exactly what the system is... But on
any plausible formal reconstruction it is clear that Gödel's proof of the
incompleteness theorems can be adapted to it.  Gödel's original proof was
for a version of SIMPLE type theory with natural numbers as individuals, but
the logical community seems to have realized fairly quickly that it
generalized to a wide variety of "verwandter Systeme."

(2) As for the differences between first and second edition "Principia"...
Bernie Linsky has a not-yet-published book on the history, drawing on
material in the Russell Archives.  For the best formalizations of the two
systems of Ramified Type Theory, I would recommend the paper "Russell's 1925
Logic" by A.P. Hazen (me) and JM Davoren, in the "Australasian Journal of
Philosophy," vol. 78 (2000), pp. 534-536. (Formalization of first edition
logic follows that given in Church, "Journal of Symbolic Logic," vol. 41
(1976), pp. 747-760.)

(3) As for mathematical strength of one of these systems with an Axiom of
Infinity (but NOT the Axioms of Reducibility)...  John Burgess showed
("Notre Dame Journal of Formal Logic," vol. 39 (1998), pp. 1-19) that EFA
(under another name) could be interpreted in Ramified Second Order Logic (a
common subsystem to both first and second edition RTT) with the usual
successor axioms (0 is not a successor, two numbers with the same successor
are the same number) as nonlogical first order axioms.  (I had proved a
weaker result, by what ***I*** thought was an easier proof, in "NDJoFL" vol.
33 (1992), pp. 101-111.)  This material is reviewed in Burgess's admirable
book "Fixing Frege" (Princeton University Press, 2005).  Using a weaker,
more Russellian,  axiom of infinity, it is easy to prove the successor
axioms for "numbers" defined as items of some higher type, after which
Burgess's interpretation of EFA can be reproduced quantifying over
propositional functions one type higher, using either first edition RTT or
the (seemingly somewhat stronger) second edition logic.

(4) There is a good argument from Gödel's Second Incompleteness theorem
(sketched by Burgess in the 1998 article and in his book) that not much more
in the way of arithmetic is to be hoped for using first edition RTT.  It is
not ***obvious*** that the bounds are as low using the 1925 logic, but --
frustratingly -- I have never been able to prove that it is possible to get
more than EFA out of it.  I regard this as an interesting (well, a little
bit interesting, at least to some people) open problem.

Allen Hazen
Philosophy Department
University of Melbourne


On 12/3/08 8:24 PM, "Rupert McCallum" <rupertmccallum at yahoo.com> wrote:

> I have become interested in the following question. ... Would a professional
logician in 1931, who had read Goedel's 1931 paper "On Formally Undecidable
Propositions...", have been able to construct a finitary proof that if [2nd ed.
PM] is
omega-consistent, then it is incomplete?