basic constructions:
strong axioms
further
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
A (global) choice operator is structure included in some foundations of mathematics which provides a uniform way to choose an element of every inhabited set or class.
In Hilbert‘s original formulation, for any property we can form a term such that
In other words, if holds of anything at all, then it holds of the particular term . A similar operator was used by Bourbaki and appears in FMathL?.
In category theory, there are two different notions of logic, the usual external logic, and the internal logic of a category. These different notions of logic leads to different notions of a choice operator in category theory, an external choice operator and an internal choice operator
Let be a well-pointed Heyting category. This allows for the objects of to behave as sets and morphisms from the terminal generator to any object to behave as elements of . Then Hilbert’s formulation of the external (global) choice operator is rendered as the following: for any object and any property on the hom-set we can form a morphism such that
This is sometimes used in categorical set theories like ETCS plus epsilon.
Let be a regular category. This implies that given an object , there is a support object , defined as the image of the unique morphism into the terminal object .
An internal (global) choice operator consists of, for every object , a morphism from the support object of to the original object .
Hilbert’s original formulation of the choice operator translates over to the internal language of into the statement that for every object and subobject , there is a morphism from the support object of to itself. This implies the formulation above since the object is always a subobject of itself; conversely, if there is a morphism for every object , then there is a morphism for subobjects .
Given a regular category , the bicategory of relations of is a unitary tabular allegory. Conversely, the category of maps of a unitary tabular allegory is a regular category. Similarly, given a Heyting category , the bicategory of relations of is a division allegory, and conversely, the category of maps of a division allegory is a Heyting category. This implies that internal global choice operators can be defined in any unitary tabular allegory and external global choice operators can be defined in any (well-pointed) division allegory.
This is sometimes used in allegorical set theories like SEAR plus epsilon.
Recall that a map in an allegory is a morphism with a right adjoint, and an injective map between objects and is a map such that . For any objects and , let
denote the hom-subset of maps between objects and . A division allegory is well-pointed if
The allegorical unit is not a zero object
for any objects and and injective maps , if for all maps from the allegorical unit to , there exists a map such that , then is a unitary isomorphism.
Then Hilbert’s formulation of the external (global) choice operator is rendered as the following: for any object and any property on we can form a map such that
The support object of an object in a unitary tabular allegory is the tabulation? of the unique map from into the allegorical unit? .
An internal (global) choice operator in consists of, for every object , an map from the support object of to the original object .
In dependent type theory with propositional truncations, the naive translation of the global choice operator results in the following rule:
The above rule could be simplified to the following rule using function types:
This corresponds to the internal global choice operator in category theory, since the logic is only internal logic in dependent type theory; there is no separate external logic.
One can also use a Hilbert-style global choice operator which says that choice operators exist for dependent sum types
where the existential quantifier is defined as
The Hilbert-style global choice operator implies the other version of the global choice operator, because given a type , the dependent sum type is definitionally isomorphic to . Conversely, the other version of the global choice operator implies the Hilbert style choice operator, since having a global choice operator for every type implies having choice operators for dependent sum types.
This rule is an axiom of set truncation, because given type and elements and , one has a function . Since is an equivalence relation, the fact that there is a function from to implies that is a set.
One could try to set-truncate the target, or restrict the global choice operator to inhabited h-sets:
However, this inference rule implies the untruncated axiom of choice:
which is inconsistent with a univalent Tarski universe with non-propositional h-sets. (See the HoTT book, section 3.8).
The existence of a choice operator implies excluded middle and the double negation law, and in particular, means that in dependent type theory the propositional truncation of a type is given by the double negation modality:
This means that the rules for choice operators can be rewritten using double negation rather than propositional truncations:
equivalently, that
It then becomes clear that the law of double negation is simply the choice operator only for h-propositions. Thus, choice operators could be called the type-theoretic law of double negation under the propositions as types interpretation of dependent type theory.
One could equivalently define the set-theoretic choice operator using double negations, by one of these inference rules:
By currying the conclusion of the second rule, one gets
which is a version of the law of double negation for h-sets.
In dependent type theory, the usual axiom of choice says that the dependent product of a family of inhabited sets is itself inhabited:
If one untruncates the codomain of the function, one gets choice operators for every set-indexed family of sets:
If one removes the requirement that the type family is a family of sets from the axiom of choice, one gets the axiom of infinity-choice:
If one untruncates the codomain of the function, one gets choice operators for every set-indexed family of type:
Similarly, the axiom of countable choice says that the dependent product of a family of inhabited sets indexed by the natural numbers is itself inhabited:
If one untruncates the codomain of the function, one gets choice operators for every -indexed family of sets:
If one removes the requirement that the type family is a family of sets from the axiom of choice, one gets the axiom of infinity-choice:
If one untruncates the codomain of the function, one gets choice operators for every -indexed family of types:
The codomain-untruncated versions of these variants of the axiom of choice are all equivalent to the original inference rule of having global choice operators, which is the special case of either
for the codomain-untruncated axiom of choice the type family being indexed by a contractible type
for the codomain-untruncated axiom of countable choice, the type family being defined by being a contractible type for all natural numbers, so that .
Every detachable subset of the natural numbers has a choice operator. This is because, every detachable subset of the natural numbers is in bijection with the set for a decidable predicate on the natural numbers . Given a decidable predicate on the natural numbers , if there exists a natural number such that holds, then one can construct a minimal natural number such that the holds. See Rijke 2022 for a proof of this in dependent type theory, where is represented by the dependent sum type and the existential quantifier is represented by the propositional truncation of the dependent sum type.
Every pointed set has a choice operator, since its support is a singleton and thus in bijection with the canonical singleton in set theory, and elements in are thus in bijection with functions from its support to itself:
Thus the choice operator can simply be defined as the evaluation of the bijection at the given point of the set,
This makes sense, since if the pointed set is already a subset of another set , then we know that there is already an element for which the predicate on representing the subset holds - the given point of the pointed set; i.e. always holds.
Constructively, the empty set is always not pointed because the function set is a singleton. However, that every set is either pointed or empty is equivalent to the excluded-middle presentation of the axiom of global choice, which says that one can construct an element of the disjoint union .
It should be noted that Hilbert and Bourbaki take the -operator, called in “Theory of Sets” to be a primitive symbol in a mathematical theory. This has the advantage of also allowing the existential and universal quantifiers to be constructed explicitly, since translates to . The intuitive meaning behind the operator is that it returns a distinguished object for which the proposition is true, or if no such object exists, it returns any object for which it is not true. Of course, the intuitive meaning can be misleading since the properties of the epsilon operator are governed by the axiom schema of existence and -extensionality, without which, the symbol has no meaning. The axiom scheme of existence is a statement of Hilbert’s axiom that avoids mention of the existential quantifier.
A wonderful usage of the global choice operator in Bourbaki is that we can easily show that paradoxical sets do not exist, since the definition of a set is given in terms of whether or not the relation defining the set is collectivizing. The example of Russell's paradox is computed in (Theory of Sets, Chapter II, §1, no.4). A consequence of this formulation is that the epsilon calculus is quantifier-free, since subsumes their roles from the predicate calculus. If we adjoin to intuitionistic logic with the axiom scheme of existence, we obtain a non-conservative extension of intuitionistic logic in which the law of excluded middle still does not hold. However, the assumption of the axiom scheme of -extensionality implies the axiom of global choice and therefore the law of excluded middle.
One use of the choice operator is to eliminate undesirable details of implementation. For example, if is “ is a Dedekind-complete totally ordered field,” then we can define “the real numbers” to be . Any of the numerous constructions of the real numbers can then be used to show that there exists an such that , after which point we can discard whichever explicit construction and work only with . This way we can no longer assert that real numbers (elements of ) are Dedekind cuts, or equivalence classes of Cauchy sequences, or anything in particular, since the axioms provide no rules about how must be chosen other than that it must satisfy . So might consist of Cauchy sequences, or Dedekind cuts, or any other way to construct the reals, but we have no way of knowing, and thus we cannot make use of any such definition in a proof about ; we are forced to use only its formal properties. (For a type-theoretic treatment of this situation, see generalized the).
In many cases, the assumption of a global choice operator implies the axiom of choice, since for any family of inhabited sets, a choice function is given by . In fact, in the form given above it often implies the stronger global axiom of choice, which applies to proper classes as well as sets.
“Here, moreover, we come upon a very remarkable circumstance, namely, that all of these transfinite axioms are derivable from a single axiom, one that also contains the core of one of the most attacked axioms in the literature of mathematics, namely, the axiom of choice: , where is the transfinite logical choice function.”
—Hilbert (1925), “On the Infinite”, excerpted in Jean van Heijenoort, From Frege to Gödel, p. 382.
However, in some foundations it seems to be possible to avoid this conclusion (if it is unwanted) by not requiring the choice operator to be extensional, i.e. it may not be the case that implies .
Like the axiom of choice, the existence of a global choice operator is consistent with the other axioms of most foundations. For example, in ZF, the constructible universe (which models , the axiom of constructibility) admits a natural classical well-ordering of the entire universe, giving rise to a naturally defined global choice operator (namely, = the smallest such that in the global well-ordering).
On the other hand, in dependent type theory a global choice operator over the entire type theory is inconsistent with a univalent universe. For univalence requires that all operations on the type universe must be natural with respect to equivalences, which no global choice operator can be. If one only has a global choice operator over only the types in a given type universe, one can still prove the limited principle of omniscience for natural numbers for the entire type theory: a global choice operator for a universe implies that the axiom of choice and excluded middle holds in , which in turn implies that the boolean domain is the homotopy-initial -frame, which is equivalent to .
Hilbert’s -Operator, PlanetMath.
Stanford Encyclopedia of Philosophy article on The Epsilon Calculus.
See also Hilbert (1927), “The Foundations of Mathematics”, pp. 464–479 in JvH.
For the principle of global choice in dependent type theory, see example 14.4.1, remark 14.4.2. and corollary 17.5.3 of
Last revised on August 31, 2024 at 17:19:11. See the history of this page for a list of all contributions to it.