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.
The following is an attempted formal definition of when a set theory is structural. It should be regarded as extremely tentative.
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:
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 to be (every potential set is a set). For such a set , the type of potential elements of must once again be the type of ZF-sets, and the elementhood predicate is simply .
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 is . The type of potential elements of is now the sum type (ZF-sets + ZF-atoms), with the membership predicate again being the ordinary membership predicate of .
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 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 to be an NBG-set when for some class . In this case the sethood predicate (for the “NBG-set” notion of set) will be .
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 being again . For each set , of course is the type of SEAR-elements of . (In contrast to ZF, these types are now nontrivially dependent on .) The elementhood predicate is , since every object in the type of SEAR-elements of is an element of 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 then asserts that is an equivalence pre-relation, with the other structure as in ordinary SEAR.
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 . The type of potential elements of each set is the type of arrows (i.e. ETCS-functions), and holds when the target of is 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 , 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 for every pair of objects and ), then the type of potential sets is the type of objects, the sethood predicate is , the type of potential elements of is , and the elementhood predicate is .
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 containing free variables and (and possibly others), if the only free occurrence of in is in the (possibly) dependent type of the variable , then
holds (where denotes all the other free variables of ). In words, for every potential set and every potential elements and of , if is a set and and are elements of , then holds of if and only if it holds of .
Equation (1) says that all elements of any set are completely indistinguishable by the formula . This is intended to approximate the idea of a structural set theory: the elements of have no independent structure (and thus cannot be distinguished from each other) apart from their identity as elements of . 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 .
Before we go on, let’s first see that ZF is definitely not structurally presented. Let be the von Nemuann numeral , and let . Clearly there are some such that holds and others such that it fails, so (1) is false. Moreover, satisfies the condition: 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 be a set containing two distinct elements and . By analogy to what we did in ZF, we’d like to take , but in SEAR this violates the required condition: must also be an element of , so appears elsewhere in than in the type of (namely, in the type of ). In fact, we can show:
SEAR is structurally presented.
Let be a formula as in the above definition. Since it does not contain free (except in the type of ), it cannot contain any variables (free or bound) denoting elements of (other than ) or relations whose source or target is . 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 . Thus, the only atomic formula involving that can appear in is , whose truth is clearly independent of the value of . It follows that the truth value of must also be so.
For similar reasons, we have:
When ETCS is written with dependent hom-types, it is structurally presented.
Let be a formula as above. Similarly to the case of SEAR, cannot contain any variables other than that denote functions whose source or target is . Since the only term-constructor in ETCS is function composition, the only terms containing that can occur in are composites ending in followed by zero or more applications of , such as itself, , , , or . Note that all of these terms denote functions with target . Moreover, the only possible terms denoting functions of target are terms of this sort, or else composites of some number of copies of (and nothing else).
Now the only atomic formulas of ETCS are equality between parallel function terms. Since the source of a composite involving cannot be (otherwise would have to occur as the source of the first function-variable in that composite), the only possible such formulas involving will be equality between two composites containing . But since 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 , and so the truth value of 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
for variables and of type “arrow”. This formula does not contain at all, yet its truth value (for a fixed and ) is not independent of . 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 we write (which can only hold when and ), and instead of we write where . 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).
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 and . Thus, for variables of type and of type , we would have an formula . By symmetry and transitivity, if and , then . But then (1) applied to implies that for any we have , so must be a subsingleton. Since 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 , which we regard as giving a way to interpret some elements as sets. Suppose moreover that each has an equality relation , and that and imply . Then for any set , if there exist and such that , then must be a subsingleton.
Suppose that and choose . By (1) it follows that holds for all , hence for all , i.e. is a subsingleton.
Note that the assumption about equality is quite reasonable if we want to interpret “” as asserting that a given element is a given set (rather than merely being related to one in some way).