basic constructions:
strong axioms
further
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.
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$:
This could be thought of in turn as a set $S_b$ indexed by the element $b \in B$.
The whole collection of sets $(S_b)_{b \in B}$ is then the family of sets.
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$
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$
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
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$.
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$.
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$
The support of the set is defined as the image of the unique function $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.
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:
The logical disjunction of two subsingletons is defined as the support of the disjoint union of the two subsingletons:
The logical implication of two subsingletons is defined as the support of the function set of the two subsingletons:
The logical equivalence of two subsingletons is defined as the support of the set of bijections of the two subsingletons:
The logical negation of a subsingleton is defined as the support of the function set into the empty set:
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:
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:
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.
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.
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]$.
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Last revised on October 21, 2022 at 20:07:20. See the history of this page for a list of all contributions to it.