foundations

# Contents

## Idea

In this article we introduce a structural set theory consisting of four basic primitives, sets, elements, functions, and relations, as well as function evaluation, and relation holding, and structural versions of 9 of the 10 axioms of ZFC presented in the nLab article of ZFC, making the set theory equivalent in strength to ZFC. We propose that structural ZFC is a suitable theory for practical foundations, as the primitives and axioms are in alignment with the usage of such objects in mathematical practice, rather than coming with its own additional baggage.

## Presentation

We work in a first-order logic with equality. In structural ZFC, there are four basic primitives:

• sets $A$

• for every set $A$, elements $a \in A$ (the membership $\in$ here is a typing judgment, rather than a relation)

• for every set $A$ and $B$, functions $f:A \to B$ with domain $A$ and codomain $B$ (the function notation $f:A \to B$ here is a judgment, rather than a relation)

• for every set $A$ and $B$, relations $\varphi:A \looparrowright B$ with domain $A$ and codomain $B$ (the relation notation $\varphi:A \looparrowright B$ here is a judgment, rather than a relation)

• for every function $f:A \to B$ and element $a \in A$, one could form the element $f(a) \in B$; this operation is called function evaluation,
• for every relation $\varphi:A \looparrowright B$ and element $a \in A$ and $b \in B$, one could form that $\varphi(a, b)$ holds of $a$ and $b$.

The axioms of structural ZFC are as follows:

Axiom 0A (Axiom of equality preservation): For all sets $A$ and $B$, functions $f:A \to B$, and elements $a \in A$ and $b \in A$, if $a = b$, then $f(a) = f(b)$.

Axiom 0B (Axiom of unique choice): For all functions $f:A \to B$, there is a unique relation $\varphi:A \looparrowright B$ such that for all $a \in A$, $\varphi(a, f(a))$ holds of $a$ and $f(a)$, and for all relations $\varphi:A \looparrowright B$ such that for all $a \in A$, there is a unique $b \in B$ such that $\varphi(a, b)$ holds of $a$ and $b$, there is a function $f:A \to B$ such that $f(a) = b$.

A function $f:A \to B$ is an injection if for all elements $a \in A$ and $b \in A$, $a = b$ if and only if $f(a) = f(b)$. Injections are written as $f:A \hookrightarrow B$.

Axiom 1 (Axiom of strong extensionality): Given sets $A$ and $B$ and an injection $i:A \hookrightarrow B$, the following statements are logically equivalent to each other:

• there exists a function $i^{-1}:B \to A$ such that for all elements $a \in A$ and $b \in B$, $i^{-1}(i(a)) = a$ and $i(i^{-1}(b)) = b$
• for every element $x \in B$ there exists an element $y \in A$ such that $i(y) = x$

One uses the axiom of strong extensionality as the definition of a bijection between sets.

Axiom 2 (Axiom of empty set): There exists a set $\emptyset$ such that for every other set $A$, there is a unique relation $u_A^\emptyset:\emptyset \looparrowright A$.

Axiom 3 (Axiom of Cartesian products): For every set $A$ and $B$, there exists a set $A \times B$ with a function $\pi_A:A \times B \to A$ and a function $\pi_B:A \times B \to B$ such that for every element $a \in A$ and $b \in B$ there is a unique element $(a, b) \in A \times B$, such that $\pi_A((a, b)) = a$ and $\pi_B((a, b)) = b$.

Given a set $I$, an $I$-indexed family of subsets is a relation $M:I \looparrowright A$ to a set $A$ called the union of $M$.

Axiom 4 (Axiom of indexed subsets): For every set $I$ and $I$-indexed family of subsets $M:I \looparrowright A$ with union $A$, and for every element $i \in I$, there exists a set $M_i$ and an injection $m:M_i \hookrightarrow A$, such that for every element $a \in M_i$, $M(i, m(a))$ holds for $i$ and $m(a)$, and for every other set $B$ with injection $f:B \hookrightarrow A$ such that for every element $b \in B$, $M(i, f(b))$ holds for $i$ and $f(b)$, there is a unique function $u_B^{M_i}:B \to M_i$ such that for every element $b \in B$, $f(b) = m(u_B^{M_i}(b))$.

Axiom 5 (Axiom schema of separation): For any set $B$ and any formula $\phi(x)$ with free variable $x \in B$, there exists a set $\{B \vert \phi\}$ with an injection $m:\{B \vert \phi\} \hookrightarrow B$ such that for every element $x \in B$, $\phi(x)$ holds if and only if there exists an element $y \in \{B \vert \phi\}$ such that $m(y) = x$.

Axiom 6 (Axiom schema of collection): For any set $A$ and formula $\phi(x, X)$ with free variables $x \in A$ and $X$, there exists a set $B$, function $p:B \to A$, and a $B$-indexed family of sets $M:B \looparrowright C$ with union $C$, such that for every $b \in B$, $\phi(p(b), M_b)$, and for every $a \in A$, if there exists a set $X$ with $\phi(a, X)$, then $a \in \mathrm{im}(p)$.

