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 ).
The axiom of subset collection combines fullness with the axiom of collection to apply in the situations where fullness is used. In the presence (I think) of either collection or full separation, subset collection is equivalent to fullness.
In its guise as fullness, the axiom states that, given any sets and , there is a set of enough entire relations from to in this sense:
We have written this in a material fashion; structurally, the axiom says that parametrises enough entire relations in this sense:
There is a subset of such that:
(we think of as giving the evaluation, as a truth value, of , as an entire relation, on the elements and ).
If is an entire relation from to , then for some in :
(we think of as an entire relation via and say that it is contained in ).
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 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 and is a function from to the set of inhabited subsets of . (Power sets on the other hand are sets of all subsets).
In its guise as subset collection, the axiom states …
I need to look this up again, including the conditions for its equivalence with fullness. In the meantime, see the Stanford Encyclopedia’s list of axioms.
In dependent type theory, given a Russell universe , the type of all entire relations between types and is given by the type
In general, this type is not -small. The axiom of fullness for states that the above type is -small, and is given by the following inference rules:
Similarly, for Tarski universes , the type of all entire relations between -small types and is given by the type
There are similar inference rules for strict Tarski universes:
For weak Tarski universes, one uses an equivalence of types instead of judgmental equality
and the two inference rules could be reduced down to the element:
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.
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, can be constructed as the subset of the power set consisting of all entire relations from to . On the other hand, the function set may be constructed as a subset of consisting of those elements such that for (the graph of) some function from to ; (the key here is that must follow when is entire and is a function). Conversely, if we have function sets, then the axiom of choice states precisely that the function set always qualifies as (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 is a projective set with a surjection (which this axiom asserts must exist), then we may take as , with iff, for some in , and .
Note that is not categorical (in the logicians' sense); that is, there may be many sets 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. One reason for adopting it instead of (only) function sets is this: it is strong enough to construct the set of (located Dedekind) real numbers from the set of natural numbers without assuming excluded middle or countable choice; see below.
Subset collection is justified by predicative versions of constructive type theory in the sense of Martin–Löf or Thierry Coquand. To see this, note that these theories justify COSHEP; their types define (not sets in general but) presets (following Bishop) or completely presented sets, which (as sets) are projective. Analogously, an element of may be considered an operation or prefunction (following ‘preset’) from to .
But note that the type of prefunctions from to , like the preset underlying , is a categorical (unique) construction in type theory, while , like COSHEP, is not. Thus type theory (or rather preset theory) gives us constructions that are not available in set theory (even with fullness or even COSHEP), such as the predicate that states whether two functions have equal underlying prefunctions.
We consider this application in some detail; see also real number object.
Using function sets, one can easily construct the set of Cauchy reals as a subquotient of the function set . Both classical and constructive mathematicians usually adopt axioms in which one can prove that ; this is equivalent to a weak countable choice principle (identified by Fred Richman et al) that follows from either excluded middle (classically accepted) or countable choice (usually constructively accepted). But there are (for example) some Grothendieck toposes in which (as a statement in the Mitchell–Bénabou language) fails, so any sort of constructive mathematics that wants to apply to such toposes cannot rely on this method to define the real numbers object .
Of course, in a topos, there are other ways to define , but what if you want your theory to also be predicative? If you adopt the fullness axiom, then you can modify the definition of to produce a definition of without assuming any choice principle. Instead of using , you use instead; can be constructed as a subquotient of that set.
Let an element of be a presequence of natural numbers, and fix a bijection between and the set of rational numbers. We call such a presequence regular if, whenever are natural numbers such that and , we have
(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 in constructive mathematics, and we follow that here.) We call two regular presequences equivalent if, whenever are natural numbers such that and , we have
Then this defines an equivalence relation on the set of regular presequences, and the quotient set is . (That is, it may be given, in the usual way, the structure of a linearly ordered Heyting field which is Dedekind-complete relative to located pairs of upper and lower sets.)
Last revised on October 15, 2023 at 21:32:06. See the history of this page for a list of all contributions to it.