The Boolean refinement of IsCharacteristic: a membership test valued in the dominance Σ, i.e. \(\chi_A : A \to \Sigma\) with \(\Sigma = \Omega\)-decided \(= @c bool\). More...

Concept definition

template<typename P>
concept dedekind::category::IsDecidableCharacteristic = 
    IsCharacteristic<P> && std::same_as<Cod<P>, bool>

Detailed Description

The Boolean refinement of IsCharacteristic: a membership test valued in the dominance Σ, i.e. \(\chi_A : A \to \Sigma\) with \(\Sigma = \Omega\)-decided \(= @c bool\).

IsCharacteristic lands in the full classifier Ω, which for the honest species is three-valued (Ternary, admitting Unknown). IsDecidableCharacteristic demands the codomain be Boole::Ω (bool): membership is answered in two-valued logic and never says Unknown. This is the arrow-level twin of sets::HasDecidableMembership: a sound, conservative certificate that \(\chi_A\) factors through the Rosolini dominance \(\iota : \Sigma \hookrightarrow \Omega\), not a decision of it (it recognises a decidable sub-class; deciding the factorisation exactly is undecidable, #847). In strict (Boolean) ETCS every characteristic arrow is already decidable (Σ = Ω); here it is the earned special case. See #846, category/logic.cppm (lift_logic = ι).

See also: Giuseppe Rosolini (Università di Genova), Oxford D.Phil. 1986 (the dominance Σ); design note: https://github.com/vincentk/dedekind/issues/267#issuecomment-5711242416