nLab SEAR

SEAR

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

SEAR

Introduction

SEAR, short for Sets, Elements, And Relations, is a structural set theory with the following properties:

  • It is equivalent in strength to the material set theory ZF. (It can be augmented by an axiom of choice to produce SEARC, which is strongly equivalent to ZFC.)
  • It contains a subtheory called bounded SEAR which (when augmented by choice) is strongly equivalent to ETCS. Conversely, ETCS can be augmented by a replacement axiom to become equivalent to SEARC.

Being a structural set theory, SEAR differs from ZF in the following ways (which are also ways in which it is similar to ETCS):

  • There is a type distinction between sets and elements; a set is never an element of another set. Every element is an element of some set.
  • The elements of a set have no “internal structure;” they are merely featureless points.
  • The “elementhood” relation xAx\in A only makes sense when xx is known to be an element of some ambient set XX and AA is known to be a subset of XX.

A good description of the difference between material and structural set theory can be found at Trimble on ETCS I. However, ZFC and ETCS also differ along another axis than the material-structural. At Trimble on ETCS III the following metaphor is proposed for this dimension:

with ZFC it’s more as if you can just hop in the car and go; with ETCS you build the car engine from smaller parts with your bare hands, but in the process you become an expert mechanic, and are not so rigidly attached to a particular make and model.

Using this metaphor, SEAR can be thought of as an ETCS-car which comes preassembled with a nice slick control panel. Or, using an alternate metaphor, ZFC is like Windows, ETCS is like UNIX, and SEAR is like OS X (or maybe Ubuntu). With SEAR you get a nice familiar interface with which it is easy to do standard things, there is less cruft than you get with ZFC, and behind the scenes you have all the power of ETCS (and more). (Of course, if you like Microsoft products, then this metaphor probably does not appeal to you.)

Note that experts will probably always prefer to build their own car/OS; the goal of SEAR is to make structural set theory accessible to a wider audience. In particular, SEAR is intended to demonstrate the complete independence of structural set theory from category theory. Thus, apart from being (by default) stronger than ETCS, SEAR differs from it in the following ways:

  • It includes the notion of an element of a set as a primitive concept, rather than defining it as a particular sort of function.
  • It does not include the notion of a function as a primitive concept (instead it includes the notion of a binary relation, with functions defined via their graphs in a familiar way).
  • It does not include the notions of composition or identities (of either functions or relations) as primitive concepts. In particular, it does not require the user to know what a category is, even implicitly.
  • As a corollary, its axioms do not require knowledge of categorical concepts such as limits and natural numbers objects (although these concepts can be very naturally introduced while learning SEAR).
  • The property of separation (one of the most important facts in the everyday use of set theory) is a direct consequence of the axioms of SEAR. Compare how in ETCS, the property of bounded separation follows from the theorem that a topos is a Heyting category, which requires substantial work.

Description of SEAR

Types

SEAR is a theory about three kinds of things: sets, elements, and relations. Every element, and every variable that ranges over elements, is always associated to something denoting a set (which might be a constant or a variable); we say it is an element of that set. If xx is an element of AA we write xAx\in A; note that this is not an assertion which may be true or false, but a typing declaration. In formal terms, this means that SEAR is a dependently typed theory, with a type of sets, a type of elements for each set term, and a type of relations for each pair of set terms.

One consequence of this is that whenever we quantify over elements we must always quantify over elements of some set; thus we can say “for all elements xAx\in A” but not “for all elements xx.” Another consequence is that the assertion x=yx=y is only well-formed (a precondition to its being true or false) if xx and yy are elements of the same set.

In a similar manner, every relation is always associated to an ordered pair of sets, the first called its source and the second its target (thus the fundamental relations in SEAR are binary relations). If φ\varphi is a relation from AA to BB we write φ:AB\varphi:A\looparrowright B. As with elements, the assertion φ=ψ\varphi=\psi is only well-formed if φ\varphi and ψ\psi have the same source and the same target.

Implicit in the existence of three types of things is that nothing is both a set and an element, etc., so in particular a statement such as x=Ax=A is not well-formed if xx is an element and AA a set. Furthermore, SEAR does not include an equality relation between sets: even if AA and BB are both sets we do not consider A=BA=B to be well-formed. (Thus SEAR respects the principle of equivalence.)

The final piece of data that we have is a notion of when a relation φ:AB\varphi:A\looparrowright B holds of a pair of elements xAx\in A and yBy\in B. We write φ(x,y)\varphi(x,y) when φ\varphi holds of xx and yy.

Basic axioms

Now we can state the axioms of SEAR, beginning with the most basic ones.

Axiom 0 (Nontriviality): There exists a set which contains an element.

Axiom 1 (Relational comprehension): For any two sets AA and BB, and any property PP that can obtain of an element of AA and an element of BB, there exists a unique relation φ:AB\varphi:A\looparrowright B such that φ(x,y)\varphi(x,y) if and only if PP obtains of xx and yy.

Here “property” is interpreted formally as “first-order formula”, which makes the axiom (like later the axiom of collection) in fact an axiom scheme.

Axiom 1 basically says that relations are what we expect them to be intuitively. It should remind the reader of the axiom of separation. The two important differences are (1) the presence of two sets and two variables, rather than one, and (2) the fact that what is produced is not a set, but a relation (a different kind of thing). The to-be-introduced Axiom 2 will enable us to make relations into (sub)sets, but first we need some terminology.

Definition

A relation φ:AB\varphi:A\looparrowright B is called a function from AA to BB if for any xAx\in A, there exists exactly one yBy\in B with φ(x,y)\varphi(x,y).

We write f:ABf:A\to B for such a function, and for xAx\in A we write f(x)f(x) for the resulting unique yBy\in B. Note that the uniqueness clause in Axiom 1 implies that functions are extensional: if f,g:ABf,g:A\to B and f(x)=g(x)f(x)=g(x) for all xAx\in A, then f=gf=g.

Axiom 2 (Tabulations): For any relation φ:AB\varphi:A\looparrowright B, there exists a set |φ||\varphi| and functions p:|φ|Ap:{|\varphi|}\to A and q:|φ|Bq:{|\varphi|}\to B such that: (1) for any xAx\in A and yBy\in B, we have φ(x,y)\varphi(x,y) if and only if there exists r|φ|r\in {|\varphi|} with p(r)=xp(r)=x and q(r)=yq(r)=y, and (2) for any r|φ|r\in {|\varphi|} and s|φ|s\in{|\varphi|}, if p(r)=p(s)p(r)=p(s) and q(r)=q(s)q(r)=q(s), then r=sr=s.

A set |φ||\varphi| equipped with pp and qq as in Axiom 2 is called a tabulation of the relation φ\varphi. We think of |φ||\varphi| as “the set of pairs (x,y)(x,y) such that φ(x,y)\varphi(x,y) holds,” with pp and qq projecting (x,y)(x,y) to xx and yy, respectively. Note that by Axiom 1, any set RR equipped with functions p:RAp:R\to A and q:RBq:R\to B satisfying (2) determines a unique relation φ:AB\varphi:A\looparrowright B such that φ(x,y)\varphi(x,y) holds iff there is an rRr\in R with p(r)=xp(r)=x and q(r)=yq(r)=y; then RR is a tabulation of φ\varphi.

