dedekind::sets::IsDecidableSet Concept Reference

A Boolean-valued L-set: an IsLSet whose membership is decidable (χ factors through the dominance Σ ↪ Ω; logic_species is Boole). More...

Concept definition

template<typename S>
concept dedekind::sets::IsDecidableSet =  IsLSet<S> && HasDecidableMembership<S>

Detailed Description

A Boolean-valued L-set: an IsLSet whose membership is decidable (χ factors through the dominance Σ ↪ Ω; logic_species is Boole).

IsLSet (category/topoi.cppm) is the general noun: a subobject with χ into any bounded chain, so a bare L-set may answer Unknown (a Kleene-valued "Ω-set"; an object of the presheaf topos on the chain). IsDecidableSet is the earned refinement — a "Σ-set" — where the classifier is the two-valued fragment and every membership query is answered in Boolean logic. It is weaker than IsSet (ETCS), which adds the axiom schema on top of Ω = 𝔹: a bare Halfspace over int is decidable without being an ETCS set. Naming the restriction positively keeps the partial (Kleene) sets first-class and makes "assume the Boolean fragment" an explicit, visible act. See #846 and Figure "Classifier Ω vs dominance Σ" in the paper.

See also

Giuseppe Rosolini (Università di Genova), Continuity and Effectiveness in Topoi (Oxford D.Phil., 1986) — the dominance Σ this concept selects. Design note / dictionary (the theory, grounded): https://github.com/vincentk/dedekind/issues/267#issuecomment-5711242416