nLab classical set

Context

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

Relations

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Constructivism, Realizability, Computability

Contents

Idea

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.

Definition

A classical set is

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

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 f:ABf:A \to B between two classical sets AA and BB at an element bb of BB is a classical set.

  • the product of two classical sets is itself a classical set

  • any subsingleton is a classical set, and in particular

  • 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 AA with a equivalence relation \sim, one can construct the quotient set A/A / \sim. If one can construct a section of the unique surjection which takes elements of AA to its equivalence class in A/A / \sim, then A/A / \sim is a classical set.

Further axioms can be assumed of the category of classical sets which are not neutrally constructive:

Cartesian closure

One can also postulate that the category of classical sets is cartesian closed or equivalently locally cartesian closed.

Theorem

There are two definable functions from every subsingleton AA to the boolean domain {0,1}\{0, 1\}, the constant functions λx:A.0\lambda x:A.0 and λx:A.1\lambda x:A.1. Suppose that either there exists x:Ax:A such that (λx:A.0)(x)(λx:A.1)(x)(\lambda x:A.0)(x) \neq (\lambda x:A.1)(x), or for all x:Ax:A, (λx:A.0)(x)=(λx:A.1)(x)(\lambda x:A.0)(x) = (\lambda x:A.1)(x). Then AA is a decidable subsingleton.

Proof

We prove by case analysis.

Suppose that there exists x:Ax:A such that (λx:A.0)(x)(λx:A.1)(x)(\lambda x:A.0)(x) \neq (\lambda x:A.1)(x). Then AA is a inhabited subsingleton and thus a decidable subsingleton.

Then suppose that for all x:Ax:A, (λx:A.0)(x)=(λx:A.1)(x)(\lambda x:A.0)(x) = (\lambda x:A.1)(x). Then AA is empty and thus a decidable subsingleton, and the function set {0,1} A\{0, 1\}^A is a singleton by the universal property of the empty set, with all functions equal to each other.

This exhausts all options for decidable subsingletons, and exhausts all possible conditions in the hypothesis.

Theorem

Suppose that classical sets are cartesian closed; i.e. suppose that for sets AA and BB with decidable tight apartness relations, the tight apartness relation on the function set B AB^A, defined by f#gx:A.f(x)g(x)f \# g \coloneqq \exists x:A.f(x) \neq g(x), is decidable. Then excluded middle holds.

Proof

Every subsingleton AA has a decidable tight apartness relation where x#yx \# y is always false. The boolean domain {0,1}\{0, 1\} also has a decidable tight apartness relation where x#yx \# y is given by the denial inequality xyx \neq y. That the tight apartness relation on the function set {0,1} A\{0, 1\}^A is decidable implies the previous theorem above, which implies that every subsingleton AA is a decidable subsingleton, which is precisely the condition of excluded middle.

Theorem

Suppose that classical sets are locally cartesian closed; i.e. suppose that for set AA with a decidable tight apartness relation, and family of sets B(x)B(x) indexed by elements xAx \in A where each B(x)B(x) comes with a decidable tight apartness relation, the tight apartness relation on the indexed Cartesian product xAB(x)\prod_{x \in A} B(x), defined by f#gx:A.f(x)g(x)f \# g \coloneqq \exists x:A.f(x) \neq g(x), is decidable. Then excluded middle holds.

Proof

Let AA be a singleton and let B(x)={0,1}B(x) = \{0, 1\} be the constant family of sets that is always defined to be the boolean domain. Then the indexed Cartesian product xAB(x)\prod_{x \in A} B(x) is in bijection with the function set {0,1} A\{0, 1\}^A, and by the previous theorem, excluded middle holds.

In essence, if we take classical mathematics to be mathematics where only the classical sets are relevant, then constructive mathematics are a form of predicative mathematics in the classical sense, where not all classical function sets exist, since general function sets are not classical sets.

Theorem

Suppose that every inequality space is a classical set. Then excluded middle holds.

Theorem

In the presence of quotient sets, suppose that every apartness relation on a set is decidable:

((x.¬R(x,x))(x,y.R(x,y)R(y,x))(x,y,z.R(x,y)R(y,z)R(x,z)))(x,y.R(x,y)¬R(x,y))((\forall x.\neg R(x, x)) \wedge (\forall x, y.R(x, y) \Rightarrow R(y, x)) \wedge (\forall x, y, z.R(x, y) \wedge R(y, z) \Rightarrow R(x, z))) \Rightarrow (\forall x, y.R(x, y) \vee \neg R(x, y))

Then excluded middle holds.

Applications

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 September 3, 2024 at 10:39:22. See the history of this page for a list of all contributions to it.