Consequences of the basic axioms

Axioms 0, 1, and 2 alone are very powerful! Here are some things we can do with them.

Theorem

There exists a set \emptyset which has no elements.

Proof

By Axiom 0, there exists a set AA. By Axiom 1, there exists a relation φ:AA\varphi:A\looparrowright A such that φ(x,y)\varphi(x,y) holds never. Using Axiom 2, let \emptyset be a tabulation of φ\varphi.

From now on we fix a particular set \emptyset having no elements. By Axiom 1, for any set AA there is exactly one relation A\emptyset\looparrowright A and exactly one relation AA\looparrowright\emptyset.

Theorem

There exists a set 11 which has exactly one element.

Proof

By Axiom 0, there exists a set AA containing an element xx. By Axiom 1, there exists a relation φ:AA\varphi:A\looparrowright A such that φ(y,z)\varphi(y,z) holds iff y=xy=x and z=xz=x. Using Axiom 2, let 11 be a tabulation of φ\varphi.

From now on we fix a particular set 11 having exactly one element; we usually denote this element by \star. By Axiom 1, for every set AA there exists a unique function f:A1f:A\to 1, defined by f(x)=f(x)=\star for every xAx\in A. Likewise, to every function g:1Ag:1\to A there corresponds a unique element xAx\in A, by g()=xg(\star)=x.

We define a subset of a set AA to be a relation S:1AS:1\looparrowright A. By Axiom 1, a subset SS of AA is determined by precisely those xAx\in A such that S(,x)S(\star,x). If S(,x)S(\star,x) we write xSx\in S. Note that this is an overloading of the notation \in; it can be distinguished from the previous usage because here SS is a relation, not a set. Note also that the previous usage xAx\in A was a typing declaration (it says what kind of thing xx is when we introduce it), whereas xSx\in S is a statement which can be either true or false.

Now Axiom 2 implies that from any subset SS of AA we can construct a set |S||S| with a function i:|S|Ai:{|S|}\to A such that (1) xSx\in S iff there is an x|S|x'\in {|S|} with i(x)=xi(x')=x, and (2) for x,x|S|x',x''\in {|S|}, if i(x)=i(x)i(x')=i(x'') then x=xx'=x''. A function ii with property (2) is called injective; in this way we set up a correspondence between subsets and injective functions. (Likewise, a function f:ABf:A\to B is surjective if for any yBy\in B there is an xAx\in A with f(x)=yf(x)=y.) Combined with Axiom 1, this implies the following separation property.

Theorem

For any property PP of elements of a set AA, there exists a set BB and an injective function i:BAi:B\to A such that for aAa\in A, we have P(a)P(a) iff a=i(b)a=i(b) for some bBb\in B.

Although the set |S||S| is not determined uniquely by the subset SS, it is determined up to bijection. We define an bijection to be a relation ψ:AB\psi:A\looparrowright B such that for every xAx\in A there is a unique yBy\in B with ψ(x,y)\psi(x,y), and for every yBy\in B there is a unique xAx\in A with ψ(x,y)\psi(x,y). Clearly any bijection is a function, as is its opposite (defined by ψ o(y,x)ψ(x,y)\psi^o(y,x) \Leftrightarrow \psi(x,y)), and these two properties characterize bijections. It is also easy to see that a function is a bijection iff it is both injective and surjective.

For example, it is easy to see that if AA and BB both have no elements, there is a unique bijection between them; thus an empty set \emptyset is determined up to unique bijection. Likewise, if AA and BB both contain a unique element, then there is a unique bijection between them; thus a set 11 with one element is also determined up to unique bijection.

Theorem

If |φ||\varphi| and |φ|{|\varphi|}' are two tabulations of the same relation φ:AB\varphi:A\looparrowright B, then there is a bijection between |φ||\varphi| and |φ|{|\varphi|}'.

Proof

By Axiom 1, define B:|φ||φ|B:{|\varphi|} \looparrowright {|\varphi|}' such that B(x,y)B(x,y) holds precisely when p(x)=p(y)p(x)=p'(y) and q(x)=q(y)q(x)=q'(y). The properties of tabulations immediately imply that BB is a bijection.

Corollary

If |S||S| and |S|{|S|}' are two tabulations of the same subset SAS\subseteq A, then there is a bijection between |S||S| and |S|{|S|}'.

The composite of two relations φ:AB\varphi:A\looparrowright B and ψ:BC\psi:B\looparrowright C is defined to be the relation ψφ:AC\psi\varphi:A\looparrowright C (also written ψφ\psi\circ\varphi) such that ψφ(x,z)\psi\varphi(x,z) holds of xAx\in A and zCz\in C iff there is a yBy\in B with φ(x,y)\varphi(x,y) and ψ(y,z)\psi(y,z). The identity relation id A:AAid_A:A\looparrowright A is defined by id A(x,y)x=yid_A(x,y) \Leftrightarrow x=y.

Theorem

Composition of relations is associative (χ(ψφ)=(χψ)φ\chi(\psi\varphi)=(\chi\psi)\varphi), and identity relations are identities for composition (id Bφ=φ=φid A\id_B\circ \varphi = \varphi = \varphi\circ\id_A). The composite of functions is a function, and the identity relation is a function. The composite of bijections is a bijection, and a relation φ:AB\varphi:A\looparrowright B is a bijection iff there is a relation ψ:BA\psi:B\looparrowright A such that ψφ=id A\psi\varphi = id_A and φψ=id B\varphi\psi=id_B.

Proof

Just as in naive set theory.

Informally speaking, we have two categories whose objects are the sets: in Rel the morphisms are the relations, while in Set the morphisms are the functions. Formally, all we can say is that these are “meta-categories,” in the sense that from any model of the first-order axioms of SEAR we can construct them as models of the first-order axioms of a category. (This is not that different from the status of large categories such as SetSet in material set theories such as ZF. We could also speak about “proper classes” as is done in ZF using first-order formulas.) See also the section on Universes, below.

In both of these (meta-)categories, the isomorphisms are the bijections. We have also already observed that \emptyset and 11 are an initial object and a terminal object in SetSet, respectively, and that \emptyset is both initial and terminal in RelRel.

For sets AA and BB, let :AB\top:A\looparrowright B denote the relation such that (x,y)\top(x,y) holds always. A tabulation of \top is denoted A×BA\times B; it is a set equipped with functions p:A×BAp:A\times B \to A and q:A×BBq:A\times B\to B such that for any xAx\in A and yBy\in B, there exists a unique zA×Bz\in A\times B with p(z)=xp(z)=x and q(z)=yq(z)=y. It is called the cartesian product of AA and BB.

Theorem

For any sets AA and BB, A×BA\times B is a product of AA and BB in the category SetSet.

Proof

Just as in naive set theory.

In particular, SetSet has products.

Theorem

The category SetSet has finite limits.

Proof

It remains to construct the equalizer of two functions f,g:ABf,g:A\to B. Let SS be the subset of AA so that xSx\in S just when f(x)=g(x)f(x)=g(x); then |S|A{|S|}\to A is easily shown to be an equalizer of ff and gg.

Theorem

