Decidable membership as a compile-time observable. More...
#include <concepts>#include <cstddef>#include <type_traits>import dedekind.sets:cardinality;import dedekind.category;
Namespaces | |
| namespace | dedekind::sets |
Concepts | |
| concept | dedekind::sets::HasDecidableMembership |
| S's membership map ranges into two-valued (classical) logic. | |
| concept | dedekind::sets::IsDecidableSet |
A Boolean-valued L-set: an IsLSet whose membership is decidable (χ factors through the dominance Σ ↪ Ω; logic_species is Boole). | |
Detailed Description
Decidable membership as a compile-time observable.
@partition :computability
computability__Decidability_Axis
Post-2026-05-09 consolidation, this partition exports a single concept along the decidability axis:
- HasDecidableMembership<S> — membership x ∈ S is answered in two-valued logic (i.e. no Unknown). Equivalent to logic_species being Boole. Independent of finiteness: a finite extensional object can be declared with Kleene (e.g. Ø<int, Kleene>, Singleton<42, Kleene>), in which case it satisfies
:sets:cardinality::IsExtensional but NOT HasDecidableMembership.
The orthogonal extensionality axis lives upstream in :sets:cardinality (the canonical home for extensionality / cardinality / enumerability vocabulary post-2026-05-09). Use IsExtensional from there for the size-observable check; IsFinite / IsCountable / IsCardinality are the cardinality-tier concepts. The partition header was trimmed in the same pass: the previous tag-based IsCompileTimeEnumerable concept was retired as redundant — the IsExtensional gate captures the same observable.
computability__Reduction_Restores_Decidability
The free operator& / operator| machinery monotonically tightens the decidability classification as compile-time reductions succeed. An intensional Set over a transfinite carrier starts at the bottom (Kleene, opaque predicate); a structural reduction to Ø or Singleton<V> lifts it to the top (Boole, decidable membership).
Wikipedia: Computability theory, Decidability (logic), Concepts (C++20)
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
- Note
- "We can only see a short distance ahead, but we can see plenty there that needs to be done." — Alan Turing, Computing Machinery and Intelligence, Mind LIX, 236 (October 1950), closing line.
