dedekind::topology::IsClopen Concept Reference

A set that is BOTH open and closed — the topological face of decidability. More...

Concept definition

template<typename S>
concept dedekind::topology::IsClopen =  IsOpen<S> && IsClosed<S>

Detailed Description

A set that is BOTH open and closed — the topological face of decidability.

In synthetic topology (Smyth / Rosolini / Escardó, the project's own Rosolini-dominance foundation) open = semidecidable / affirmable and closed = refutable, so clopen = open ∩ closed = decidable. IsClopen is the topological conservative certificate of that in the carrier's order topology; sets::HasDecidableMembership (logic_species == Boole) is the certificate in the decidability (Sierpiński) topology. They are different topologies, so neither is defined from the other: on a dense carrier an open ray on ℚ is decidable yet not order-closed, and a Kleene-tagged set on a discrete carrier is order-clopen yet not recognised decidable (the #847 gap). On a discrete carrier (HasDiscreteCarrier) every subset is order-clopen, so there the decidability reader implies the order reader; the converse still fails for a Kleene-tagged set, whose logic_species discreteness does not change. Stone duality glues the decidability reading to the Boolean-ring one (#903, #894); the clopen sublattice of Ω measures decidability = disconnectedness (Boole totally disconnected → fully decidable; a Kleene chain highly connected → only the poles ⊥ / ⊤ clopen).

See also

dedekind::sets::HasDecidableMembership