nLab axiom of separation

Redirected from "comprehension rule".
Axiom schemes of separation

This is about the axiom of separation in set theory. For the axioms in topology also called “separation”, see separation axioms.


Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

(0,1)(0,1)-Category theory

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

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
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity 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 set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
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

homotopy levels

semantics

Axiom schemes of separation

Idea

In set theory, the axiom scheme of separation aka specification states that, given any set XX and any property PP of the elements of XX, there is a set

{X|P}={aX|P(a)} \{ X | P \} = \{ a \in X \;|\; P(a) \}

consisting precisely of those elements of XX for which PP holds:

a{X|P}aXP(a). a \in \{ X | P \} \;\leftrightarrow\; a \in X \;\wedge\; P(a) .

Note that {X|P}\{X|P\} is a subset of XX.

It is important to specify what language PP can be written in. This connects the axiom to logic and the foundations of mathematics. Arguably, first-order logic developed in order to explain the meaning of Ernst Zermelo's axiom of separation (although Zermelo himself disagreed with the interpretation that this gave). Separation is (usually) given as an axiom scheme because there is one axiom for each way to state a property in the language. (We also allow parameters in PP.)

Statements

From weaker to stronger:

  • For bounded separation aka restricted separation aka Δ 0\Delta_0-separation, PP must be written in the language of first-order set theory and all quantifications must be guarded by a set: of the form xA\forall x \in A or xA\exists x \in A for some set AA.

  • For limited separation aka Δ 0 𝒫\Delta_0^{\mathcal{P}}-separation, PP must be written in the language of first-order set theory and all quantifications must be guarded by a set or a power class: of the form xA\forall x \in A, BA\exists B \subseteq A, etc. Limited separation trivially implies bounded separation, while bounded separation implies limited separation if power sets exist.

  • For full separation aka simply separation, PP must be written in the language of first-order set theory, but otherwise anything goes; in a class theory, PP must be guarded by a class. Full separation trivially implies limited separation.

  • For large separation, PP must be written in the language of first-order class theory; of course, this only makes sense in a class theory. The difference in strength between the class theories MKMK and NBGNBG is precisely that the former has large separation but the latter does not.

  • Separation is sometimes called restricted comprehension; for full comprehension, a.k.a. simply comprehension, no set XX needs to be given ahead of time. Full comprehension was proposed by Gottlob Frege, but leads to Russell's paradox. However, full comprehension can sometimes be allowed if the ambient logic is nonclassical, such as linear logic or paraconsistent logic.

  • For stratified comprehension, no set XX is given, but PP is restricted to stratified formulas, in which each variable xx can be given a consistent natural number σ(x)\sigma(x) (its stratification) such that xyx \in y appears in the formula only if σ(y)=σ(x)+1\sigma(y) = \sigma(x) + 1. This is used in Van Quine's New Foundations.

In structural set theory

Set theory is usually given in material form, with a language based on a global membership relation \in, and we have implicitly followed this above. However, separation makes sense also in structural set theory (although full comprehension does not, except in a structural class theory with a class of all sets, where it again leads to paradox). The conclusion of the axiom is the existence of a set

{X|P}={a:X|P(a)} \{ X | P \} = \{ a\colon X \;|\; P(a) \}

and an injection i P:{X|P}Xi_P\colon \{X|P\} \to X such that

b:S,a=i P(b)P(a). \exists b\colon S,\; a = i_P(b) \;\leftrightarrow\; P(a) .

Note that {X|P}\{X|P\}, equipped with i Pi_P, is a subset of XX in the structural sense.

The structural axioms can of course be stated even in a material set theory, where they are actually weaker than the corresponding material axioms; however, the material axioms follow (as usual) from the structural axioms using restricted replacement, which is quite weak (and also follows from the material form of limited separation).

If a structural set theory is given by stating axioms for the category of sets, then restricted separation amounts to the property that this category is a Heyting category. If it is an elementary topos, then since it satisfies the power set axiom, this implies limited separation as well. Full separation is somewhat less natural to state category-theoretically, but the combination of full separation with the structural axiom of collection is equivalent to saying that the category of sets is autological? (see here for now for a definition of autological categories).

The axiom schema of restricted separation is formally expressed by the rules

