Automated Reasoning in Higher Order Logic
This page was created and is maintained by Chad E Brown.
Some Links to Notes on Ramified Type Theory
Leivant's Survey of Higher Order Logic includes a discussion of Russell's Ramified Type Theory and relates Ramified Type Theory to first order logic via Lindstrom's Theorem. He also discusses the possibility of iterating the power set operation beyond omega.