nLab structurally presented set theory





The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms



A structural set theory is a set theory which describes only structural mathematics. A structural presentation is an attempt to describe formally when a particular (presentation of a) set theory is structural in this sense. Paradoxically, this is achieved by requiring that the elements of sets have no internal structure.

Semiformal Definition

The following is an attempted formal definition of when a set theory is structural. It should be regarded as extremely tentative.

Notions of set

First of all, in order to give a definition pertaining to all set theories, we need to know: what is a set theory? Probably no theory can intrinsically be called a set theory; it is only given that distinction by our intent to regard some of its objects of study as “sets” and others as their “elements.” Thus we make the following definition.


A notion of set in a typed first-order theory consists of:

  • A type 𝕊\mathbb{S} called the type of potential sets.
  • A unary predicate set()set(-) on 𝕊\mathbb{S} called being a set.
  • A type 𝔼 A\mathbb{E}_A, possibly depending on A𝕊A\in\mathbb{S}, called the type of potential elements of AA.
  • A unary predicate in A()in_A(-) on 𝔼 A\mathbb{E}_A called being an element of AA.

We have split the notions of sethood and elementhood into both a type and a predicate to allow for variation in theories which model them by one or the other method or a combination. Here are some examples.

  • ZF is a one-typed theory; we call the objects in the one type “ZF-sets” for clarity. The type of ZF-sets is the type of potential sets, and we take the predicate set()set(-) to be \top (every potential set is a set). For such a set AA, the type of potential elements of AA must once again be the type of ZF-sets, and the elementhood predicate is simply in A(x)(xA)in_A(x) \equiv (x\in A).

  • ZF can be augmented by the presence of urelements or atoms. One way to represent this is with two types, the type of ZF-sets and the type of ZF-atoms. Again we take the type of ZF-sets to be the type of potential sets, and the sethood predicate set()set(-) is \top. The type of potential elements of AA is now the sum type (ZF-sets + ZF-atoms), with the membership predicate again being the ordinary membership predicate of AA.

  • Atoms can be added to ZF in another way: we maintain only a single type, say the type of “ZF-objects,” but we add a “sethood” predicate which distinguishes the sets from the atoms. Now the type of potential sets is of course the type of ZF-objects, and the predicate set()set(-) is the ZF-sethood predicate.

  • In NBG or MK set-class theory, there are two possible “notions of set”: the sets and the classes. The way to formalize this depends on how the set-class theory is stated. For instance, one way to state NBG is with a single type of classes, defining a class AA to be an NBG-set when ABA\in B for some class BB. In this case the sethood predicate (for the “NBG-set” notion of set) will be set(A)(B.AB)set(A) \equiv (\exists B. A\in B).

  • In SEAR, which is a dependently typed theory, we take the type of potential sets to be the type of SEAR-sets, with the sethood predicate set()set(-) being again \top. For each set AA, of course 𝔼 A\mathbb{E}_A is the type of SEAR-elements of AA. (In contrast to ZF, these types are now nontrivially dependent on AA.) The elementhood predicate is \top, since every object in the type of SEAR-elements of AA is an element of AA by definition (that is, in SEAR elementhood is a typing assertion).

  • In the variant of SEAR without primitive equality (and thus also in SEAR+ε?), the type of potential sets is the type of “SEAR-sets equipped with an endo-relation” (a dependent sum type). The sethood predicate set(A,R)set(A,R) then asserts that RR is an equivalence pre-relation, with the other structure as in ordinary SEAR.

  • Since ETCS is an extension of the first-order theory of a category, it can be stated in several ways.

    • If ETCS is stated with two types (objects and arrows), then the type of potential sets is the type of objects (i.e. ETCS-sets) and the sethood predicate is \top. The type of potential elements of each set AA is the type of arrows (i.e. ETCS-functions), and in A(x)in_A(x) holds when the target of xx is AA and its source is a terminal object.

    • If ETCS is stated with one type, then the type of potential sets is that type, the sethood predicate is set(A)(A=s(A))set(A) \equiv (A=s(A)), the type of potential elements is of course again the single type, and the elementhood predicate is as in the two-typed version.

    • If ETCS is stated with dependent types (a type hom(A,B)hom(A,B) for every pair of objects AA and BB), then the type of potential sets is the type of objects, the sethood predicate is \top, the type of potential elements of AA is hom(1,A)hom(1,A), and the elementhood predicate is \top.