ΓSsetΓ,xSP(x)propΓ{xS|P(x)}set\frac{\Gamma \vdash S \; \mathrm{set} \quad \Gamma, x \in S \vdash P(x) \; \mathrm{prop}}{\Gamma \vdash \{x \in S \vert P(x)\} \; \mathrm{set}}
ΓSsetΓ,xSP(x)propΓi:{xS|P(x)}S\frac{\Gamma \vdash S \; \mathrm{set} \quad \Gamma, x \in S \vdash P(x) \; \mathrm{prop}}{\Gamma \vdash i:\{x \in S \vert P(x)\} \to S}
ΓSsetΓ,xSP(x)propΓ,y{xS|P(x)},z{xS|P(x)},i(y)=i(z)truey=ztrue\frac{\Gamma \vdash S \; \mathrm{set} \quad \Gamma, x \in S \vdash P(x) \; \mathrm{prop}}{\Gamma, y \in \{x \in S \vert P(x)\}, z \in \{x \in S \vert P(x)\}, i(y) = i(z) \; \mathrm{true} \vdash y = z \; \mathrm{true}}
ΓSsetΓ,xSP(x)propΓ,xR,y{xS|P(x)}.x=i(y)trueP(x)true\frac{\Gamma \vdash S \; \mathrm{set} \quad \Gamma, x \in S \vdash P(x) \; \mathrm{prop}}{\Gamma, x \in R, \exists y \in \{x \in S \vert P(x)\}.x = i(y) \; \mathrm{true} \vdash P(x) \; \mathrm{true}}
ΓSsetΓ,xSP(x)propΓ,xR,P(x)truey{xS|P(x)}.x=i(y)true\frac{\Gamma \vdash S \; \mathrm{set} \quad \Gamma, x \in S \vdash P(x) \; \mathrm{prop}}{\Gamma, x \in R, P(x) \; \mathrm{true} \vdash \exists y \in \{x \in S \vert P(x)\}.x = i(y) \; \mathrm{true}}

In dependent type theory

In dependent type theory, it is possible to define a Tarski universe (V,)(V, \in) of pure sets which behaves as a material set theory. The universal type family of the Tarski universe is given by the type family x:V y:Vyxx:V \vdash \sum_{y:V} y \in x. The axiom schema of separation is given by the following inference rule:

