Uniqueness in Structural Set Theories

Over the last couple of years, I've occasionally tried to have a go at understanding certain categorical formulations of set theory. These are sometimes also called "structural set theories". There are a number of these now, including:
Historically, Lawvere's $\mathsf{ETCS}$ appeared first, in
Lawvere, 1964: "An elementary theory of the category of sets", Proceedings of the National Academy of Sciences of the USA 52, 1506-1511.
A number of variants have since been given; and there are a number of very interesting recent formulations, given by category theorists Todd Trimble, Tom Leinster, Toby Bartels and Mike Shulman. These have been described at the category-theory wiki nLab: e.g.,
ETCS at nLab.
Structural set theory at nLab.
SEAR at nLab.
Two summaries of the philosophical outlook are given in recentish blogposts:
Tom Leinster, "Rethinking Set Theory", n-Category Cafe (Dec 18, 2012; article here)
Mike Shulman, "From Set Theory to Type Theory", n-Category Cafe (Jan 7, 2013)
Both have very stimulating comments! Mike Shulman emphasizes the following difference:
... if $X$ is a structural-set, then there are some things which by their very nature are elements of $X$. (In $\mathsf{ETCS}$, those things are the functions with domain $1$ and codomain $X$.) If a thing is not given to you as an element of $X$, then it isn’t an element of $X$, and no thing can be given to you as an element of more than one structural-set. The statement $A \in X$ is not something that you would ever think about proving about two pre-existing things $A$ and $X$, or assuming as a hypothesis except at the same time as you introduce $A$ as a new variable (as a way of saying “this is the sort of thing that $A$ is”). That is, to be maximally faithful to its usage in mathematics, $A \in X$ should not be considered as a proposition.
It seems to me, at first sight, that this will cause trouble with applied mathematics. For example, when we apply mathematics, in physics, chemistry, statistics and so on, one wants to consider
  • classes of non-mathematical things, 
  • various quantity functions (and indeed physical fields) from those things to various value ranges (e.g., $\mathbb{R}$ or some linear space, etc.). 
Still, let's put that worry aside.

To some extent, the emergence of such "structural set theories" responds to the challenge, by some mathematicians who have expressed their preference for the ordinary (Cantorian) concept of a set as a "definite collection of things", to give a fully axiomatic presentation of structural set theory.

Here I try and focus on the theory $\mathsf{SEAR}$ ("sets, elements and relations") which I find a bit easier to understand, as the algebra only takes off slowly ... I only give the basic syntax (at least as I understand it: I may be reading it wrongly), and three of the axioms.

What is interesting is the topic of uniqueness.


1. Syntax of $L_{\mathsf{SEAR}}$

I take the alphabet $\Sigma$ of $L_{\mathsf{SEAR}}$ to be:
$\Sigma = \{\mathbf{Set}, =, :, \neg, \wedge, \vee, \bot, \exists, \forall , \looparrowright, (,) \} \cup \{v^{set}_i\}_{i \in \omega} \cup \{v^{rel}_i\}_{i \in \omega} \cup \{v^{el}_i\}_{i \in \omega}$
Where it is implicitly assumed that all labelled syntactical thingies are distinct. There are three things worth highlighting:
(i) This language is 3-sorted (or there are 3 types, if you like). There are three disjoint sets (!!) $\{v^{set}_i\}$, $\{v^{rel}_i\}$, $\{v^{el}_i\}$ of variables, for "sets", "elements" and "relations". These will be relabelled, for ease of notation, in a moment.
(ii) There is a symbol, $:$, used for "type declaration". For example, given variables $x,A$, it gives a term $x : A$.
(iii) There is a symbol, $\looparrowright$, used for type declaration of relations: given $A,B, \varphi$, it gives a term $\varphi : A \looparrowright B$.
Definition 1 (Terms of $L_{\mathsf{SEAR}}$)
For each $i, j,k \in \omega$, the following expressions are terms:
$v^{set}_i : \mathsf{Set}$
$v^{el}_i : v^{set}_j$
$v^{rel}_i : v^{set}_j \looparrowright v^{set}_k$
Nothing else is a term. (These are "type-declarations". Note that variables are not counted as terms.)

