  This version of Type theory, as simplified by Ramsey, Gödel, Carnap and Quine. is the point of departure for Quine [1937a] (which is still a good place to read the background). NF is obtained from this type theory by taking its axioms and stripping the type subscripts off all the variables. This is subtly different from Type Theory used with a policy of typical ambiguity. Under that scheme a formula like 