For any function f:ABf:A\to B we have f=mef = m e, where m:im(f)Bm:im(f)\hookrightarrow B is an injection and e:Aim(f)e:A\twoheadrightarrow im(f) is a surjection. A set im(f)im(f) equipped with such mm and ee is unique up to bijection and is called the image of ff.

Proof

Let im(f)im(f) be |S||S| where SS is defined by ySy\in S iff there exists an xAx\in A with f(x)=yf(x)=y. By definition, we have an injection m:im(f)Bm:im(f)\hookrightarrow B. And for any xAx\in A, clearly f(x)Sf(x)\in S, so there is a unique yim(f)y\in im(f) with m(y)=f(x)m(y)=f(x); we define e(x)=ye(x)=y. It is easy to verify the rest.

Similarly, we can define the union and intersection of subsets of AA in the usual way: we have xSTx\in S\cup T iff xSx\in S or xTx\in T, and xSTx\in S\cap T iff xSx\in S and xTx\in T.

Theorem

SetSet is a well-pointed Heyting category and RelRel is a division allegory.

Proof

Left to the reader.

Power sets and colimits

In structural set theory, sets cannot contain other sets (or relations), so we cannot strictly speaking have “the set of subsets of a set AA.” What we generally do instead is have a set PAP A each of whose elements is associated to a subset of AA in a bijective way. This association happens via a specified relation between AA and PAP A.

Axiom 3 (power sets): For any set AA, there exists a set PAP A and a relation ϵ:APA\epsilon:A\looparrowright P A such that for any subset SS of AA, there exists a unique sPAs\in P A with the property that for any xAx\in A, we have xSx\in S iff ϵ(x,s)\epsilon(x,s).

As in both material set theory and ETCS, many useful consequences flow from this axiom. We first observe that the property of PAP A stated for subsets actually implies an analogous property for all relations.

Theorem

For any relation R:BAR:B\looparrowright A, there exists a unique function f R:BPAf_R:B\to P A such that R(y,x)R(y,x) if and only if ϵ(x,f R(y))\epsilon(x,f_R(y)). It follows that SetSet is a topos (and RelRel is a power allegory).

Proof

We simply define f Rf_R elementwise; for each yy we define f R(y)f_R(y) to be the unique element of PAP A such that ϵ(x,f R(y))\epsilon(x,f_R(y)) holds iff R(y,x)R(y,x) holds. Extensionality of functions implies that it is unique.

As usual, power sets also imply the existence of function sets.

Theorem

For any two sets AA and BB, there exists a set B AB^A and a function ev:B A×ABev:B^A \times A\to B such that for any function f:ABf:A\to B there exists a unique element s fB As_f\in B^A such that ev(s f,a)=f(a)ev(s_f,a)=f(a) for all aAa\in A. It follows that SetSet is a cartesian closed category.

Proof

We take B AB^A to be a tabulation of the subset of P(A×B)P(A\times B) containing only the functions. More precisely, define FP(A×B)F\subseteq P(A\times B) such that sFs\in F iff for every xAx\in A, there exists a unique yBy\in B such that ϵ((x,y),s)\epsilon((x,y),s), and let B A=|F|B^A = {|F|}.

The correspondences in Theorems and are “meta-bijections,” but by a standard Yoneda lemma argument they can be converted into actual bijections as defined above in SEAR. This produces bijections such as C A×B(C A) BC^{A\times B} \cong (C^A)^B and P(A×B)(PA) BP(A\times B) \cong (P A)^B.

We now construct quotient sets. Of course, by an equivalence relation on a set AA we mean a relation R:AAR:A\looparrowright A which is reflexive, transitive, and symmetric.

Theorem

If RR is an equivalence relation on AA, then there is a surjective function q:ABq:A\twoheadrightarrow B such that R(x,y)R(x,y) holds iff q(x)=q(y)q(x)=q(y).

Proof

RR induces a function f R:APAf_R:A\to P A as above; let BB be im(f R)im(f_R) and qq the surjective part of the image factorization. If R(x,y)R(x,y) holds, then by symmetry and transitivity, R(x,z)R(y,z)R(x,z)\Leftrightarrow R(y,z) for all zz; hence f R(x)=f R(y)f_R(x)=f_R(y) and so q(x)=q(y)q(x)=q(y). Conversely, if q(x)=q(y)q(x)=q(y), then f R(x)=f R(y)f_R(x)=f_R(y); but yf R(y)y\in f_R(y) by reflexivity, hence yf R(x)y\in f_R(x) and thus R(x,y)R(x,y) holds.

Such a BB, which is easily seen to be unique up to bijection, is called a quotient of RR and often written A/RA/R.

Likewise, given sets AA and BB, let AB=|S|A\sqcup B={|S|}, where SS is the subset of PA×PBP A \times P B consisting of the pairs ({x},{})(\{x\},\{\}) for xAx\in A and ({},{y})(\{\},\{y\}) for yBy\in B. (Of course, here we are identifying elements of PA×PBP A \times P B with ordered pairs of subsets of AA and BB via the projections of the product and the defining relations ϵ A\epsilon_A and ϵ B\epsilon_B.) We have evident injections AABA\to A\sqcup B and BABB\to A\sqcup B which are jointly surjective and have disjoint image; we call ABA\sqcup B the disjoint union of AA and BB.

In particular, it follows that SetSet is a pretopos (as is any topos).

Infinity

Axiom 4 (Infinity): There exists a set NN, containing an element oo, and a function s:NNs:N\to N such that s(n)os(n)\neq o for any nNn\in N and s(n)=s(m)s(n) = s(m) only if n=mn = m for any n,mNn, m\in N.

It is easy to deduce any of the usual consequences of the axiom of infinity. The set NN is not asserted to be minimal, but it is easy to cut it down to be so using separation. In particular, this axiom implies that SetSet has a natural numbers object. We can then proceed to construct the set \mathbb{Q} of rational numbers and the set \mathbb{R} of real numbers in any of the usual ways.

Note also that Axiom 4 implies Axiom 0.

We can however define sets with nn elements for each natural number nn directly axioms 0, 1, 2 and 3.

Collection

The final axiom of SEAR is somewhat trickier to motivate. It corresponds to the axiom of replacement (or more precisely collection; see Wikipedia until we get around to writing our own article) in ZFC\mathbf{ZFC}, and the reasons that we need it are the same as the reasons that ZFC\mathbf{ZFC} needs it.

The ghost of a universal set

One way to motivate the collection axiom is as follows. Suppose for the sake of argument that there existed a universal set, meaning a set containing all other sets. Now in structural set theory this is meaningless, since no set can contain other sets, but there is an easy fix: we consider instead indexed families of sets. There are multiple ways to make this precise, but here is a very simple one: an AA-indexed family of sets is simply a relation M:AXM:A\looparrowright X. The set indexed by each element aAa\in A is M a={xX|M(a,x)}M_a = \{x\in X | M(a,x)\}. (Often one requires the M aM_a to be a disjoint decomposition of XX, so that M oM^o is a function XAX\to A, but this is unnecessary. In fact, if M:AXM:A\looparrowright X is a general family, then |M|A{|M|} \to A is a function that represents a family in this stronger sense which is equivalent to MM.)

