nLab internal logic of set theory

Ideas

In any foundational set theory out there, the sets and functions, however defined, form a category. As a result, the set theory should have an internalization of the predicate logic used to define the set theory, the internal logic of the resulting category of sets induced by the subsingletons, the injections, and the support sets of the set theory. This article will describe the internal logic of set theory, in the language of predicate logic over set theory.

Families of sets

We begin with the definition of families of sets and indexed sets. Recall that a fiber or preimage of a function $f$ with domain $A$ and codomain $B$ at an element $b \in B$ is the set of all elements $a \in A$ such that $f(a) = b$:

$$\{a \in A \vert f(a) = b\}$$

This could be thought of in turn as a set $S_b$ indexed by the element $b \in B$.

$$S_b \coloneqq \{a \in A \vert f(a) = b\}$$

The whole collection of sets $(S_b)_{b \in B}$ is then the family of sets.

Indexed disjoint unions and cartesian products

Given a family of sets $(S_i)_{i \in I}$ indexed by the set $I$, the indexed disjoint union is defined as the set of all pairs $(i, a)$ consisting of an element $i \in I$ and an element $a \in S_i$

$$\biguplus_{i \in I} S_i \coloneqq \{(i, a) \vert i \in I, a \in S_i\}$$

The indexed cartesian product is defined as the set of all pairs $(i, f)$ consisting of an element $i \in I$ and a function $f:I \to S_i$

$$\prod_{i \in I} S_i \coloneqq \{(i, f) \vert i \in I, f:I \to S_i\}$$

Subsingletons and singletons

A subsingleton is a set $S$ which has at most one element: every two elements $a \in S$ and $b \in S$ are equal to each other

$$\mathrm{isSubsingleton}(S) \coloneqq \forall a \in S.\forall b \in S. a = b$$

A singleton is a pointed subsingleton. Equivalently, a singleton is a pointed set $S$ with specified element $a \in S$ such that every element $b \in S$ is equal to $a$, or a set $S$ where there exists an element $a \in S$ such that every element $b \in S$ is equal to $a$.

$$\mathrm{isSingleton}(S) \coloneqq \exists a \in S.\forall b \in S. a = b$$

Every subsingleton is a subset of a singleton.

In the internal logic of set theory, subsingletons represent the internal propositions, families of subsingletons represent the internal predicates, the empty set represents the internal truth value false, and singletons represent the internal truth value true.

Since any family of sets is defined by the fibers of a function $f:A \to B$, every family of subsingletons is defined such that the fibers of the function $f:A \to B$ are all subsingletons. However, that is just the requirement that the function $f:A \to B$ be an injection. Similarly, every family of singletons is equivalently just a bijection $f:A \simeq B$.

Support of a set

Every set $S$ has a unique function $u:S \to 1$ into any singleton $1$ with point $* \in 1$, defined by $u(a) = *$ for all elements $a \in S$.

Recall that the image of a function $f:A \to B$ is the subset of all elements $b \in B$ which are of the form $f(a)$ for all elements $a \in A$

$$\mathrm{image}(f) \coloneqq \{f(a) \vert a \in A, f:A \to B\}$$

The support of the set is defined as the image of the unique function $u:S \to 1$.

$$[S] \coloneqq \{u(a) \vert a \in S, u:S \to 1\}$$

Since the image is always a subset of the codomain of the function, the support of a set is thus a subsingleton. The support enables us to make every set $S$ into a subsingleton.

One could also apply the support to any family of sets $(S_b)_{b \in S}$, resulting in the family of subsingletons $([S_b])_{b \in S}$. Since every family of subsingletons is equivalently an injection, this is the same as the usual image factorization of every function into an injection and a surjection.

Internal logical operators

Supports are important because they will allow us to define the logical operators conjunction, disjunction, implication, logical equivalence, negation, existential quantification, and universal quantification internal to the set theory:

The logical conjunction of two subsingletons is defined as the support of the cartesian product of the two subsingletons:

$$A \wedge B \coloneqq [A \times B]$$

The logical disjunction of two subsingletons is defined as the support of the disjoint union of the two subsingletons:

$$A \vee B \coloneqq [A \uplus B]$$

The logical implication of two subsingletons is defined as the support of the function set of the two subsingletons:

$$A \implies B \coloneqq [B^A]$$

The logical equivalence of two subsingletons is defined as the support of the set of bijections of the two subsingletons:

$$A \iff B \coloneqq [A \simeq B]$$

The logical negation of a subsingleton is defined as the support of the function set into the empty set:

$$\neg A \coloneqq [\emptyset^A]$$

The logical existential quantification of a family of subsingletons $(S_b)_{b \in B}$ ranging over the set $B$ is defined as the support of the indexed disjoint union of the family of subsingletons:

$$\exists b \in B.S_b \coloneqq \left[\biguplus_{b \in B} S_b\right]$$

The logical universal quantification of a family of subsingletons $(S_b)_{b \in B}$ ranging over the set $B$ is defined as the support of the indexed cartesian product of the family of subsingletons:

$$\forall b \in B.S_b \coloneqq \left[\prod_{b \in B} S_b\right]$$

All these operations are not restricted only to subsingletons, they are also defined over general sets. However, by definition, these operations result in a subsingleton.

Internal equality

