nLab axiom of fullness

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Universes

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
propositional 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

Contents

Idea

In set theory and the foundations of mathematics, the axiom of fullness is an axiom intermediate in strength between the existence of power sets and function sets. Of course, these can only be distinguished in constructive mathematics, since classically power sets and function sets are equivalent (at least if you have the set 𝟚={,}\mathbb{2} = \{\top, \bot\}).

Statements

In set theory

The axiom of fullness states that, given any sets XX and YY, there is a set F X,YF_{X,Y} of enough entire relations from XX to YY in this sense:

  • Every element of F X,YF_{X,Y} is an entire relation from XX to YY;
  • If RR is an entire relation from XX to YY, then for some SF X,YS \in F_{X,Y}, SRS \subseteq R.

We have written this in a material fashion; structurally, the axiom says that F X,YF_{X,Y} parametrises enough entire relations in this sense:

  • There is a subset E X,YE_{X,Y} of F X,Y×X×YF_{X,Y} \times X \times Y such that:

    • for every element rr of F X,YF_{X,Y} and every element aa of XX, there is an element bb of YY such that (r,a,b)E X,Y(r,a,b) \in E_{X,Y};

    (we think of E X,YE_{X,Y} as giving the evaluation, as a truth value, of rr, as an entire relation, on the elements aa and bb).

  • If RR is an entire relation from XX to YY, then for some ss in F X,YF_{X,Y}:

    • for every element aa of XX and bb of YY, if (s,a,b)E X,Y(s,a,b) \in E_{X,Y}, then aa is RR-related to bb;

    (we think of ss as an entire relation via E X,YE_{X,Y} and say that it is contained in RR).

In the context of material set theory, the structural axiom is weaker than the material axiom, but they become equivalent in the presence of restricted replacement, which is quite weak.

You can also write down an internal version of fullness by adding arbitrary additional parameters to the structural version above (analogously to the generalisation from power set to power object, although more complicated since F X,YF_{X,Y} is not given by a universal property).

Given function sets, fullness is equivalent to the set theory having sets of inhabited subsets, since an entire relation between AA and BB is a function from AA to the set of inhabited subsets of BB. (Power sets on the other hand are sets of all subsets).

 In dependent type theory

In dependent type theory, given a Russell universe UU, the type of all entire relations between types A:UA:U and B:UB:U is given by the type

R:A×BU x:A( y:AisProp(R(x,y)))×y:A.R(x,y)\sum_{R:A \times B \to U} \prod_{x:A} \left(\prod_{y:A} \mathrm{isProp}(R(x, y))\right) \times \exists y:A.R(x, y)

In general, this type is not U U -small. The axiom of fullness for UU states that the above type is UU-small, and is given by the following inference rules:

ΓA:UΓB:UΓEntRel(A,B):U\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:U}{\Gamma \vdash \mathrm{EntRel}(A, B):U}
ΓA:UΓB:UΓEntRel(A,B) R:A×BU x:A( y:AisProp(R(x,y)))×y:A.R(x,y)type\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:U}{\Gamma \vdash \mathrm{EntRel}(A, B) \equiv \sum_{R:A \times B \to U} \prod_{x:A} \left(\prod_{y:A} \mathrm{isProp}(R(x, y))\right) \times \exists y:A.R(x, y) \; \mathrm{type}}

Similarly, for Tarski universes (U,T)(U, T), the type of all entire relations between UU-small types A:UA:U and B:UB:U is given by the type

R:T(A)×T(B)U x:T(A)( y:T(A)isProp(T(R(x,y))))×y:T(A).T(R(x,y))\sum_{R:T(A) \times T(B) \to U} \prod_{x:T(A)} \left(\prod_{y:T(A)} \mathrm{isProp}(T(R(x, y)))\right) \times \exists y:T(A).T(R(x, y))

There are similar inference rules for strict Tarski universes:

ΓA:UΓB:UΓEntRel(A,B):U\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:U}{\Gamma \vdash \mathrm{EntRel}(A, B):U}
ΓA:UΓB:UΓT(EntRel(A,B)) R:T(A)×T(B)U x:T(A)( y:T(A)isProp(T(R(x,y))))×y:T(A).T(R(x,y))type\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:U}{\Gamma \vdash T(\mathrm{EntRel}(A, B)) \equiv \sum_{R:T(A) \times T(B) \to U} \prod_{x:T(A)} \left(\prod_{y:T(A)} \mathrm{isProp}(T(R(x, y)))\right) \times \exists y:T(A).T(R(x, y)) \; \mathrm{type}}

For weak Tarski universes, one uses an equivalence of types instead of judgmental equality

ΓA:UΓB:UΓfullness(A,B):T(EntRel(A,B)) R:T(A)×T(B)U x:T(A)( y:T(A)isProp(T(R(x,y))))×y:T(A).T(R(x,y))\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:U}{\Gamma \vdash \mathrm{fullness}(A, B):T(\mathrm{EntRel}(A, B)) \simeq \sum_{R:T(A) \times T(B) \to U} \prod_{x:T(A)} \left(\prod_{y:T(A)} \mathrm{isProp}(T(R(x, y)))\right) \times \exists y:T(A).T(R(x, y))}

and the two inference rules could be reduced down to the element:

fullness: F:U×UU A:U B:UT(F(A,B)) R:T(A)×T(B)U x:T(A)( y:T(A)isProp(T(R(x,y))))×y:T(A).T(R(x,y))\mathrm{fullness}:\sum_{F:U \times U \to U} \prod_{A:U} \prod_{B:U} T(F(A, B)) \simeq \sum_{R:T(A) \times T(B) \to U} \prod_{x:T(A)} \left(\prod_{y:T(A)} \mathrm{isProp}(T(R(x, y)))\right) \times \exists y:T(A).T(R(x, y))