With this definition, a universal family of sets would be a set UU with a UU-indexed family of sets E:UYE:U\looparrowright Y such that for any set AA, there exists a unique uUu\in U and a bijection AE uA\cong E_u. The existence of such a universal set is inconsistent, but the collection axiom can be thought of as the “ghost” of what would be implied by Axioms 1 and 2 if a universal set did exist. Let’s now unravel that.

If UU were a universal set, then any AA-indexed family M:AXM:A\looparrowright X would induce a unique function f:AUf:A\to U such that E f(x)M xE_{f(x)} \cong M_x for all xAx\in A. Conversely, any function f:AUf:A\to U would induce an AA-indexed family of sets with this property: just take the composite relation EfE \circ f. (This family would not be unique, but it would be unique up to a suitable notion of equivalence between indexed families.) Thus it is reasonable to consider the “ghost” of a function f:AUf:A\to U to be simply an AA-indexed family of sets.

The ghost of a relation AUA\looparrowright U is even easier. By Axiom 1, to give such a relation would be equivalent to describing a property PP that can obtain of an element of AA and a set. Thus, the ghost of a relation AUA\looparrowright U is simply such a property.

If UU existed, Axiom 2 would imply that any relation AUA\looparrowright U had a tabulation consisting of a set BB and functions p:BAp:B\to A and q:BUq:B\to U. We now kill UU and inspect the ghostly remnants of this tabulation.

Axiom 5 (Collection): For any set AA and any property PP which can obtain of an element of AA and a set, there exists a set BB, function p:BAp:B\to A, and a BB-indexed family of sets M:BYM:B\looparrowright Y such that (1) P(p(b),M b)P(p(b),M_b) holds for any bBb\in B, and (2) for any aAa\in A, if there exists a set XX with P(a,X)P(a,X), then aim(p)a\in im(p).

What this axiom asserts is actually a bit weaker than the precise ghost of a tabulation of PP; that would require instead of (2) that for any aAa\in A and any set XX with P(a,X)P(a,X), there exists a bBb\in B with p(b)=ap(b)=a and M bXM_b\cong X. However, this stronger statement is still inconsistent, because if we took A=1A=1 and P=P=\top it would resurrect UU in the form of BB! The form given above is weak enough to keep the dead in their graves, yet strong enough to be useful. (The former statement follows from the discussion below about inter-interpretability of SEAR and ZF, at least as long as the reader believes that ZF is consistent. The latter remains to be gone more into.)

Exercise: why respect for the principle of equivalence necessary for Axiom 5 to be reasonable as stated?

Applications of collection

One thing that Axiom 5 is good for is the recursive construction of sets. For example, using Axioms 1–4 we can construct the sets NN, P(N)P(N), P(P(N))P(P(N)), and so on, but we cannot construct anything larger than all the sets in this sequence. Axiom 5 allows us to do that.

(more detail to be added here…)

Variants and Comparisons

The Axiom of Choice

We obtain a theory called SEARC (SEAR with Choice) by adding the following axiom:

Axiom 6 (Choice): If φ:AB\varphi:A\looparrowright B is a relation such that for any aAa\in A, there exists a bBb\in B with φ(a,b)\varphi(a,b), then there exists a function f:ABf:A\to B with φ(a,f(a))\varphi(a,f(a)) for all aAa\in A.

This is easily seen to be equivalent to asserting that all surjections are split in SetSet, which is a more common categorical form of the axiom of choice.

Constructive SEAR

Axioms 1–5 of SEAR make perfect sense whether the ambient logic is classical or constructive. By Diaconescu’s argument, Choice implies the logic is classical. We may call SEAR interpreted in intuitionistic logic ISEAR.

To obtain a predicative theory, Axiom 3 can be replaced by an appropriate weaker axiom, such as the existence of disjoint unions and quotient sets. We may call this variation of SEAR PSEAR.

If desired, we can also add function sets or even a structural version of the axiom of subset collection; as usual, function sets, subset collection, and power sets are all equivalent using classical logic. We may call this variation of SEAR CSEAR.

Compare Erik Palmgren's constructive ETCS.

Bounded SEAR and ETCS

By bounded SEAR we mean the subtheory consisting of axioms 2–4 of SEAR plus

Axiom 1B (Bounded relational comprehension): The same as Axiom 1, but the property PP must be bounded (it can only involve quantifiers over elements, not sets or relations).

All the theorems cited above remain true with Axiom 1 replaced by Axiom 1B, so bounded SEAR still implies that SetSet is a well-pointed topos with a NNO. Therefore, bounded SEARC implies ETCS. Conversely, it is not hard to show that given any well-pointed topos, if we interpret “set” as “object of the topos”, “element of AA” as “global element 1A1\to A”, and “relation ABA\looparrowright B” as “subobject of A×BA\times B,” then Axioms 0, 1B, 2, and 3 are satisfied. It follows that ETCS also implies bounded SEARC, so the two are equivalent.

ETCS can also be augmented with additional axioms to make it equivalent to full SEARC, but that is beyond our scope at the moment.

SEAR and ZF

From ZF to SEAR

It is fairly straightforward to construct a model of SEAR from a model of ZF. Given a model of ZF, we define the SEAR-sets to be the ZF-sets, and the SEAR-elements of AA to be the ZF-elements of AA. If we prefer, we can take the SEAR-elements of AA to be pairs (x,A)(x,A) where x ZFAx\in_{ZF} A, so that the elements of distinct sets will be disjoint—but this is not necessary, since in SEAR the question of whether two distinct sets have elements in common is not even well-posed. Finally, we of course take the SEAR-relations ABA\looparrowright B to be the ZF-subsets of A×BA\times B, and we let φ(x,y)\varphi(x,y) hold in SEAR iff (x,y) ZFφ(x,y)\in_{ZF} \varphi. It is then easy to prove Axioms 0, 1, 2, 3, and 4 from the axioms of ZF, and likewise Axiom 6 follows easily from the axiom of choice in ZFC. (In fact, Z and ZC, where the replacement axiom is omitted, suffice for these conclusions.) The only axiom which requires some thought is Collection, and it is here that we use replacement.

Theorem

The sets, elements, and relations in a model of ZF satisfy the Collection axiom of SEAR.

Proof

Let AA be a set and PP a property as in Axiom 5. As given, PP is a first-order statement in the language of SEAR, but we can easily translate it into a statement in the language of ZF; from now on we work in ZF. Define

A={aA|X.P(a,X)}.A' = \{a\in A | \exists X. P(a,X)\}.

By the axiom of foundation, for each aAa\in A' there exists an ordinal λ\lambda and an XV λX\in V_{\lambda} such that P(a,X)P(a,X); let λ a\lambda_a be the smallest such λ\lambda. Then aV λ aa\mapsto V_{\lambda_a} is a class function, so by the axiom of replacement, the set {V λ a|aA}\{V_{\lambda_a} | a\in A'\} exists. Let YY be the union of this set. Define

B={(a,X)A×Y|P(a,X)},B = \{ (a,X)\in A\times Y | P(a,X)\},

let p:BAp:B\to A be the projection onto the first factor, and let M:BYM:B\looparrowright Y be defined by

M((a,X),x)xX.M((a,X),x) \Leftrightarrow x\in X.

