nLab
decidable subset

In constructive mathematics, a subset AA of a set XX is called decidable if it is classified by a function from XX to the Boolean domain 2={,}\mathbf{2} = \{\bot, \top\} of classical truth values. Of course, in classical mathematics, 2\mathbf{2} is the set of all truth values, so there every subset is decidable. (A decidable subset is alternatively called a detachable subset, at least in Fred Richman‘s school.)

Equivalently, AA is a decidable subset of XX if every element of XX either does or does not belong to AA.

A set XX has decidable equality if the equality relation is decidable as a subset of X×XX \times X. This generalises in topos theory to the notion of decidable object.

Working with decidable subsets of sets with decidable equality 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 the set of real numbers may have very few decidable subsets. (For example, in intuitionistic mathematics, Russian constructivism, and the topos of sheaves over the real line?, albeit for different reasons in each case, every function from \mathbb{R} to 2\mathbf{2} must be at least pointwise-continuous and thus constant, and therefore there are exactly two decidable subsets of \mathbb{R}: the empty subset and \mathbb{R} itself.)

Last revised on February 7, 2020 at 16:14:01. See the history of this page for a list of all contributions to it.