[FOM] seeking information about the ramified theory of types

[Rupert McCallum]

I have become interested in the following question. Let PM* be the
version of the ramified theory of types used in the second edition of
"Principa Mathematica", with the axiom schema of extensionality and the
axiom of infinity, but not the axiom schema of reducibility. (Russell
discussed this system in the introduction to the second edition, and
included an appendix exploring which instances of induction could be
justified in it). 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 PM* is
omega-consistent, then it is incomplete?

First of all, I have only recently become aware that the version of the
ramified theory of types used in the second edition is different to
that used in the first edition. I would be grateful if anyone could
point me to definitions of these two versions of the ramified theory of
types.

Second, I thought I once saw a message here on FOM which gave a
reference to a paper proving that EFA was interpretable in PM* but
probably not much more. If I am right about this and someone knows the
paper, I would be grateful if they could provide me with a reference to
it.

Thanks very much in advance.


      ____________________________________________________________________________________
Looking for last minute shopping deals?  
Find them fast with Yahoo! Search.  http://tools.search.yahoo.com/newsearch/category.php?category=shopping