Then M (a,X)=XM_{(a,X)} = X, since each V λV_\lambda is a transitive set, so P((a,X),M (a,X))P((a,X), M_{(a,X)}) holds for any (a,X)B(a,X)\in B. Finally, by construction, if there exists XX with P(a,X)P(a,X) then aim(p)a\in im(p); thus the SEAR axiom of collection is satisfied.

Note the use of the axiom of foundation in addition to the axiom of replacement. This can be avoided if we use instead the ZF version of the axiom of collection, which is equivalent to the axiom of replacement over the other ZF axioms (including foundation), by an argument like that above.

From SEAR to ZF

Conversely, from any model of SEAR one can construct a model of ZF. The basic idea of this process is described at pure set. Given a model of SEAR, we define a ZF-set to be an equivalence class of well-founded extensional accessible graphs, as described at pure set. We define the global membership relation \in on ZF-sets to be the “immediate subgraph” relation.

The proofs of most of the axioms of ZF are straightforward, and may eventually be found at pure set. Here we treat the proof of the replacement/collection axiom of ZF from the Collection axiom of SEAR, since that is specific to SEAR.

Theorem

The ZF-sets constructed from a model of SEAR satisfy the ZF axiom of collection (which is equivalent to the axiom of replacement over the other axioms of ZF).

Proof

We will prove the version of the ZF axiom of collection which states that for any first-order formula PP in the language of ZF, and any ZF-set AA, there exists a ZF-set DD such that for any ZF-element x ZFAx\in_{ZF} A, if there exists a ZF-set yy such that P(x,y)P(x,y), then there exists such a yy which is a ZF-element of DD. Note that any first-order formula in the language of ZF about ZF-sets can easily be translated into a first-order formula in the language of SEAR.

Fix such a PP and AA; thus AA is a SEAR-set equipped with a binary relation \to of a certain type. Let AA' be the subset of AA consisting of the children of the root of AA. For a SEAR-set XX, let P(a,X)P'(a,X) mean that XX admits the structure of a ZF-set such that the ZF-statement P(down(a),X)P(down(a),X) holds. By the SEAR axiom of collection, there is a set BB, a function p:BAp:B\to A', and a BB-indexed family of sets M:BYM:B\looparrowright Y such that (1) each M bM_b admits the structure of a ZF-set with P(down(p(b)),M b)P(down(p(b)),M_b), and (2) if there is a ZF-set XX with P(down(a),X)P(down(a),X), then aim(p)a\in im(p).