Structural Presentation

Now we make the following definition.


A notion of set in a typed first-order theory is called structurally presented if for any first-order formula φ\varphi containing free variables A:𝕊A:\mathbb{S} and x:𝔼 Ax:\mathbb{E}_A (and possibly others), if the only free occurrence of AA in φ\varphi is in the (possibly) dependent type 𝔼 A\mathbb{E}_A of the variable xx, then

(1)(z)(A:𝕊)(x,y:𝔼 A)(set(A)in A(x)in A(y)(φφ[y/x])) (\forall \vec{z})(\forall A:\mathbb{S})(\forall x,y:\mathbb{E}_A) \Big(set(A) \Rightarrow in_A(x) \Rightarrow in_A(y) \Rightarrow \big(\varphi \Leftrightarrow \varphi[y/x]\big)\Big)

holds (where z\vec{z} denotes all the other free variables of φ\varphi). In words, for every potential set AA and every potential elements xx and yy of AA, if AA is a set and xx and yy are elements of AA, then φ\varphi holds of xx if and only if it holds of yy.

Equation (1) says that all elements of any set AA are completely indistinguishable by the formula φ\varphi. This is intended to approximate the idea of a structural set theory: the elements of AA have no independent structure (and thus cannot be distinguished from each other) apart from their identity as elements of AA. Of course, we can’t do mathematics without some way to distinguish the elements of a set, but the idea of structural set theory is that this happens only through external structure imposed on the set, such as functions and relations, rather than through intrinsic properties of the elements themselves. This is the idea behind the restrictions placed on φ\varphi.

Before we go on, let’s first see that ZF is definitely not structurally presented. Let A={,{}}A=\{\emptyset, \{\emptyset\}\} be the von Nemuann numeral 22, and let φ(x=)\varphi \equiv (x = \emptyset). Clearly there are some xAx\in A such that φ\varphi holds and others such that it fails, so (1) is false. Moreover, φ\varphi satisfies the condition: AA does not occur in it at all. For the same reasons, NBG and MK are not structurally presented.

Now, why can’t we do the same thing in a structural set theory? Consider SEAR, and let AA be a set containing two distinct elements aa and aa'. By analogy to what we did in ZF, we’d like to take φ(x=a)\varphi \equiv (x = a), but in SEAR this violates the required condition: aa must also be an element of 𝔼 A\mathbb{E}_A, so AA appears elsewhere in φ\varphi than in the type of xx (namely, in the type of aa). In fact, we can show:


SEAR is structurally presented.


Let φ\varphi be a formula as in the above definition. Since it does not contain AA free (except in the type of xx), it cannot contain any variables (free or bound) denoting elements of AA (other than xx) or relations whose source or target is AA. But the only atomic formulas in the language of SEAR are equalities of set-elements, equalities of relations, and assertions that a relation holds of a pair of set-elements, and SEAR has no term constructors that could produce an element of some other set from an element of AA. Thus, the only atomic formula involving xx that can appear in φ\varphi is x=xx=x, whose truth is clearly independent of the value of xx. It follows that the truth value of φ\varphi must also be so.

For similar reasons, we have:


When ETCS is written with dependent hom-types, it is structurally presented.


Let φ\varphi be a formula as above. Similarly to the case of SEAR, φ\varphi cannot contain any variables other than xx that denote functions whose source or target is AA. Since the only term-constructor in ETCS is function composition, the only terms containing xx that can occur in φ\varphi are composites ending in x:1Ax:1\to A followed by zero or more applications of id Aid_A, such as xx itself, xfx\circ f, id Ax\id_A\circ x, (xg)h(x\circ g)\circ h, or (id Ax)(ij)(id_A\circ x)\circ (i\circ j). Note that all of these terms denote functions with target AA. Moreover, the only possible terms denoting functions of target AA are terms of this sort, or else composites of some number of copies of id Aid_A (and nothing else).

