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:

• $\mathsf{ETCS}$: "elementary theory of the category of sets" (long version) (Lawvere 2005)
• $\mathsf{SEAR}$: "sets, elements and relations" (nLab)

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.]