Notation: It is convenient to use the variables $x,y,z, \dots$ instead of $v^{el}_i$, in the obvious way. It is convenient to use the variables $A,B,C, \dots$ instead of $v^{set}_i$, in the obvious way. It is convenient to use the variables $\varphi, \psi, \dots$ instead of $v^{rel}_i$, in the obvious way.

Definition 2 (Atomic Formulas of $L_{\mathsf{SEAR}}$)
For any element variables $x,y$, relation variables $\varphi, \psi$, the following are atomic formulas:
$\bot$
$x = y$
$\varphi = \psi$
$\varphi(x,y)$
These are all the atomic formulas.

It is worth highlighting that equations with $=$ flanked by set variables, i.e., of the form
$A = B$, 
do not count as atomic formulas. This is related to what is unclear about the uniqueness issue raised below. In fact, if I understand the syntax properly,
set variables do not appear in any atomic formulas.
Rather, set variables appear only in complex terms: namely, either in the type-declaration
$A : \mathsf{Set}$,
or as domain and codomain within the type declaration
$\varphi : A \looparrowright B$
of a relation.

Definition 3 (Formulas of $L_{\mathsf{SEAR}}$)
Then we define the formulas by the usual inductive clauses:
Each atomic formula is a formula.
If $\phi$ is a formula, then $\neg \phi$ is a formula.
If $\phi, \theta$ are formulas, then $\phi \vee \theta$ is a formula.
If $\phi, \theta$ are formulas, then $\phi \wedge \theta$ is a formula.
If $\phi$ is a formula and $t$ a term, then $(\forall t) \phi$ is a formula.
If $\phi$ is a formula and $t$ a term, then $(\exists t) \phi$ is a formula.
Nothing else is a formula.

Notation: We don't fuss about brackets. We assume that the additional binary connectives $\to$ and $\leftrightarrow$ have been introduced by explicit definition in the usual way. That is:
$\phi \to \theta$ is short for $\neg \phi \vee \theta$
$\phi \leftrightarrow \theta$ is short for $(\phi \to \theta) \wedge (\theta \to \phi)$
So, for example, we have:
$A: \mathsf{Set}$ is a term.
$x : A$ is a term.
$\varphi: A \looparrowright B$ is a term.
$x = y$ is a formula.
$(\forall A : \mathsf{Set})(\exists \varphi: A \looparrowright A)(\forall x : A)(\forall y :A)(\varphi(x,y) \leftrightarrow x = y)$ is a formula.
Definition 4 (Function) Suppose $\varphi : A \looparrowright B$ and, for all $x:A$, there is exactly one $y:B$ such that $\varphi(x,y)$. Then we say that $\varphi : A \looparrowright B$ is a function.

Notation: It is convenient to introduce special variables, $p, q, \dots$ for functions. If
$\varphi : A \looparrowright B$
is a function, then we relabel as
$p : A \looparrowright B$
instead, and the function notation
$p(x) = y$
is short for $\varphi(x,y)$.

2. Axioms of $\mathsf{SEAR}$

