Inhomogeneity of the urelements in the usual models of NFU
M. Randall Holmes · 2005
The simplest typed theory of sets is the multi-sorted first order system TST with equality and membership as primitive predicates and with sorts (types) indexed by the natural numbers. Atomic formulas are well-formed if they are of one of the forms x n ∈ y n+1; x n = y n. The axioms of TST are extensionality (objects of positive type are equal iff they have the same members) and comprehension (“{x n | φ} n+1 exists ” for any formula φ in the language of TST). (this theory has often been incorrectly attributed to Russell, by this author among others: see [17] for a discussion of the actual history of this system). Quine’s New Foundations (NF) ([14]) is obtained from TST by abandoning the types but retaining the same axioms. Note that the comprehension axioms of NF are not all the axioms “{x | φ} exists ” for φ a formula in the language of NF: this would be the inconsistent comprehension axiom of naive set theory. The comprehension axioms of NF are those assertions “{x | φ} exists ” where φ can be obtained from a formula of TST by dropping distinctions of type between variables (without creating any additional identifications between variables).