Let CC be the subset of B×P(Y×Y)×YB\times P(Y\times Y)\times Y consisting of pairs (b,r,y)(b,r,y) such that yM by\in M_b and rr represents a binary relation on M bM_b making it into a ZF-set such that P(down(p(b)),M b)P(down(p(b)),M_b). Now CC can be equipped with the relation that is the disjoint union of all the rrs, i.e. we set (b,r,y)(b,r,y)(b,r,y)\to (b',r',y') iff b=bb=b', r=rr=r', and y ryy\to_r y'. Let C=C1C'=C\sqcup 1 extend this relation with the additional point being a root, i.e. (b,r,y)(b,r,y)\to \star iff yy is the root of rr. Now CC' is a well-founded accessible graph, but it may not be extensional; we take DD to be the ZF-set represented by the extensional quotient of CC'.
Then for any x ZFAx\in_{ZF}A, we have xdown(a)x\cong down(a) for some child aa of the root of AA, i.e. aAa\in A'. Thus, if there is a ZF-set yy with P(x,y)P(x,y), then aim(p)a\in im(p) and so there is such a ZF-set represented by one of the rr‘s occurring in CC. By construction, this ZF-set is then equivalent to down(d)down(d) for some child of the root of DD, hence down(d) ZFDdown(d) \in_{ZF} D. Thus DD satisfies the requirement of the ZF axiom of collection.

Thus, SEAR and SEARC are at least equiconsistent with ZF and ZFC, respectively. In fact, SEARC and ZFC are equivalent, in the sense that passage back and forth in either direction yields an equivalent model. However, passage from SEAR to ZF and back again can lose information, if there are sets in the model of SEAR which do not admit any well-founded extensional relation (this doesn’t happen in the presence of choice, since then every set can be well-ordered).

Type theory and internalization

Every topos has an internal logic, which is a type theory. However, the line between type theory and structural set theory is fine and sometimes hard to see; the main difference is that structural set theory can involve quantifiers over sets (= types), while type theory only allows (“bounded”) quantifiers over elements of types. However, formally, if one has a type judgment AtypeA \; \mathrm{type} and a type of sets SettypeSet \; \mathrm{type} rather than a set judgment AsetA \; \mathrm{set}, one could use quantifers bounded over elements of SetSet instead of unbounded quantifiers. The type of sets SetSet in structural set theory behaves as a Russell universe in type theory, where given a set ASetA \in Set one could derive a type AtypeA \; \mathrm{type}. Through this correspondence, Intuitionistic Bounded SEAR can be treated as a type theory and interpreted internally in any topos with a NNO. Of course, if the topos is boolean, then the logic can be classical.

One can also write down stronger axioms on a topos such that if they are satisfied, then full Intuitionistic SEAR can be interpreted “internally” in that topos, extending the usual internal logic.

Making alternate primitive choices

Three-sorted SEAR

An alternate formulation of the theory uses three sorts, one for sets, elements, and relations, making SEAR into a three-sorted set theory. The membership aAa \in A becomes a relation between the sort of elements and the sort of sets, while the relational domain and codomain notation φ:AB\varphi:A \looparrowright B also becomes a ternary relation between the sort of relations, and two copies of the sort of sets. There is a quinary relation holds(A,B,φ,a,b)\mathrm{holds}(A, B, \varphi, a, b) between all three sorts, which says that given sets AA and BB, the relation φ\varphi holds for element aa and bb in the context of φ:AB\varphi:A \looparrowright B, aAa \in A, and bBb \in B.

SEPS: Using pairs and subsets instead of relations

An alternate formulation of the theory, suggested by Toby, has four primitive notions: sets, elements, subsets, and a pairing operation. Sets and elements are as before. A subset is, like an element, attached to a certain set; it is always a subset of some set. Thus we have a typing declaration SAS\subseteq A. We also have a primitive notion of when an element xAx\in A belongs to a subset SAS\subseteq A; thus now we have xSx\in S as a possible assertion of the theory (analogous to R(x,y)R(x,y) before). We allow a typed equality predicate for subsets. Finally, there is an operation which assigns to every pair of sets AA and BB a set A×BA\times B, and to every pair of elements xAx\in A and yBy\in B an element (x,y)A×B(x,y)\in A\times B.

Axiom 0 is the same as before.

Axiom 12\frac{1}{2} (Pairing): For every pair of sets AA and BB and every element zA×Bz\in A\times B, there exists a unique pair of elements xAx\in A and yBy\in B such that z=(x,y)z=(x,y).

Axiom 1121\frac{1}{2} (Subset comprehension): For every property PP that can obtain of elements xx of some set AA, there exists a unique subset SAS\subseteq A such that xSx\in S precisely when PP obtains of xx

We now define a relation ABA\looparrowright B to be a subset of A×BA\times B. With this definition, Axiom 1121\frac{1}{2} clearly implies Axiom 1 (relational comprehension). We define functions and their properties as before. Axiom 12\frac{1}{2} implies that there are projection functions A×BAA\times B\to A and A×BBA\times B\to B which make A×BA\times B into a product in SetSet.

Axiom 2122\frac{1}{2} (Separation): For every set AA and every subset SAS\subseteq A, there exists a set |S||S| and an injective function i:|S|Ai:{|S|}\to A such that for any xAx\in A, we have xSx\in S if and only if there is a z|S|z\in {|S|} with i(z)=xi(z)=x.

Applying separation to subsets of A×BA\times B and composing ii with the product projections, we recover Axiom 2 (tabulations). We can now go on with the subsequent axioms stated in the same way as before.

SEPAF: Using pairs and functions instead of relations

One could use functions instead of relations. Sets and elements are as before. A function f:ABf:A \to B depends on two sets AA and BB, similar to a relation. For every function f:ABf:A \to B and element aAa \in A, one could form the element f(a)Bf(a) \in B called the function evaluation of ff at aa. Finally, there is an operation which assigns to every pair of sets AA and BB a set A×BA\times B, and to every pair of elements xAx\in A and yBy\in B an element (x,y)A×B(x,y)\in A\times B, as well as functions π A:A×BA\pi_A:A \times B \to A and π B:A×BB\pi_B:A \times B \to B.

Axiom 0 is the same as before.

Axiom 14\frac{1}{4} (strong extensionality): Given function i:ABi:A \to B, the following statements are logically equivalent to each other:

  • there exists a function i 1:BAi^{-1}:B \to A such that for all elements xAx \in A and yBy \in B, i 1(i(x))=xi^{-1}(i(x)) = x and i(i 1(y))=yi(i^{-1}(y)) = y
  • for every element xBx \in B there exists a unique element yAy \in A such that i(y)=xi(y) = x

A function is a bijection if one of the two conditions above hold.

Axiom 12\frac{1}{2} (Pairing): For every pair of sets AA and BB and for every element xAx \in A, yBy \in B, and zA×Bz\in A\times B, π A((x,y))=x\pi_A((x, y)) = x, π B((x,y))=y\pi_B((x, y)) = y, and z=(π A(z),π B(z))z=(\pi_A(z),\pi_B(z)).

An function f:ABf:A \to B is an injection if for all elements xAx \in A and yAy \in A, x=yx = y if and only if f(x)=f(y)f(x) = f(y), and is usually denoted f:ABf:A \hookrightarrow B. AA is a subset of BB if it comes with an injection i:ABi:A \hookrightarrow B. We now define a relation to be a set RR with an injective function i:RA×Bi:R \hookrightarrow A\times B.

Axiom 2122\frac{1}{2} (Separation): For every property PP that can obtain of elements xx of some set AA, there exists a set SS and unique injection i:SAi:S \hookrightarrow A such that there exists an element ySy \in S such that i(y)=xi(y) = x precisely when PP obtains of xx

A relation i:RA×Bi:R \hookrightarrow A \times B is a total functional relation if for all elements aAa \in A, there exists a unique element bBb \in B and a unique element zA×Bz \in A \times B such that i(z)=(a,b)i(z) = (a, b). Since there is a function π Ai:RA\pi_A \circ i:R \to A, by strong extensionality there is an inverse function (π Ai) 1:AR(\pi_A \circ i)^{-1}:A \to R, and the function π B(π Ai) 1:AB\pi_B \circ (\pi_A \circ i)^{-1}:A \to B is the function satisfying i((π Ai) 1(a))=(a,π B((π Ai) 1(a))i((\pi_A \circ i)^{-1}(a)) = (a, \pi_B((\pi_A \circ i)^{-1}(a)). Thus, the principle of unique choice holds.

Applying separation to relations i:RA×Bi:R \hookrightarrow A \times B and using the principle of unique choice, we recover Axioms 1 (relational comprehension) and 2 (tabulations). We can now go on with the subsequent axioms stated in the same way as before.

Eliminating equality

As stated SEAR includes a fundamental “equality” relation on elements of a given set. However, we can also make equality into structure. This is definitely not along the “more accessible to undergraduates” direction! But it may sometimes be technically helpful.

Consider a theory of pre-sets, elements, and pre-relations as in SEAR, with “pre-sets” replacing sets, except that there is no given equality relation on anything. Axiom 0 requires no modification. In Axiom 1, we reinterpret the “uniqueness” clause as a definition of what it means for two parallel pre-relations to be equal, i.e. φ=ψ\varphi=\psi if φ(x,y)ψ(x,y)\varphi(x,y)\Leftrightarrow\psi(x,y) for all xx and yy in the source and target of φ\varphi and ψ\psi.

Before stating the version of Axiom 2 we need some definitions. We define a set to be a preset AA equipped with an equivalence pre-relation = A=_A. A relation between sets (A,= A)(A,{=_A}) and (B,= B)(B,{=_B}) is a pre-relation φ:AB\varphi:A\looparrowright B which is extensional in the sense that if φ(x,y)\varphi(x,y), x= Axx'=_A x, and y= Byy'=_B y, then φ(x,y)\varphi(x',y'). Finally, a function f:(A,= A)(B,= B)f:(A,{=_A}) \to (B,{=_B}) is a relation which is (a) entire: for any xAx\in A, there is a yBy\in B with f(x,y)f(x,y), and (b) functional: if f(x,y)f(x,y) and f(x,y)f(x',y') and x= Axx=_A x', then y= Byy=_B y'.

Now Axiom 2 reads: for any sets (A,= A)(A,{=_A}) and (B,= B)(B,{=_B}) and any relation φ:(A,= A)(B,= B)\varphi:(A,{=_A})\looparrowright (B,{=_B}), there exists a set (|φ|,= |φ|)({|\varphi|},{=_{|\varphi|}}) and functions p:|φ|Ap:{|\varphi|}\to A and q:|φ|Bq:{|\varphi|}\to B such that: (1) for any xAx\in A and yBy\in B, we have φ(x,y)\varphi(x,y) if and only if there exists r|φ|r\in {|\varphi|} with p(r,x)p(r,x) and q(r,y)q(r,y), and (2) for any r|φ|r\in {|\varphi|} and s|φ|s\in{|\varphi|}, if p(r)= Ap(s)p(r)=_A p(s) and q(r)= Bq(s)q(r)=_B q(s), then r= |φ|sr=_{|\varphi|}s. Note that it is sufficient to assert merely that |φ||\varphi| is a pre-set and pp and qq are entire relations satisfying (1), since (2) can then be used to define = |φ|=_{|\varphi|} in such a way as to make it a set and pp and qq functions.

The construction of \emptyset is just as in ordinary SEAR. The construction of 11 in ordinary SEAR used equality, but we now have a simple replacement for it: let 11 be any pre-set containing an element, equipped with the equivalence relation such that x=yx=y always for any x,y1x,y\in 1. Similarly, in this variant we can construct quotient sets without needing powersets; we simply enlarge the equivalence relation on the underlying pre-set of a set.

Of course, if (A,= A)(A,{=_A}) is a set, a subset of AA is a relation 1(A,= A)1\looparrowright (A,{=_A}). Axiom 3 can now be translated as-is, or it can be simplified to assert merely the existence of a pre-set PAP A such that any subset of AA is represented by some element of PAP A, with the uniqueness clause turned into a definition of = PA=_{P A}. The same idea applies to all the other axioms.

If to this equality-free version of SEAR we add a primitive notion of (non-extensional) “operation” and a choice operator, we obtain SEAR+?.

Models

In model theory, one could construct models of a particular theory CC.

Models of SEAR

Here, we construct a categorical model of SEAR in the context of homotopy type theory. This particular model of SEAR, CC, consists of

  • A type Ob(C)Ob(C), whose terms are called “sets”. We shall call these “internal sets”, to distinguish them from the sets of the metatheory?.

  • For each internal set A:Ob(C)A:Ob(C), a set El(A)El(A), whose terms are called “elements”. We shall call these “internal elements”, to distinguish them from the elements of the metatheory.

  • For each internal set A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C), a set Hom(A,B)Hom(A,B), whose terms are called “relations”. We shall call these “internal relations”, to distinguish them from the relations of the metatheory.

  • For each internal set A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C), internal relation R:Hom(A,B)R:Hom(A,B), and internal element a:El(A)a:El(A) and b:El(B)b:El(B), a type R(a,b)R(a,b) with a term p:isProp(R(a,b))p:isProp(R(a,b)) representing that R(a,b)R(a,b) is a mere proposition.

  • For each internal set A:Ob(C)A:Ob(C), B:Ob(C)B:Ob(C), D:Ob(C)D:Ob(C), a function

    ()():Hom(B,D)×Hom(A,B)Hom(A,D)(-)\circ(-):Hom(B,D) \times Hom(A,B) \to Hom(A,D)

    representing composition of internal relations, and a term

    γ: A:Ob(C) B:Ob(C) D:Ob(C) R:Hom(A,B) S:Hom(B,C) a:El(A) d:El(D)(SR)(a,d)[ b:El(B)S(b,d)×R(a,b)]\gamma:\prod_{A:Ob(C)} \prod_{B:Ob(C)} \prod_{D:Ob(C)} \prod_{R:Hom(A,B)} \prod_{S:Hom(B,C)} \prod_{a:El(A)} \prod_{d:El(D)} (S \circ R)(a, d) \cong \left[\sum_{b:El(B)} S(b,d) \times R(a,b)\right]

    where [T]\left[T\right] is the propositional truncation of the type TT. This states that for all internal sets AA, BB, and DD, all internal relations R:Hom(A,B)R:Hom(A,B) and S:Hom(B,C)S:Hom(B,C), and all internal elements a:El(A)a:El(A) and d:El(D)d:El(D), (SR)(a,d)(S \circ R)(a, d) if and only if there exists an element b:El(B)b:El(B) such that S(b,d)S(b,d) and R(a,b)R(a,b).

  • For each internal set A:Ob(C)A:Ob(C), a relation

    id A:Hom(A,A)id_{A}:Hom(A,A)

    representing the internal identity relation, and terms

    p: A:Ob(C) B:Ob(C) R:Hom(A,B) a:El(A) a :El(A) b:El(B) b :El(B)(R(a,b)×id A(a,a )×id B(b,b ))R(a ,b )p:\prod_{A:Ob(C)} \prod_{B:Ob(C)} \prod_{R:Hom(A,B)} \prod_{a:El(A)} \prod_{a^{'}:El(A)} \prod_{b:El(B)} \prod_{b^{'}:El(B)} (R(a,b) \times id_A(a,a^{'}) \times id_B(b,b^{'})) \to R(a^{'},b^{'})

    This states the axiom of extensionality: that for all internal sets AA and BB, internal relation RR, and internal elements a:El(A)a:El(A), a :El(A)a^{'}:El(A), b:El(B)b:El(B), and b :El(B)b^{'}:El(B), R(a,b)R(a,b) and id A(a,a )id_A(a,a^{'}) and id B(b,b )id_B(b,b^{'}) together imply R(a ,b )R(a^{'},b^{'}).

Thus, CC is a dagger 2-poset whose underlying category is a concrete category.

Let the type of all internal maps between internal sets A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) in CC be defined as

