[xcthulhu]

>No one uses ramified type theory these days, at least not that I am aware

In the 1920s Frank Ramsey proved that the theory of ramified types + "The Axiom of Reducibility" is equivalent to the theory of simple types: http://en.wikipedia.org/wiki/Type_theory#Simple_theory_of_ty...

The history I've heard is that ramified types were abandoned after this, since simple type theory is easier and has the same expressive power.

[ionfish]

That's certainly always the way I've heard it, although I did come across an interesting lacuna when I was reading the the SEP article earlier, which is that the effect of the axiom of reducibility was first noticed by Polish logician Leon Chwistek [1]. His article 'The Theory of Constructive Types' was published in 1924, while Ramsey's paper dates from 1926.

José Ferreirós in The Princeton Companion to Mathematics mentions his name as well, albeit without much detail. Chwistek seems a fascinating character: like his contemporary Witkacy, he was an artist as well as a logician, and according to the biography of Alfred Tarski by the Fefermans [2], was appointed to a professorship at Lvov in 1930 which Tarski was also in the running for; apparently a letter of recommendation from Russell was the decisive factor (see p. 67 of the aforementioned).

Bernard Linsky seems to have written a chapter on Chwistek and type theory in The Golden Age of Polish Philosophy. You can read the first page [3] but I haven't been able to find the entire thing online.

[1] http://en.wikipedia.org/wiki/Leon_Chwistek

[2] http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=052...

[3] http://www.springerlink.com/content/v078l3n714589036/

[xcthulhu]

> Bernard Linsky seems to have written a chapter on Chwistek and type theory in The Golden Age of Polish Philosophy. You can read the first page [3] but I haven't been able to find the entire thing online.

Try gigapedia.com ;-D