If the dependent type theory does not have any type universes at all, one could still express the axiom of fullness by explicitly postulating the type of all entire relations using inference rules.

Relation to other axioms

In the presence of the usual basic axioms of set theory (in particular, the axioms of bounded separation and pairing in a material set theory and the existence of equalisers and products in a structural set theory), we have:

power sets → fullness → function sets

On the one hand, F X,YF_{X,Y} can be constructed as the subset of the power set 𝒫(X×Y)\mathcal{P}(X \times Y) consisting of all entire relations from XX to YY. On the other hand, the function set Y XY^X may be constructed as a subset of F X,YF_{X,Y} consisting of those elements SS such that SRS \subseteq R for RR (the graph of) some function from XX to YY; (the key here is that S=RS = R must follow when SS is entire and RR is a function). Conversely, if we have function sets, then the axiom of choice states precisely that the function set Y XY^X always qualifies as F X,YF_{X,Y} (although function sets and excluded middle are already sufficient for power sets and thus fullness).

Fullness also follows from function sets in the presence of COSHEP, a fairly strong but constructive (in that it implies no general principle of omniscience) form of the axiom of choice. If PP is a projective set with a surjection p:PXp\colon P \to X (which this axiom asserts must exist), then we may take Y PY^P as F X,YF_{X,Y}, with (r,a,b)E X,Y(r,a,b) \in E_{X,Y} iff, for some cc in PP, p(c)=ap(c) = a and r(c)=br(c) = b.

Note that F X,YF_{X,Y} is not categorical (in the logicians' sense); that is, there may be many sets F,F,F, F', \ldots that all satisfy the axiom without being (in an appropriate sense) equal. This is the downside to adopting the fullness axiom, compared to power sets or function sets; this is also why the internal version is complicated.

As fullness is weaker than power sets in a constructive framework, we may consider it predicative in the sense of the constructive school; this is one reason for adopting it while rejecting power sets.

Definition of the real numbers

One reason for adopting the axiom of fullness instead of (only) function sets is this: it is strong enough to construct the set \mathbb{R} of (located Dedekind) real numbers from the set \mathbb{N} of natural numbers without assuming excluded middle or countable choice. Using function sets, one can easily construct the set C\mathbb{R}_C of Cauchy reals as a subquotient of the function set \mathbb{N}^{\mathbb{N}}. Both classical and constructive mathematicians usually adopt axioms in which one can prove that \mathbb{R} is isomorphic to C\mathbb{R}_C; this is equivalent to a weak countable choice principle AC ,2\mathrm{AC}_{\mathbb{N},2} that follows from either excluded middle (classically accepted) or countable choice. But there are (for example) some Grothendieck toposes in which \mathbb{R} is not isomorphic to C\mathbb{R}_C (as a statement in the Mitchell–Bénabou language), so any sort of constructive mathematics that wants to apply to such toposes cannot rely on this method to define the real numbers object \mathbb{R}.

Of course, in a topos, there are other ways to define \mathbb{R}, but what if you want your theory to also be predicative? If you adopt the fullness axiom, then you can modify the definition of C\mathbb{R}_C to produce a definition of \mathbb{R} without assuming any choice principle. Instead of using \mathbb{N}^{\mathbb{N}}, you use F ,F_{\mathbb{N},\mathbb{N}} instead; \mathbb{R} can be constructed as a subquotient of that set.

Let an element of F ,F_{\mathbb{N},\mathbb{N}} be a multivalued sequence of natural numbers, and fix a bijection ϕ:\phi\colon \mathbb{N} \to \mathbb{Q} between \mathbb{N} and the set \mathbb{Q} of rational numbers. We call such a multivalued sequence rr regular if, whenever i,j,x,yi,j,x,y are natural numbers such that r(i,x)r(i,x) and r(j,y)r(j,y), we have

|ϕ(x)ϕ(y)|1/i+1/j. {|\phi(x) - \phi(y)|} \leq 1/i + 1/j .

(It is common, but not really necessary in the presence of function sets, to use regular sequences instead of the more general Cauchy sequences when defining C\mathbb{R}_C in constructive mathematics, and we follow that here.) We call two regular multivalued sequences r,sr,s equivalent if, whenever i,j,x,yi,j,x,y are natural numbers such that r(i,x)r(i,x) and s(j,y)s(j,y), we have

|ϕ(x)ϕ(y)|1/i+1/j. {|\phi(x) - \phi(y)|} \leq 1/i + 1/j .

Then this defines an equivalence relation on the set of regular multivalued sequences, and the quotient set is \mathbb{R}. (That is, it may be given, in the usual way, the structure of an Archimedean ordered field which is Dedekind complete relative to located pairs of upper and lower sets.)

However, on one hand, if one’s goal is to have the real numbers, the axiom of fullness is overkill: one can simply just postulate the real numbers in any number of ways, such as a real numbers object or a terminal Archimedean ordered field: they contain all real numbers by definition and are Dedekind complete relative to located pairs of upper and lower sets. In dependent type theory, there is also a resizing axiom for Dedekind cuts. On the other hand, in constructive mathematics, the set of real numbers is less well behaved then the locale of real numbers, and it is currently unknown how to define the locale of real numbers with only the axiom of fullness.

References

Last revised on June 14, 2025 at 23:52:46. See the history of this page for a list of all contributions to it.