The internal equality relation in a set $S$ is represented by the initial reflexive graph structure on $S$. By a graph structure on $S$ we mean a set $R$ and a pair of function $s:R \to S$ and $t:R \to S$. The set $S$ is called the carrier set of the graph structure. We do not assume the two functions are jointly injective, so the graph structures are really directed pseudograph structures. By a reflexive graph structure, we mean that every element of the carrier set has a loop: there is a function $\mathrm{refl}:S \to R$ such that $s(\mathrm{refl}(a)) = a$ and $t(\mathrm{refl}(a)) = a$.

A graph structure homomorphism between two graph structures on the carrier set $S$, $(R, s, t)$ and $(R,', s', t')$ is a function $f: R \to R'$, such that for all $p \in R$, $s'(f(p)) = s(p)$ and $t'(f(p)) = t(p)$.

A reflexive graph structure homomorphism is a graph structure homomorphism $f:R \to R'$ between two graph structures $(R, s, t, \mathrm{refl})$ and $(R', s', t', \mathrm{refl}')$ on a carrier set $S$ where additionally, for every element $a \in S$ of the carrier set, $f(\mathrm{refl}(a)) = \mathrm{refl}'(f(a))$.

A reflexive graph structure $(\mathrm{Id}_S, s_{\mathrm{Id}}, t_{ \mathrm{Id}}, \mathrm{refl}_S)$ on a carrier set $S$ is an initial reflexive graph structure on $S$ if for every other reflexive graph structure $(R, s, t, \mathrm{refl})$ on $S$, there exists a unique reflexive graph structure homomorphism $f:\mathrm{Id}_S \to R$.

Every set $S$ has an initial reflexive graph structure given by the diagonal function of $S$.

It could be shown from this universal property that the functions $s_\mathrm{Id}$ and $t_\mathrm{Id}$ are jointly injective, and thus that axiom K holds internally in set theory.

Internal and external axioms

Since every logical operation in predicate logic have been internalized in the set theory itself, one then has to distinguish between the axioms written in the external predicate logic used to define the set theory, and the axioms written in the predicate logic internal to the set theory.

For example, the external law of double negation states that for any proposition $P$ the double negation of $P$ implies $P$, $\neg \neg P \implies P$. The internal law of double negation would say that for every subsingleton $S$, the subsingleton $\neg \neg S \implies S$ is a singleton, or equivalently, that for every set $S$ there is an element $\mathrm{doubleneg}_S \in \neg \neg [S] \implies [S]$.

Similarly, the external law of excluded middle states that for any proposition $P$ it is possible to derive that $P \vee \neg P$. The internal law of excluded middle would say that for every for every subsingleton $S$, the subsingleton $S \vee \neg S$ is a singleton, or equivalently, that for every set $S$, there is a element $\mathrm{lem}_S \in[S] \vee \neg [S]$.

See also

• split support
• internal logic
• dependent type theory
• propositions as types
• Trimble on ETCS II

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logic	set theory (internal logic of)	category theory	type theory
proposition	set	object	type
predicate	family of sets	display morphism	dependent type
proof	element	generalized element	term/program
cut rule		composition of classifying morphisms / pullback of display maps	substitution
introduction rule for implication		counit for hom-tensor adjunction	lambda
elimination rule for implication		unit for hom-tensor adjunction	application
cut elimination for implication		one of the zigzag identities for hom-tensor adjunction	beta reduction
identity elimination for implication		the other zigzag identity for hom-tensor adjunction	eta conversion
true	singleton	terminal object/(-2)-truncated object	h-level 0-type/unit type
false	empty set	initial object	empty type
proposition, truth value	subsingleton	subterminal object/(-1)-truncated object	h-proposition, mere proposition
logical conjunction	cartesian product	product	product type
disjunction	disjoint union (support of)	coproduct ((-1)-truncation of)	sum type (bracket type of)
implication	function set (into subsingleton)	internal hom (into subterminal object)	function type (into h-proposition)
negation	function set into empty set	internal hom into initial object	function type into empty type
universal quantification	indexed cartesian product (of family of subsingletons)	dependent product (of family of subterminal objects)	dependent product type (of family of h-propositions)
existential quantification	indexed disjoint union (support of)	dependent sum ((-1)-truncation of)	dependent sum type (bracket type of)
logical equivalence	bijection set	object of isomorphisms	equivalence type
	support set	support object/(-1)-truncation	propositional truncation/bracket type
		n-image of morphism into terminal object/n-truncation	n-truncation modality
equality	diagonal function/diagonal subset/diagonal relation	path space object	identity type/path type
completely presented set	set	discrete object/0-truncated object	h-level 2-type/set/h-set
set	set with equivalence relation	internal 0-groupoid	Bishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
	equivalence class/quotient set	quotient	quotient type
induction		colimit	inductive type, W-type, M-type
higher induction		higher colimit	higher inductive type
-		0-truncated higher colimit	quotient inductive type
coinduction		limit	coinductive type
	preset		type without identity types
	set of truth values	subobject classifier	type of propositions
domain of discourse	universe	object classifier	type universe
modality		closure operator, (idempotent) monad	modal type theory, monad (in computer science)
linear logic		(symmetric, closed) monoidal category	linear type theory/quantum computation
proof net		string diagram	quantum circuit
(absence of) contraction rule		(absence of) diagonal	no-cloning theorem
		synthetic mathematics	domain specific embedded programming language