constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A subobject given by a monomorphism in a coherent category is called complemented (also: decidable) if it has a complement: a subobject such that
their intersection is the initial object
their union is all of
In constructive mathematics, a complemented subobject in Set is called a decidable subset.
Every subobject is complemented in a Boolean category.
In classical mathematics, every subset is decidable. Indeed, the law of excluded middle may be taken to say precisely that every subset of the point is complemented.
More generally, if every subobject of the terminal object of a well-pointed coherent category is complemented, then every subobject in is complemented.
Last revised on July 15, 2019 at 10:45:08. See the history of this page for a list of all contributions to it.