mathematical logic deduction system, natural deduction, sequent calculus, lambda-calculus, judgment type theory, simple type theory, dependent type theory collection, object, type, term, set, element equality, judgmental equality, typal equality universe, size issues higher-order logic In material set theory, there is an intuitive conception of what a set is, which may be stated informally as follows: a set is a collection of sets. Actually, it is possible to have urelements in a material set theory (such as ZFA), although the most common axiom systems do not allow this; in any case we can say that a pure set is a collection of pure sets. The primary motivation for structural set theory is that this conception of a set is not needed in ordinary mathematics; it is sufficient to characterise the category of sets (although a structural set theory can also be described in ways other than category-theoretic). However, material set theory is itself part of mathematics, and we may want to describe the material notion of a pure set in structural terms. There is also a very practical point to this exercise: the translation between material and structural set theories. Any model of a material set theory is already a model of a corresponding structural set theory, but we go through the yoga below to construct a model of a material set theory out of a model of a structural set theory. In particular, we must do this to prove that two set theories (one material and one structural) are equiconsistent. See also at material-structural adjunction. Taking a base notion of set as granted, we wish to define a pure set to be a set of pure sets. On the face of it, this is a circular definition, but like many such definitions, it can be made precise in (at least) two ways: recursively and corecursively. The ‘recursive’ meaning is that all pure sets must be constructed, starting from nothing, as sets of other previously constructed pure sets. This results in the well-founded pure sets....