General models and extensionality

Abstract

It is well known that equality is definable in type theory. Thus, in the language of [2], the equality relation between elements of type α is definable as , i.e., x α = y α iff every set which contains x α also contains y α . However, in a nonstandard model of type theory, the sets may be so sparse that the wff above does not denote the true equality relation. We shall use this observation to construct a general model in the sense of [2] in which the Axiom of Extensionality is not valid. Thus Theorem 2 of [2] is technically incorrect. However, it is easy to remedy the situation by slightly modifying the definition of general model. Our construction will show that the Axiom Schema of Extensionality is independent even if one takes as an axiom schema. We shall assume familiarity with, and use the notation of, [2] and §§2–3 of [1].