Map(A,B) f:Hom(A,B) a:El(A)isContr( b:El(B)P(f)(a,b))Map(A, B) \coloneqq \sum_{f:Hom(A,B)} \prod_{a:El(A)} isContr\left(\sum_{b:El(B)} P(f)(a,b)\right)
  • For each internal set A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C), a function ()(()):Map(A,B)×El(A)El(B)(-)((-)): Map(A,B) \times El(A) \to El(B) representating evaluation of internal maps and a term δ:isContr(P(f)(a,f(a)))\delta:isContr(P(f)(a, f(a))), representing that the relation P(f)(a,f(a))P(f)(a, f(a)) is true.

  • A internal set A:Ob(C)A:Ob(C) with a term ϵ:[El(A)]\epsilon:\left[El(A)\right], representing that there is an inhabited set.

  • For each internal set A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) and internal relation R:Hom(A,B)R:Hom(A,B), an internal set |R|:Ob(C)\vert R \vert:Ob(C) and map f:Hom(|R|,A)f:Hom(\vert R \vert, A), g:Hom(|R|,B)g:Hom(\vert R \vert, B), and a term q:R=f gq:R = f^\dagger \circ g and a term

    η: x:El(|R|) y:El(|R|)(f(x)=f(y))×(g(x)=g(y))(x=y)\eta:\prod_{x:El(\vert R \vert)} \prod_{y:El(\vert R \vert)} (f(x) = f(y)) \times (g(x) = g(y)) \to (x = y)

    representing that every internal relation comes with a subset of the product set El(A)×El(B)El(A) \times El(B).

  • For each internal set A:Ob(C)A:Ob(C), a internal set 𝒫(A)\mathcal{P}(A) and a internal relation A:Hom(A,𝒫(A))\in_A:Hom(A, \mathcal{P}(A)) and a term

    ι: B:Ob(C) R:Hom(A,B)[ χ R:Hom(A,P(B))isMap(χ R)×(R=( B )χ R)]\iota:\prod_{B:Ob(C)} \prod_{R:Hom(A,B)} \left[\sum_{\chi_R:Hom(A,P(B))} isMap(\chi_R) \times (R = (\in_B^\dagger) \circ \chi_R)\right]

    representing that internal power sets exist.

As a result, CC is an elementarily topical dagger 2-poset.

  • An internal set :Ob(C)\mathbb{N}:Ob(C) with internal maps 0:El()0:El(\mathbb{N}) and s:Hom(,)s:Hom(\mathbb{N},\mathbb{N}) and a term

    κ: A:Ob(C) 0 A:El(A) s A:Hom(A,A)[ f:Hom(,A)(f(0)=0 A)× n:El()(f(s(n))=s A(f(n)))]\kappa:\prod_{A:Ob(C)} \prod_{0_A:El(A)} \prod_{s_A:Hom(A,A)} \left[\sum_{f:Hom(\mathbb{N},A)} (f(0) = 0_A) \times \prod_{n:El(\mathbb{N})} (f(s(n)) = s_A(f(n)))\right]

    representing that a natural numbers object exist.

  • For each internal set A:Ob(C)A:Ob(C) and function Q:El(A)×Ob(C)Prop 𝒰Q:El(A) \times Ob(C) \to Prop_\mathcal{U}, an internal set B:Ob(C)B:Ob(C) with an internal map p:Hom(B,A)p:Hom(B,A), a function M:El(B)Ob(C)M:El(B) \to Ob(C) and terms

    λ: b:El(B)isContr(Q(p(b),M(b)))\lambda:\prod_{b:El(B)} isContr(Q(p(b),M(b)))
    μ: a:El(A)[ X:Ob(C)isContr(Q(a,X))][ b:Bp(b)=a]\mu:\prod_{a:El(A)} \left[\sum_{X:Ob(C)} isContr(Q(a,X))\right] \to \left[\sum_{b:B} p(b) = a\right]

    representing that the axiom of collection is validated.

