Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
basic constructions:
strong axioms
further
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
In constructive mathematics, equality and denial inequality of sets do not have all the properties that they do in classical mathematics. Hence, a classical set is a set in which equality and denial inequality do behave as they do in classical mathematics.
“Classical sets” is a placeholder name for a concept which may or may not have another name in the mathematics literature. The idea however is that classical sets in constructive mathematics are those whose equality and denial inequality behave as they do in classical mathematics.
A classical set is
a set with a decidable tight apartness relation
a set with decidable equality whose denial inequality is an apartness relation.
The two conditions are equivalent:
Decidable equality implies stable equality, which implies that if denial inequality is an apartness relation, it is a tight apartness relation, meaning that the tight apartness relation is decidable.
Conversely, every decidable tight apartness relation implies that the tight apartness relation is a stable relation and thus equivalent to denial inequality; hence denial inequality is decidable and an apartness relation and equality is also decidable.
Note that classical sets are not the same as sets with decidable equality, there are possibly sets with decidable equality and with a tight apartness relation which cannot be proved decidable, such as the real numbers with analytic WLPO but no analytic LPO.
The category of classical sets is the category whose objects are classical sets and whose morphisms are functions. Since tight apartness coincides with denial inequality in classical sets, every function between classical sets is a strongly extensional function.
In constructive mathematics, the category of classical sets is a Heyting category. In particular,
finite sets are classical sets
The natural numbers are a classical set
the disjoint union of two classical sets is itself a classical set
the indexed disjoint union of a family of classical sets indexed by a classical set is a classical set
The preimage of a function between two classical sets and at an element of is a classical set.
the product of two classical sets is itself a classical set
any subsingleton is a classical set, and in particular
the support of any set is a classical set
given two subsingletons and , the function set from to is a classical set
the cartesian product of any family of subsingletons is a classical set
more generally, any subset of a classical set is a classical set, and in particular
subfinite sets are classical sets
subcountable sets are classical sets
the disjoint union of any family of subsingletons is a classical set
Given a classical set with a equivalence relation , one can construct the quotient set . If one can construct a section of the unique surjection which takes elements of to its equivalence class in , then is a classical set.
Further axioms can be assumed of the category of classical sets which are not neutrally constructive:
That Cantor space is a classical set is equivalent to the limited principle of omniscience.
That the Dedekind real numbers are a classical set is equivalent to the analytic LPO.
That the category of classical sets is cartesian closed or equivalently locally cartesian closed, which implies the limited principle of omniscience. This is provable in the cohesive mode in cohesive homotopy type theory from crisp excluded middle and punctual cohesion.
That every inequality space is a classical set, which implies analytic LPO. In the presence of quotient sets, this is equivalent in strength to the statement that every apartness relation on a set is decidable:
The category of classical sets being cartesian closed implies that the boolean domain is the initial Boolean algebra with all joins and meets indexed by classical sets. If every set is a classical set, this implies that the boolean domain is a complete Boolean algebra.
If classical sets are cartesian closed, there is a cartesian closed subcategory of the category of classical sets, which is the initial cartesian closed category with pullbacks and closed under finite sets and the natural numbers. This cartesian closed subcategory is a Boolean topos since if classical sets are cartesian closed, the only subsingletons that can be generated by finite sets and natural numbers in a cartesian closed category with pullbacks are the decidable subsingletons. This means that cartesian closure of classical sets is sufficient to replicate the entirety of (neutral, impredicative) classical mathematics in constructive mathematics, so long as one only works inside the Boolean subtopos.
Working with decidable subsets of sets with a decidable tight apartness makes constructive mathematics very much like classical mathematics. This is why constructivism has few consequences for basic combinatorics and algebra (although it does have important consequences for more advanced topics in those fields). In analysis, in contrast, constructivism matters right away, because constructively the set of real numbers may not have decidable tight apartness.
Last revised on August 31, 2024 at 14:55:21. See the history of this page for a list of all contributions to it.