Axiom 7 (Axiom of power sets): For any set $A$, there exists a set $\mathcal{P}(A)$ and a relation $(-)\in_A(-):A\looparrowright \mathcal{P}(A)$ such that for any set $B$ with injection $i:B \hookrightarrow A$, there exists a unique $b \in \mathcal{P}(A)$ such that for any $x \in A$, $x \in_A b$ holds of $x$ and $b$ if and only if there exists an element $y \in B$ such that $i(y) = x$.

Axiom 8 (Axiom of natural numbers): There exists a set $\mathbb{N}$ with an element $0 \in \mathbb{N}$ and a function $s:\mathbb{N} \to \mathbb{N}$, such that for all sets $A$ with an element $0_A:A$ and function $s_A:A \to A$, there is a unique function $u_A^\mathbb{N}:\mathbb{N} \to A$ such that $u_A^\mathbb{N}(0) = 0_A$ and for all elements $n \in \mathbb{N}$, $u_A^\mathbb{N}(s(n)) = s_A(u_A^\mathbb{N}(n))$.

Axiom 9 (Axiom of choice): If $f:A \to B$ is a function such that for every element $x \in B$ there exists an element $y \in A$ such that $f(y) = x$, then there is a function $g:B \to A$ such that for all elements $x \in B$, $f(g(x)) = x$.

The structural version of the axiom of foundation, the axiom of well-founded materialization, states that every set can be embedded in some well-founded extensional graph. This axiom follows from the axiom of choice, and well-founded extensional graphs are not a fundamental concept in structural set theory, so it is not listed here as a separate axiom.

## Making alternate primitive choices

One could choose to make either the relations or the functions a derived object of the other, leading to categorical ZFC and allegorical ZFC respectively.

### Dependently-sorted categorical ZFC

Categorical ZFC follows ETCS with elements in taking functions to be fundamental and relations as defined.

We work in a first-order logic with equality. In structural ZFC, there are three basic primitives:

• sets $A$

• for every set $A$, elements $a \in A$ (the membership $\in$ here is a typing judgment, rather than a relation)

• for every set $A$ and $B$, functions $f:A \to B$ with domain $A$ and codomain $B$ (the function notation $f:A \to B$ here is a judgment, rather than a relation)

In addition, for every function $f:A \to B$ and element $a \in A$, one could form the element $f(a) \in B$; this operation is called function evaluation. A relation between sets $A$ and $B$ is a set $R$ with an injection $(s, t):R \hookrightarrow A \times B$.

### Three-sorted categorical ZFC

An alternate formulation of categorical ZFC three sorts, one for sets, elements, and functions, making structural ZFC into a three-sorted set theory. The membership $a \in A$ becomes a relation between the sort of elements and the sort of sets, while the functional domain and codomain notation $f:A \to B$ also becomes a ternary relation between the sort of functions, and two copies of the sort of sets. There is a quinary relation $\mathrm{eval}(A, B, f, a, b)$ between all three sorts, which says that given sets $A$ and $B$, the function $f$ can be evaluated at element $a$ and the result of the evaluation is the element $b$, in the context of $\varphi:A \looparrowright B$, $a \in A$, and $b \in B$.

### Dependently sorted allegorical ZFC

Allegorical ZFC follows SEAR in taking relations to be fundamental and functions as defined.

We work in a first-order logic with equality. In structural ZFC, there are three basic primitives:

• sets $A$

• for every set $A$, elements $a \in A$ (the membership $\in$ here is a typing judgment, rather than a relation)

• for every set $A$ and $B$, relations $\varphi:A \looparrowright B$ with domain $A$ and codomain $B$ (the relation notation $\varphi:A \looparrowright B$ here is a judgment, rather than a relation)

In addition, for every relation $\varphi:A \looparrowright B$ and element $a \in A$, one could form the judgment that $\varphi(a, b)$ holds. A function is a relation $\varphi:A \looparrowright B$ such that for all $a \in A$, there is a unique element $b \in B$ such that $\varphi(a, b)$ holds, and $b$ is said to be the evaluation of $a$ at $\varphi$.

### Three-sorted allegorical ZFC

An alternate formulation of allegorical ZFC uses three sorts, one for sets, elements, and relations, making SEAR into a three-sorted set theory. The membership $a \in A$ becomes a relation between the sort of elements and the sort of sets, while the relational domain and codomain notation $\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 $\mathrm{holds}(A, B, \varphi, a, b)$ between all three sorts, which says that given sets $A$ and $B$, the relation $\varphi$ holds for element $a$ and $b$ in the context of $\varphi:A \looparrowright B$, $a \in A$, and $b \in B$.