nLab internal logic of set theory

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

Contents

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 ff with domain AA and codomain BB at an element bBb \in B is the set of all elements aAa \in A such that f(a)=bf(a) = b:

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

This could be thought of in turn as a set S bS_b indexed by the element bBb \in B.

S b{aA|f(a)=b}S_b \coloneqq \{a \in A \vert f(a) = b\}

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

Indexed disjoint unions and cartesian products

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

iIS i{(i,a)|iI,aS 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)(i, f) consisting of an element iIi \in I and a function f:IS if:I \to S_i

iIS i{(i,f)|iI,f:IS 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 SS which has at most one element: every two elements aSa \in S and bSb \in S are equal to each other

isSubsingleton(S)aS.bS.a=b\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 SS with specified element aSa \in S such that every element bSb \in S is equal to aa, or a set SS where there exists an element aSa \in S such that every element bSb \in S is equal to aa.

isSingleton(S)aS.bS.a=b\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:ABf:A \to B, every family of subsingletons is defined such that the fibers of the function f:ABf:A \to B are all subsingletons. However, that is just the requirement that the function f:ABf:A \to B be an injection. Similarly, every family of singletons is equivalently just a bijection f:ABf:A \simeq B.

Support of a set

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

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

image(f){f(a)|aA,f:AB}\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:S1u:S \to 1.

[S]{u(a)|aS,u:S1}[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 SS into a subsingleton.

One could also apply the support to any family of sets (S b) bS(S_b)_{b \in S}, resulting in the family of subsingletons ([S b]) bS([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:

AB[A×B]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:

AB[AB]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:

AB[B A]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:

AB[AB]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:

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

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

bB.S b[ bBS b]\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) bB(S_b)_{b \in B} ranging over the set BB is defined as the support of the indexed cartesian product of the family of subsingletons:

bB.S b[ bBS b]\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 SS is represented by the initial reflexive graph structure on SS. By a graph structure on SS we mean a set RR and a pair of function s:RSs:R \to S and t:RSt:R \to S. The set SS 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 refl:SR\mathrm{refl}:S \to R such that s(refl(a))=as(\mathrm{refl}(a)) = a and t(refl(a))=at(\mathrm{refl}(a)) = a.

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

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

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

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

It could be shown from this universal property that the functions s Ids_\mathrm{Id} and t Idt_\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 PP the double negation of PP implies PP, ¬¬PP\neg \neg P \implies P. The internal law of double negation would say that for every subsingleton SS, the subsingleton ¬¬SS\neg \neg S \implies S is a singleton, or equivalently, that for every set SS there is an element doubleneg S¬¬[S][S]\mathrm{doubleneg}_S \in \neg \neg [S] \implies [S].

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

See also

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction setinternal homfunction type
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian productdependent productdependent product type
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijectionisomorphism/adjoint equivalenceequivalence of types
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

Last revised on October 21, 2022 at 20:07:20. See the history of this page for a list of all contributions to it.