Now the only atomic formulas of ETCS are equality between parallel function terms. Since the source of a composite involving xx cannot be AA (otherwise AA would have to occur as the source of the first function-variable in that composite), the only possible such formulas involving xx will be equality between two composites containing xx. But since 11 is a terminal object, any two functions that factor through it will always be equal. Thus, the truth value of such an atomic formula is independent of the value of xx, and so the truth value of φ\varphi must also be so.

However, if ETCS is written using a two-sorted or one-sorted definition of a category, then it is not structurally presented. For instance, we can take the formula

φ((s(f)=t(x))(fx=z))\varphi \equiv \big((s(f)=t(x)) \wedge (f\circ x = z)\big)

for variables ff and zz of type “arrow”. This formula does not contain AA at all, yet its truth value (for a fixed ff and zz) is not independent of xx. This is why we have defined “structurally presented” rather than “structural”—the presentation matters.

It is, however, easy to modify the two- or one-sorted version of ETCS to make it structurally presented: we simply require the equality relation on functions to be decorated by the source and target sets, and the composition operation on functions to be decorated with the set along which composition occurs. That is, instead of f=gf=g we write equal(f,g,A,B)equal(f,g,A,B) (which can only hold when s(f)=s(g)=As(f)=s(g)=A and t(f)=t(g)=Bt(f)=t(g)=B), and instead of gfg\circ f we write g Bfg\circ_B f where t(f)=s(g)=Bt(f)=s(g)=B. Now the same argument as for the dependently-typed version applies.

It would be nice to have a definition according to which any “presentation” of ETCS would be structural; intuitively, a theory should be structural if it is “equivalent” in some sense to a structurally presented one. However, I haven’t yet been able to come up with a notion of “equivalence” which includes the above modifications of ETCS, yet excludes the equivalence between ETCS and BZC (or ZFC and ETCS+R or SEARC).

Consequences of structural presentation

From our definition of structural presentation we can deduce some of the other standard properties of structural set theories. The first is that “elements of different sets cannot be compared for equality.”


If a structurally presented notion of set includes a notion of equality between the elements of distinct sets, which is symmetric and transitive, then all of its sets are subsingletons.


Suppose that we have an equality relation that can relate elements of two distinct sets AA and BB. Thus, for variables xx of type AA and zz of type BB, we would have an formula x=zx=z. By symmetry and transitivity, if x=zx=z and x=zx'=z, then x=xx=x'. But then (1) applied to φ(x=z)\varphi\equiv (x=z) implies that for any x,y:Ax,y\colon A we have x=yx=y, so AA must be a subsingleton. Since AA was arbitrary, all sets must be subsingletons.

The second is “elements of sets are not themselves sets.”


Suppose that a structurally presented notion of set includes relations is A:𝔼 A𝕊is_A:\mathbb{E}_A\looparrowright\mathbb{S}, which we regard as giving a way to interpret some elements as sets. Suppose moreover that each 𝔼 A\mathbb{E}_A has an equality relation = A=_A, and that is A(x,B)is_A(x,B) and is A(y,B)is_A(y,B) imply x= Ayx =_A y. Then for any set AA, if there exist a:𝔼 Aa:\mathbb{E}_A and B:𝕊B:\mathbb{S} such that is A(a,B)is_A(a,B), then AA must be a subsingleton.


Suppose that is A(a,B)is_A(a,B) and choose φis A(x,B)\varphi\equiv is_A(x,B). By (1) it follows that is A(x,B)is_A(x,B) holds for all x:𝔼 Ax:\mathbb{E}_A, hence x= Ayx =_A y for all x,y:𝔼 Ax,y:\mathbb{E}_A, i.e. AA is a subsingleton.

Note that the assumption about equality is quite reasonable if we want to interpret “is Ais_A” as asserting that a given element is a given set (rather than merely being related to one in some way).

Last revised on October 20, 2022 at 16:52:58. See the history of this page for a list of all contributions to it.