Γ,x:Vϕ(x)typeΓseperation V ϕ():( x:VisProp(ϕ(x))) a:V S:V x:V(xa)(ϕ(x)(xS))\frac{\Gamma, x:V \vdash \phi(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{seperation}_V^{\phi(-)}:\left(\prod_{x:V} \mathrm{isProp}(\phi(x))\right) \to \prod_{a:V} \sum_{S:V} \prod_{x:V} (x \in a) \to (\phi(x) \simeq (x \in S))}

In hyperdoctrines

Lawvere’s definition

Lawvere gives a definition (Lawvere70, p. 12-13) of comprehension in hyperdoctrines.

Definition

Let p:EBp \colon E \to B be a bifibration over the category BB, and assume that each fibre E XE_X of EE has a terminal object T XT_X. For any morphism t:YXt \colon Y \to X in BB, define the image imtim t of tt to be the pushforward (dependent sum) t !T Yt_! T_Y. This gives rise to a functor im:B/XE Xim \colon B/X \to E_X for each XX. Then EE is said to have comprehension, or to satisfy the comprehension schema, if each image functor has a right adjoint {}:E XB/X\{-\} \colon E_X \to B/X.

Remark

This means that for each PE XP \in E_X there is a morphism i P:{P}Xi_P \colon \{ P \} \to X in BB such that there is a bijection between commuting triangles t=i Ptt = i_P \circ t' in BB and morphisms imtPim t \to P in E XE_X. Lawvere calls the morphism {P}X\{P\} \to X the extension of PP, so that one could say that EE satisfies the comprehension schema if the extensions of all predicates exist.

Ehrhard’s reformulation

Notice that, in the above situation, morphisms imtP\im t \to P in E XE_X are in bijection with morphisms T Yt *PT_Y \to t^* P in E YE_Y, and that these are the same as morphisms T YPT_Y \to P in the total category EE that lie over tt. This leads to an alternative formulation of the definition, originally considered by Ehrhard 1988 (see also Jacobs 1993, Jacobs 99), which does not depend on pp being a bifibration.

Suppose the fibres E XE_X have terminal objects that are preserved by the reindexing functors. This is equivalent to saying that p:EBp:E\to B has a section T:BET:B\to E taking each object XX to a terminal object T XT_X of E XE_X and each morphism to a cartesian arrow; such a functor is then automatically fully faithful and right adjoint to p:EBp:E\to B. If BB has a terminal object 11, then this is additionally equivalent to saying that the entire category EE has a terminal object T 1T_1 preserved by pp, since then X *(T 1)X^*(T_1) will be terminal in E XE_X by combining the universal properties of X *X^* and T 1T_1. Note also that if pp is a bifibration, as in Lawvere’s definition, then the reindexing functors are right adjoints and hence automatically preserve all terminal objects.

Comprehension in the sense above is equivalent to the existence of a further right adjoint to the terminal-object functor T:BET:B\to E.

The implication from Lawvere’s definition to Ehrhard’s is clear. Conversely, if a fibration p:EBp \colon E \to B satisfies the Ehrhard definition, then there is a bijection between morphisms T YPT_Y \to P in EE and morphisms Y{P}Y \to \{P\} in BB. One must then show that the composite of this last with the canonical {P}X\{P\} \to X (given by pp applied to the counit T {P}PT_{\{P\}} \to P) is equal to pp applied to the morphism Y{P}Y \to \{P\}, thus giving a morphism in B/XB/X of the right sort. But in fact the morphism Y{P}Y \to \{P\} is unique with the property that applying the functor T T_{-} and composing with the counit gives the morphism T YPT_Y \to P, by the counit’s universal property, and applying pp to this commuting triangle in EE produces the required one in BB.

Examples

Subsets

The tautological example which is useful to see what the abstract definition by Lawvere axiomatizes is the following.

Let B=B = Set be the category of sets and for XX a set let E XE_X be the poset of subsets of XX, regarded as the propositions about elements in XX. Then comprehension exists and is given by sending a subset of XX regarded as an object of E XE_X (hence regarded as a proposition) to the same subset, but now regarded as a monomorphism in Set into XX.

More generally, the same construction works for the posets of subobjects in any regular category.

Presheaves

There is a functor Cat 1 opCAT 1Cat_1^{op} \to CAT_1, from the large 1-category of categories and functors to the ‘very large’ 1-category of large categories and functors, that sends a category CC to the category of presheaves [C op,Set][C^{op}, Set] on CC, and a functor F:CDF \colon C \to D to the pullback functor F *:[D op,Set][C op,Set]F^* \colon [D^{op}, Set] \to [C^{op}, Set]. These pullback functors have left and right adjoints given by Kan extension.

Lawvere 70 shows that this fibration has comprehension, with the extension of a presheaf given by its category of elements together with the canonical projection from this to the base category.

In dependent linear type theory

If the hyperdoctrine has linear type theories/symmetric monoidal categories as fibers, then it is more natural to consider in def. not the terminal object in some fiber (if any) but the tensor unit (which of course happens to be the terminal object in the case of cartesian monoidal) fibers.

In this case then the image functor in def. is

Σ X:(YfX)f1 Y. \Sigma_X \;\colon\; (Y \stackrel{f}{\to} X) \mapsto \underset{f}{\sum} 1_Y \,.

If this has a right adjoint R XR_X, hence if we have linear comprehension according to def. , then the induced comonad

! XΣ XR X !_X \coloneqq \Sigma_X \circ R_X

is (the dependent version of) the canonical categorical interpretation of the exponential modality of linear logic. See at dependent linear type theory – The canonical co-modality for more.

The comprehensive factorization system

If the extension functors E XB/XE_X \to B/X are fully faithful, then together they make EE into a ‘fibrewise reflective’ subfibration of the codomain fibration of BB, which is a reflective subfibration if the image functors preserve pullbacks. (See stable factorization system.)

Call a morphism of the form {P}X\{P\} \to X a subtype inclusion. Every morphism t:YXt \colon Y \to X of BB factors through one such by means of the unit η t\eta_t of the adjunction im{}im \dashv \{-\}:

Y η t {imt} t i t X \array{ Y & & \overset{\eta_t}{\to} & & \{ im t \} \\ & \mathllap{t}\searrow & & \swarrow\mathrlap{i_t} & \\ & & X & & }

This gives rise to an orthogonal factorization system precisely when each η t\eta_t is orthogonal to all subtype inclusions. It is shown by (Carboni et. al., section 2.12) that this holds if and only if subtype inclusions are closed under composition.

For the subobject fibration of a regular category, this gives the usual (regular epi, mono) factorization system, while for the fibration of presheaves over CatCat it gives the factorization of a functor into a final functor followed by a discrete fibration. (See also comprehensive factorization for a description of the latter as a factorization system in a 2-category.)

Axiom or axiom scheme?

Although usually presented as an axiom scheme, in many cases, all instances of separation follow from finitely many special cases (which can then be packaged into a single axiom, using conjunction, although this is probably pointless). This is the case, for example, in ETCS (a structural set theory that satisfied bounded separation) and NBG (a material class theory that satisfies full separation). In type-theoretic foundations of mathematics, separation is usually invisible, but again some form (generally only bounded) can again be proved from a few specific axioms or constructions.

Relation to the axiom of replacement

Full separation follows from the axiom of replacement and the principle of excluded middle (along with the axiom of the empty set). Therefore, the axiom is often left out entirely of a description of ZFC (the usually accepted foundation of mathematics). In versions of set theory for constructive mathematics, however, we often have replacement but only bounded or limited separation, and in any case separation must be listed explicitly.

References

General

(…)

In hyperdoctrines

On the relation between comprehension schemes and factorisation systems:

Discussion in ( , 1 ) (\infty,1) -category theory:

Last revised on February 28, 2024 at 02:48:21. See the history of this page for a list of all contributions to it.