Models of SEPS

Here, we construct a model of SEPS in the context of homotopy type theory. This particular model of SEPS, CC, consists of

  • A type Ob(C)Ob(C), whose terms are called “sets”. We shall call these “internal sets”, to distinguish them from the sets of the metatheory?.

  • For each “set” A:Ob(C)A:Ob(C), a set El(A)El(A), whose terms are called “elements”. We shall call these “internal elements”, to distinguish them from the elements of the metatheory.

  • For each “set” A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C), a set A×BA \times B, whose terms are called “pairs”. We shall call these “internal pairs”, to distinguish them from the pairs of the metatheory.

  • For each “set” A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C), a function ((),()):El(A)×El(B)El(A×B)((-),(-)):El(A) \times El(B) \to El(A \times B) with functions p A:El(A×B)El(A)p_A:El(A \times B) \to El(A) and p B:El(A×B)El(B)p_B:El(A \times B) \to El(B)

  • For each “set” A:Ob(C)A:Ob(C), a type Sub(A)Sub(A), whose terms are called “subsets”, and a term p:isHeytAlg(Sub(A))p:isHeytAlg(Sub(A)), representing that the subsets of AA are Heyting algebras. We shall call these “internal subsets”, to distinguish them from the subsets of the metatheory.

An internal relation is a term R:Sub(A×B)R:Sub(A \times B).

  • For each internal set A:Ob(C)A:Ob(C), B:Ob(C)B:Ob(C), D:Ob(C)D:Ob(C), a function

    ()():Sub(B×D)×Sub(A×B)Sub(A×D)(-)\circ(-):Sub(B \times D) \times Sub(A \times B) \to Sub(A \times D)

    and a term

    γ: A:Ob(C) B:Ob(C) D:Ob(C) R:Sub(A×B) S:Sub(B×C) a:El(A) d:El(D)(SR)(a,d)=[ b:BS(b,d)×R(a,b)]\gamma:\prod_{A:Ob(C)} \prod_{B:Ob(C)} \prod_{D:Ob(C)} \prod_{R:Sub(A \times B)} \prod_{S:Sub(B \times C)} \prod_{a:El(A)} \prod_{d:El(D)} (S \circ R)(a, d) = \left[\sum_{b:B} S(b,d) \times R(a,b)\right]

    where [T]\left[T\right] is the propositional truncation of the type TT.

  • For each internal set A:Ob(C)A:Ob(C), B:Ob(C)B:Ob(C), a relation

    id A,B:Sub(A×B)id_{A,B}:Sub(A \times B)

    and terms

    p: A:Ob(C) B:Ob(C) R:Sub(A×B) a:El(A) a :El(A) b:El(B) b :El(B)(R(a,b)×id A(a,a )×id B(b,b ))R(a ,b )p:\prod_{A:Ob(C)} \prod_{B:Ob(C)} \prod_{R:Sub(A \times B)} \prod_{a:El(A)} \prod_{a^{'}:El(A)} \prod_{b:El(B)} \prod_{b^{'}:El(B)} (R(a,b) \times id_A(a,a^{'}) \times id_B(b,b^{'})) \to R(a^{'},b^{'})

Let the type of all internal maps between internal maps A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) in CC be defined as

Map(A,B) f:Sub(A×B) a:El(A)isContr( b:El(B)P(f)(a,b))Map(A, B) \coloneqq \sum_{f:Sub(A \times B)} \prod_{a:El(A)} isContr\left(\sum_{b:El(B)} P(f)(a,b)\right)
  • For each internal set A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C), a function ()(()):Map(A,B)×El(A)El(B)(-)((-)): Map(A,B) \times El(A) \to El(B) and a term δ:isContr(P(f)(a,f(a)))\delta:isContr(P(f)(a, f(a))).

  • An internal set A:Ob(C)A:Ob(C) with a term ϵ:[El(A)]\epsilon:\left[El(A)\right].

  • For each internal set A:Ob(C)A:Ob(C), there is a function |()|:Sub(A)Ob(C)\vert(-)\vert:Sub(A) \to Ob(C), and for every subset S:Sub(A)S:Sub(A) there is an injection? i:|S|Ai:\vert S \vert \to A.

  • For each internal set A:Ob(C)A:Ob(C), an internal set 𝒫(A)\mathcal{P}(A) and a internal relation A:Sub(A×𝒫(A))\in_A:Sub(A \times \mathcal{P}(A)) and a term

    ι: B:Ob(C) R:Sub(A×B)[ χ R:Hom(A,P(B))isMap(χ R)×(R=( B )χ R)]\iota:\prod_{B:Ob(C)} \prod_{R:Sub(A \times B)} \left[\sum_{\chi_R:Hom(A,P(B))} isMap(\chi_R) \times (R = (\in_B^\dagger) \circ \chi_R)\right]
  • An internal sets :Ob(C)\mathbb{N}:Ob(C) with internal maps 0:El()0:El(\mathbb{N}) and s:Sub(×)s:Sub(\mathbb{N} \times \mathbb{N}) and a term

κ: A:Ob(C) 0 A:El(A) s A:Sub(A×A)[ f:Hom(,A)(f(0)=0 A)× n:El()(f(s(n))=s A(f(n)))]\kappa:\prod_{A:Ob(C)} \prod_{0_A:El(A)} \prod_{s_A:Sub(A \times A)} \left[\sum_{f:Hom(\mathbb{N},A)} (f(0) = 0_A) \times \prod_{n:El(\mathbb{N})} (f(s(n)) = s_A(f(n)))\right]
  • For each internal set A:Ob(C)A:Ob(C) and function Q:El(A)×Ob(C)Prop 𝒰Q:El(A) \times Ob(C) \to Prop_\mathcal{U}, an internal set B:Ob(C)B:Ob(C) with an internal map p:Sub(B×A)p:Sub(B \times A), a function M:El(B)Ob(C)M:El(B) \to Ob(C) and terms
    λ: b:El(B)isContr(Q(p(b),M(b)))\lambda:\prod_{b:El(B)} isContr(Q(p(b),M(b)))
    μ: a:El(A)[ X:Ob(C)isContr(Q(a,X))][ b:Bp(b)=a]\mu:\prod_{a:El(A)} \left[\sum_{X:Ob(C)} isContr(Q(a,X))\right] \to \left[\sum_{b:B} p(b) = a\right]

The following pages develop various aspects of set theory in SEAR or related theories.

Last revised on December 19, 2022 at 18:56:27. See the history of this page for a list of all contributions to it.