The SEP entry on second order or higher logic in passing say that countable order logic is type theory. My impression that this is the type theory of the Principia (I may be wrong here).

There is type theory in contemporary logic and computer-science, for example you have the typed lambda calculus, or typed first order logic.

It only just occurred to me that this may be referring to the same concept - mainly because the 2nd order logic with Henkin semantics is equivalent to typed first order logic. This gives the impression that one can fold down the hierarchy of predicates in countable order logic to a kind of type theory.

Is this on the right track?

1 Answer 1


The type theory of Principia is ramified in a nasty way, so its version of type theory isn't the modern simple theory of types we inherit from Ramsey, Gödel, Tarski and Church [if I recall!]. But Principia is the inspiration.

  • 1
    @MoziburUllah Here are some more resources in case you are interested. Warren Goldfarb has a paper explaining Russell's reasons for ramifying. It was Ramsey who showed that the simple theory of types was sufficient for most (all?) of these purposes, thus allowing us to collapse Russell's hierarchy into what we now know as the simple theory of types.
    – Dennis
    Feb 3, 2013 at 0:39
  • From the section of the SEP article on type theory explaining ramification: "As noticed however first by Chwistek, and later by Ramsey, in the presence of the axiom of reducibility, there is actually no point in introducing the ramified hierarchy at all!" That SEP entry has some good pointers to further reading in the bibliography as well.
    – Dennis
    Feb 3, 2013 at 0:43

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .