Intensional Models for the Theory of Types

The axiom scheme of Extensionality states that whenever two predicates or relations are coextensive they must have the same propertie s: XY ( null x(Xnull x Ynull x) Z (ZX ZY)) (1) Historically Extensionality has always been problematic, the main problem being that in many areas of application, though not perhaps in t he foundations of mathematics, the statement is simply false. This was reco gnized by Whitehead and Russell in Principia Mathematica [32], where intensional functions such as ' A believes that p ' or'it is a strange coincidence that p ' are discussed at length. However, in the introduction to the second edition ( 1927) of the Prin-cipia Whitehead and Russell (influenced by Wittgenstein's Tractatus) already entertain the possibility that "all functions of functions are extensional". Thirteen years later, in Church's [6] canonical formulation of t he Theory of Types, it is observed that axioms of Extensionality should be adopt ed "[i]n order to obtain classical real number theory (analysis)", a wording that does not seem to rule out the option of not adopting them. Church's formula tion of type theory was completely syntactic and axioms could be adopted or d ropped at will, The Journal of Symbolic Logic, to appear.