S's membership map ranges into two-valued (classical) logic. More...

Concept definition

template<typename S>
concept dedekind::sets::HasDecidableMembership =  requires {
  typename std::remove_cvref_t<S>::logic_species;
} && std::same_as<typename std::remove_cvref_t<S>::logic_species, Boole>

Detailed Description

S's membership map ranges into two-valued (classical) logic.

computability__Species_On_The_Classifier

There is no carrier-axis species resolver: a universe over a regular carrier answers in Boole (its equality is decidable), and a set's species is read off its classifier (category::classifier_logic_t, joined along the dominance in :expressions). Cardinality stays a cardinality (IsCountable) and picks no logic.

The presence of Unknown in the codomain would forbid this — so Ternary- classified Sets fail. This is the library's observable proxy for "membership is decidable": the compiler knows there's no third answer.

Rosolini reading: this is a sound, conservative certificate that "the characteristic map χ: A → Ω factors through the dominance Σ ↪ Ω" (χ = lift_logic ∘ χ_total with χ_total: A → Σ = Boole::Ω), not a decision of it. It checks that the logic species is Boolean, so it recognises a decidable sub-class but may answer conservatively: an ℝ-tagged Halfspace whose χ never actually returns Unknown is still Kleene-classified, and deciding the factorisation exactly is undecidable (Rice). ETCS proper is the Σ = Ω case; a partial set is χ: A → Ω = Kleene::Ω. See category/logic.cppm (lift_logic = the inclusion Σ ↪ Ω), #267, and #847 (the recognised-vs-actual sub-quadrant).

Note: This is the decidability (Sierpiński) topology's "clopen" — the Δ-reader of the decidability grade (Δ decidable / Σ semidecidable / Π co-semidecidable), of which logic_species is the coarse projection (Δ ↦ Boole, else Kleene). It is deliberately not dedekind::topology::IsClopen, which speaks the carrier's order topology: an open ray on ℚ is decidable yet not order-closed. On a discrete carrier (dedekind::topology::HasDiscreteCarrier) every subset is order-clopen, so there decidable implies order-clopen; the converse fails for a Kleene-tagged set.

See also: dedekind::topology::IsClopen; dedekind::topology::IsOpen; dedekind::topology::IsClosed; dedekind::topology::HasDiscreteCarrier