The logic species a classifier answer type belongs to. More...

Detailed Description

template<typename T>
struct dedekind::category::ClassifierLogic< T >

The logic species a classifier answer type belongs to.

logic__Dominance_Inclusion

The Rosolini dominance inclusion \(\iota : \mathbb{B} \hookrightarrow \Omega\), the decided core into a classifier.

The dominance is general in the classifier \(\Omega\). \(\mathbb{B}\) = Boole::Ω = bool is the two-valued decided core \(\{\top,\bot\}\) that sits inside every answer-lattice \(\Omega\) (every IsΩ), and \(\iota\) is its inclusion. So \(\mathbb{B}\) is primus inter pares among the truth-objects: a peer of any other \(\Omega\) at the object layer, but the one target every decidable map factors through (the Rosolini dominance \(\Sigma\)). Ternary (Kleene \(K_3\)), Percentage and Chain<T> are the non-trivial \(\Omega\) we currently ship: peers of \(\mathbb{B}\), not the canonical \(\Omega\); for Ternary \(\iota\) is the concrete map bool ↪ Ternary (Ternary = \(\mathbb{B} + 1\), adjoining Unknown), while the concept IsDominanceInclusion fixes only the shape \(\mathbb{B} \to \Omega\); a future \(\Omega\) is admitted by that shape but supplies its own \(\mathbb{B}\)-inclusion (lift_logic embeds bool ↪ \(\Omega\) generically, sending \(\bot/\top\) to the target species' poles: Ternary::{False, True}, Chain<T>'s numeric_limits {min,max}; a value already in \(\Omega\) passes through unchanged). \(\top \in \mathbb{B}\) and \(\mathbb{B}\) is closed under dependent conjunction, so a \(\mathbb{B}\)-valued map is decidable: a set whose characteristic map factors as \(A \to \mathbb{B} \xrightarrow{\iota} \Omega\) never answers Unknown. HasDecidableMembership is a sound, conservative certificate of that factorisation (see sets/computability.cppm), not a decision of it (Rice): a ternary-tagged map that never returns Unknown factors through \(\mathbb{B}\) yet the observable stays false. ETCS proper is the degenerate case \(\mathbb{B} = \Omega\).

See also: Giuseppe Rosolini, Continuity and Effectiveness in Topoi, D.Phil. thesis, University of Oxford, 1986 — the origin of the dominance \(\Sigma\) (Rosolini is at the Università di Genova). E. Robinson & G. Rosolini, Categories of Partial Maps, Information and Computation 79(2):95–130, 1988.; Design note and Rosolini↔codebase dictionary (the theory this concept instantiates, not an improvisation): https://github.com/vincentk/dedekind/issues/267#issuecomment-5711242416 The factorisation \(A \to \Sigma \to \Omega\) is named sets::IsDecidableSet / HasDecidableMembership; the classifier arrows are IsCharacteristic / IsDecidableCharacteristic and this inclusion is IsDominanceInclusion (all #846).

Defined for exactly the answer types: bool (Boole), Ternary (Kleene), and any type declaring its logic_species (Percentage, Truth<L>). There is no default: an int is not a truth value unless a species says so (Chain<int>'s Ω is int, but the species is named at the universe, not read off the number). Contrast GetLogic, the permissive read for carriers.

The documentation for this struct was generated from the following file:

src/main/modules/dedekind/category/logic.cppm