The first three axioms of  $\mathsf{SEAR}$ are:
Axiom 0 (Non-Triviality).
$(\exists A: \mathsf{Set})(\exists x : A ) (x = x)$. 
Axiom 1 (Relational Comprehension).
$(\forall A: \mathsf{Set})(\forall B: \mathsf{Set}) (\exists! \varphi : A \looparrowright B) (\forall x :A)(\forall y : B)(\varphi(x,y) \leftrightarrow P(x,y))$
Axiom 2 (Tabulations)
$(\forall A : \mathsf{Set})(\forall B: \mathsf{Set})(\forall \varphi : A \looparrowright B)(\exists C: \mathsf{Set})(\exists p : C \looparrowright A)(\exists q : C \looparrowright B)$
such that:
$(\forall x: A)(\forall y : B) (\varphi(x,y) \leftrightarrow (\exists r: C)(p(r) = x \wedge q(r) = y)$
$(\forall r:C)(\forall s:C) ((p(r) = p(s) \wedge q(r) = q(s)) \to r = s)$
The second axiom, Axiom 1 (Relational comprehension) is an axiom scheme. We may put for $P(x,y)$ any $L_{\mathsf{SEAR}}$-formula $\theta$ (so long as the relation variable $\varphi$ is not free in $\theta$).

The third axiom, Axiom 2, asserts, in intuitive set-theoretic lingo, that given a relation
$R \subseteq A \times B$
we have a set
$C : = \{(x,y) \in A \times B \mid Rxy\}$
which is the set of "ordered pairs" in $R$. But the theory does not assume ordered pairs of elements as a primitive notion. So, to do this, Axiom 2 asserts the existence of a "tabulation"
$C, p, q$
(of the appropriate types) where the functions $p : C \to A$ and $q : C \to B$ project, for any pair $(x,y) \in C$, the first and second components of the pair.


3. Existence of Empty Set

Theorem 1. $\mathsf{SEAR} \vdash (\exists C:\mathsf{Set})(\forall y:C)(y \neq y)$

This theorem asserts the existence of an empty set.

Proof: Here is an informal proof based on the one at nLab (Theorem 1 too there).
By Axiom 0, we have $A: \mathsf{Set}$ and $\exists x : A$ with $x = x$.
By Axiom 1, we may assert the existence and uniqueness of the relation
$\varphi : A \looparrowright A$
such that
$\varphi(x,y) \leftrightarrow \bot$,
for all $x, y : A$. Let us call this relation $\Phi$. So,
$(\forall x :A)(\forall y : A)(\Phi(x,y) \leftrightarrow \bot)$.
By Axiom 2, we can assert the existence of a tabulating set
$C: \mathsf{Set}$
and projection functions
$p : C \looparrowright A$,
$q : C \looparrowright A$
such that
$(\forall x: A)(\forall y : A) (\Phi(x,y) \leftrightarrow (\exists r: C)(p(r) = x \wedge q(r) = y))$.
And so, for all $x: A$, for all $y : A$,
$\bot \leftrightarrow (\exists r: C)(p(r) = x \wedge q(r) = y)$.
Suppose, for a contradiction, we have $(\exists r: C)(r = r)$. So, let $p(r) = a$ and $q(r) = b$, with $a:A$ and $b:A$. Then
$(\exists r: C)(p(r) = a \wedge q(r) = b)$.
And so, $\bot$. Therefore, $\neg (\exists r: C)(r = r)$. So, $C$ is empty. QED.


4. Uniqueness

This proof establishes the existence and uniqueness of an empty relation
$\Phi : A  \looparrowright  A$.
But note that this relation is sort of "attached" to $A$. It establishes the existence of an empty set, namely $C : \mathsf{Set}$, which tabulates $\Phi$.

However, it does not establish the uniqueness of the empty set $\varnothing$.

I'm somewhat bothered by this. I could simply be misunderstanding something quite simple. But if not, then it seems that this kind of non-uniqueness would occur quite generally. The underlying reason for it, I think, is this. As I understand the syntax, it is stipulated from the outset that one cannot express "uniqueness" of a set $A$ satisfying some condition $P$ in this theory. To do this, we would need to write down:
$P(A) \wedge P(B) \to A = B$
But the required identity formula $A = B$, with set variables, is not syntactically allowed.

What's unclear to me then, at bottom, is whether forbidding formulas of the form $A = B$ is mandated by the motivating philosophical/conceptual thought behind structural set theory, or whether it is largely a matter of convenience.

[UPDATE (21 July 2013): I have made a couple of notational revisions.]

Comments

  1. "What's unclear to me then, at bottom, is whether forbidding formulas of the form A=B is mandated by the motivating philosophical/conceptual thought behind structural set theory, or whether it is largely a matter of convenience."

    Jeffrey, Maybe this answers your doubt?
    (from http://ncatlab.org/nlab/show/structural+set+theory):

    "Structural set theory provides a foundation for mathematics which is free of this “superfluous baggage” attendant on theories such as ZF, in which there is lots of information such as whether or not 3∈17 (yes, says von Neumann; no, says Zermelo) which is never used in mathematics. In a structural set theory, the elements (such as 3) of a set (such as ℕ) have no identity apart from their existence as elements of that set, and whatever structure is given to that set by the functions and relations placed upon it. That is, sets (together with other attendant concepts such as elements, functions, and relations) are the “raw material” from which mathematical structures are built. By contrast, theories such as ZF may be called material set theories or membership-based set theories.

    Thus, somewhat paradoxically, it turns out that one of the primary attributes of a structural set theory is that the elements of a set have no “internal” structure; they are only given structure by means of functions and relations. In particular, they are not themselves sets, and by default cannot be elements of any other set (not in the sense that it is false that they are, but in the sense that it is meaningless to ask whether they are), ***so that elements of different sets cannot be compared*** (unless and until extra structure is imposed). Structural set theory thus looks very much like type theory. We contrast it with material set theories such as ZF, in which the elements of sets can have internal structure, and are often (perhaps always) themselves sets."

    ReplyDelete
  2. Thanks, Antonio
    Yes, I know that passage; it's very similar to the one I quote above too, from Mike Shulman:

    "no thing can be given to you as an element of more than one structural-set."

    But it doesn't really seem to answer the question concerning uniqueness of $\varnothing$.

    Suppose $\varnothing_1 : \mathsf{Set}$ and $\varnothing_2: \mathsf{Set}$ satisfy the conditions of being *an* empty set. These structural sets tabulate empty relations $\varphi : A \looparrowright B$, where $\varphi(x,y)$ never holds for $x:A$, $y:B$. These empty sets $\varnothing_1$ and $\varnothing_2$ will be isomorphic or "equivalent", in some relevant category-theoretic sense.

    But I want to know if we have:

    $\varnothing_1 = \varnothing_2$?

    Are they literally the same thing? Or merely "isomorphic"?

    Cheers,

    Jeff

    ReplyDelete
  3. Hi Jeffrey, Thanks.
    Yes, the quote was indeed supposed to answer not the issue of uniqueness, but maybe only your doubt "whether forbidding formulas of the form A=B is mandated by the motivating philosophical/conceptual thought behind structural set theory, or whether it is largely a matter of convenience.". And to me that passage seems to allow for the first answer.

    As for uniqueness, at least for ETCS, here they say that "by ∅ we mean an initial object. I mean any initial object (there can be lots!), although any two are uniquely isomorphic." (from http://boolesrings.org/asafk/2013/on-leinsters-rethinking-set-theory/)

    Antonio

    ReplyDelete
  4. Antonio,

    Right - I think that is indeed the answer, and reading around other formulations (e.g., Makkai's), the non-uniqueness is mandated in structural set theories.

    Cheers,

    Jeff

    ReplyDelete
  5. Jeffrey, as to whether structural set theory allows multiple empty sets: do you have the same reservations about ZFU, where the different Urelements are -- formally -- just distinct memberless items?

    ReplyDelete
  6. Aldo, no, because while atoms/urelemente are empty, they're not sets (or classes). The point of permitting atoms/urelemente is to make set theory applicable to non-sets. In fact, I'd like to treat sui generis mathematicalia as atoms, so every sui generis abstractum $a$ (e.g., a pair, or a cardinal, or a real) is "empty" in the sense that, for all $x$, $x \notin a$.

    But, at the moment, I'm trying gradually to understand the basic picture here behind the notions of a "structural set" versus a "material set", without delving into the complicated algebra used to model subsets, power sets, etc. But I do have an intuition that $\varnothing$ should be unique simpliciter, rather than unique up to isomorphism.

    Cheers,

    Jeff

    ReplyDelete
  7. Your structural theories tell us how to make a building structure designee with easy way thanks for share it personal statement business management .

    ReplyDelete

Post a Comment