Loading...
Searching...
No Matches
logic.cppm File Reference
module dedekind.category
The Rules of Thought (Ω). More...
#include <algorithm>#include <cmath>#include <compare>#include <concepts>#include <cstdint>#include <functional>#include <limits>#include <type_traits>#include <utility>import dedekind.category:involution;
Include dependency graph for logic.cppm:
Classes | |
| struct | dedekind::category::Boole |
| The internal logic of the Classical Topos ({True, False}). More... | |
| struct | dedekind::category::Kleene |
| The internal logic of the Kleene Topos. More... | |
| struct | dedekind::category::Chain< T > |
Chain<T>: the finite Kleene chain over an integral carrier T, the full-T-range many-valued logic. Boole (2 grades) and Kleene (3) are the small distinguished members; Chain<int> spans the implementation's full int range. More... | |
| struct | dedekind::category::Percentage |
Percentage: a range-enforcing | |
| struct | dedekind::category::Percent |
The bounded confidence chain: a 101-grade De Morgan (Kleene) chain, self-dual about 50. More... | |
| struct | dedekind::category::GetLogic< T > |
The logic a thing lives in, with Boole as the permissive default: a type that names no logic_species and is not a known answer type is read as classical. IsTotalArrow asks this of a plain carrier (an int domain is classical). Do not use it to read the species off a classifier answer: that is classifier_logic_t, which has no default and rejects an answer type that names no species. More... | |
| struct | dedekind::category::GetLogic< Ternary > |
| struct | dedekind::category::GetLogic< T > |
| struct | dedekind::category::ClassifierLogic< bool > |
| struct | dedekind::category::ClassifierLogic< Ternary > |
| struct | dedekind::category::ClassifierLogic< T > |
| struct | dedekind::category::unit_trait< C, Sup > |
A classifier answer's ends are its species' ⊥ and ⊤: the identities of Sup (∨) and Inf (∧), derived once for every answer (𝔹, K₃, Percentage, …), the one spelling of a truth chain's bottom and top. More... | |
| struct | dedekind::category::unit_trait< C, Inf > |
| struct | dedekind::category::species_embed< L, L > |
| struct | dedekind::category::species_embed< Boole, To > |
| struct | dedekind::category::species_embed< Kleene, Percent > |
| struct | dedekind::category::join_logic< L1, L2 > |
| struct | dedekind::category::meet_logic< L1, L2 > |
The meet of two species: the greatest species embedding into both. Total: 𝔹 (the dominance Σ) embeds into every species, so the order is a meet-semilattice with 𝔹 at the bottom. Comparable species meet at the smaller one; an incomparable shipped pair meets at 𝔹 (their only common lower bound). The meet is relative to the registered edges: two even chains (Chain<int>, Chain<long>) meet at 𝔹 here although an embedding between them exists mathematically; register the edge to refine it. A new species that shares a non-𝔹 lower bound with a species it does not compare to must specialise this. More... | |
| struct | dedekind::category::meet_logic< L1, L2 > |
| struct | dedekind::category::Semidecided |
The verdict of a bounded search, read in K₃ along the dominance \(\Sigma \hookrightarrow \Omega\): a witness found is ⊤, none found so far is U, and nothing is ever ⊥, since the absence of a witness within a budget refutes nothing. The one arrow by which "undecided" enters a computation. More... | |
| class | dedekind::category::Truth< L > |
| The Monic Wrapper for a Logical Species (Ω). More... | |
| struct | dedekind::category::SpeciesTraits< Truth< L > > |
| Bridge the Monic Wrapper to the Logic Species Registry. More... | |
| struct | dedekind::category::LogicTraits< T > |
| Primary Template: Default to Classical (Boolean) Logic. More... | |
| struct | dedekind::category::LogicTraits< T > |
| Specialization for Floating-Point Species (IEEE 754 NaN handling). More... | |
| struct | dedekind::category::SubobjectClassifier< T > |
| struct | dedekind::category::logic_complement< L > |
Bridge the species' static-method ops (L::AND / L::OR / L::RFL) to the function-object types the | |
| struct | dedekind::category::NegationArrow< L > |
The arrow reading of logic negation ¬ = L::RFL on the truth object Ω — the canonical order-reversing arrow. More... | |
| struct | dedekind::category::LiftLogic< L > |
The arrow reading of the Rosolini dominance inclusion \(\iota:\mathbb{B}\hookrightarrow\Omega\) (lift_logic): a decided bool answer embeds as the target species' poles (⊥↦False, ⊤↦True). The canonical order-PRESERVING arrow, and the covariant codomain axis of a classifier \(\chi:A\to\Omega\) (#908). More... | |
| struct | dedekind::category::is_involutive< logic_complement< Boole >, bool > |
Witness: Boolean negation is an involution. Boole's RFL is std::logical_not on bool (!!b = b). More... | |
| struct | dedekind::category::is_involutive< logic_complement< Kleene >, Ternary > |
Witness: Kleene negation is an involution. Kleene's RFL reflects the K₃ chain about Unknown, so ¬¬a = a on all three values (the static_asserts above prove it). More... | |
| struct | dedekind::category::is_involutive< logic_complement< Chain< T > >, T > |
Witness: the Chain<T> reflection ~a is an involution (~~x = x) for every integral carrier. More... | |
| struct | dedekind::category::is_involutive< logic_complement< Percent >, Percentage > |
Witness: the Percent reflection 100-p is an involution. More... | |
| struct | dedekind::category::is_involutive< NegationArrow< L >, typename L::Ω > |
The arrow form of the reflection carries the same certificate: NegationArrow<L> is an involution on L::Ω exactly when the species' complement is, so the laws engine ( | |
Namespaces | |
| namespace | dedekind::category |
Concepts | |
| concept | dedekind::category::IsOckhamAlgebra |
| The IsOckhamAlgebra Concept (The Algebraic Signature of Truth). | |
| concept | dedekind::category::HasLogicalOperators |
Pure syntactic shape: T supports the logical operators &&, ||, ! with closed results. | |
| concept | dedekind::category::IsΩ |
| A truth-object: a type that can serve as the classifier Ω for a logical species. | |
| concept | dedekind::category::IsPst |
A truth-object that is a bounded chain: an IsΩ classifier whose values are totally ordered. | |
| concept | dedekind::category::LogicalMap |
| A callable Pred that maps T -> Ω for some IsΩ Ω. Captures the notion of a predicate valued in an arbitrary logic species. | |
| concept | dedekind::category::IsClassifierAnswer |
T is a classifier answer: it names its species. | |
| concept | dedekind::category::LiftsTo |
| concept | dedekind::category::HaveLogicJoin |
| concept | dedekind::category::LiftableInto |
T can be lifted into To's answers: it already is one, or it is a classifier answer whose species' registered embedding into To accepts it and lands in To::Ω (a Truth<L> wrapper is not an L::Ω and is refused). | |
| concept | dedekind::category::IsDeMorganAlgebra |
| The committed algebraic tower for the truth objects (#901). | |
| concept | dedekind::category::IsBoundedDeMorganChain |
A De Morgan algebra whose truth carrier Ω is totally ordered; by the chain-normality theorem this is automatically a Kleene lattice. | |
| concept | dedekind::category::IsBooleanLogic |
A bounded De Morgan chain whose reflection is a genuine complement (a∧¬a=⊥, a∨¬a=⊤); on a chain this forces the 2-element case 𝔹. | |
Typedefs | |
| template<typename Pred, typename T> | |
| using | dedekind::category::OmegaOf |
| Extract the Ω-type of a LogicalMap. | |
| template<typename T> | |
| using | dedekind::category::classifier_logic_t |
| template<typename L1, typename L2> | |
| using | dedekind::category::join_logic_t = typename join_logic<L1, L2>::type |
| template<typename L1, typename L2> | |
| using | dedekind::category::meet_logic_t = typename meet_logic<L1, L2>::type |
| template<typename T> | |
| using | dedekind::category::LogicOf = typename LogicTraits<T>::type |
| Shorthand for the Logic Species of a type. | |
| template<typename T> | |
| using | dedekind::category::Omega = typename LogicOf<T>::Ω |
| Shorthand for the Subobject Classifier (Omega) of a species. | |
Enumerations | |
| enum class | dedekind::category::Ternary : std::int8_t { False = -1 , Unknown = 0 , True = 1 } |
| A three-valued propositional logic for handling partial information. More... | |
| enum class | dedekind::category::CardinalityTag { Finite , Countable , Continuum } |
Functions | |
| template<std::same_as< Percentage > P> | |
| constexpr P | dedekind::category::operator&& (P a, P b) noexcept |
The logical register on Percentage, as Ternary has below: && / || / ! are the species' AND / OR / RFL, so a Percentage answer conjoins as an answer (a product's membership a(x.first) && b(x.second) stays a Percentage) and HasLogicalOperators holds. Deduced on both operands, so no int → Percentage conversion sneaks a bare number into the register. | |
| template<std::same_as< Percentage > P> | |
| constexpr P | dedekind::category::operator|| (P a, P b) noexcept |
| template<std::same_as< Percentage > P> | |
| constexpr P | dedekind::category::operator! (P a) noexcept |
| constexpr Ternary | dedekind::category::operator&& (Ternary a, Ternary b) |
| constexpr Ternary | dedekind::category::operator|| (Ternary a, Ternary b) |
| constexpr Ternary | dedekind::category::operator! (Ternary a) |
| constexpr Ternary | dedekind::category::successor (Ternary a) noexcept |
K₃'s step: the cover False → Unknown → True, saturating at the top (and its dual at the bottom), the NNO step of the chain ( | |
| constexpr Ternary | dedekind::category::predecessor (Ternary a) noexcept |
| constexpr std::strong_ordering | dedekind::category::operator<=> (Ternary a, Ternary b) noexcept |
Truth-order <=> on Ternary: the chain False < Unknown < True | |
|
template<typename TargetLogic, typename T> requires LiftableInto<T, TargetLogic> | |
| constexpr auto | dedekind::category::lift_logic (T value) |
Lift an answer along the dominance into TargetLogic::Ω. A value already in TargetLogic::Ω passes through; otherwise its species is read off the answer type (classifier_logic_t) and the registered embedding applies. Constrained, so an unsupported lift is a substitution failure at the call site, not an error inside. | |
| template<typename L> | |
| constexpr bool | dedekind::category::holds (Truth< L > proposition) noexcept |
| Semantic truth projection for assertion contexts. | |
| template<typename L> | |
| constexpr bool | dedekind::category::refutes (Truth< L > proposition) noexcept |
| Semantic falsity projection for assertion contexts. | |
| template<typename L> requires IsOckhamAlgebra<L> && logic_negation_is_involutive_v<L> && std::equality_comparable<typename L::Ω> | |
| constexpr bool | dedekind::category::is_decided (typename L::Ω value) |
Membership in the decided core \(\{\top, \bot\}\) of an answer-lattice \(\Omega\) — the Rosolini dominance \(\Sigma\), which the paper and lift_logic define as exactly the decided subobject \(\{\top,\bot\}
\hookrightarrow \Omega\). | |
Variables | |
| template<typename From, typename To> | |
| constexpr bool | dedekind::category::lifts_to_v |
The dominance order: From ⊑ To iff the embedding species_embed<From, To> is registered. Reflexive and, over the shipped species, transitive (𝔹 ⊑ K₃ ⊑ Percent; 𝔹 ⊑ Chain<T>). | |
| template<> | |
| constexpr bool | dedekind::category::is_reflexive_v< Percentage, std::less_equal<> > = true |
Register the Kleene carrier Ternary in the bool and int are registered. | |
| template<> | |
| constexpr bool | dedekind::category::is_transitive_v< Percentage, std::less_equal<> > = true |
| template<> | |
| constexpr bool | dedekind::category::is_antisymmetric_v< Percentage, std::less_equal<> > = true |
| template<> | |
| constexpr bool | dedekind::category::is_connex_v< Percentage, std::less_equal<> > = true |
| template<> | |
| constexpr bool | dedekind::category::is_reflexive_v< Percentage, std::less_equal< Percentage > > |
| template<> | |
| constexpr bool | dedekind::category::is_transitive_v< Percentage, std::less_equal< Percentage > > |
| template<> | |
| constexpr bool | dedekind::category::is_antisymmetric_v< Percentage, std::less_equal< Percentage > > = true |
| template<> | |
| constexpr bool | dedekind::category::is_connex_v< Percentage, std::less_equal< Percentage > > |
| template<typename L> | |
| constexpr bool | dedekind::category::logic_negation_is_involutive_v |
true iff the logic negation ¬ = L::RFL is a certified involution. Both shipped De Morgan logics (𝔹, K₃) qualify; a future intuitionistic species whose ¬¬ is only a closure would not. Downstream double-negation elimination gates on this so it stays honest per logic. | |
| template<typename L> | |
| constexpr bool | dedekind::category::logic_is_complemented_v = false |
true iff the species' reflection is a genuine complement (a∧¬a=⊥ and a∨¬a=⊤ for all a), i.e. the chain is 2-element. Boole qualifies; Kleene and Chain<T> (|Ω|>2) do not: their interior values have no complement. This is the logic_species= of decidability: the clopen core Σ = 𝔹 ↪ Ω. | |
| template<> | |
| constexpr bool | dedekind::category::logic_is_complemented_v< Boole > = true |
Detailed Description
The Rules of Thought (Ω).
@partition :logic
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
logic__Algebraic_Logic
"Metoda algebraiczna w logice polega na traktowaniu każdego systemu logicznego jako pewnego określonego rodzaju algebry abstrakcyjnej." (The algebraic method in logic consists in treating every logical system as a specific type of abstract algebra.) — Helena Rasiowa
Before we can define a "Body" (Set) or a "Path" (Sequence), we must establish the "Rules of Presence." This partition defines the logic species that act as the truth-value objects (Ω) for all categorical predicates.
By reifying logic into the Truth wrapper, we prevent the "leaky abstractions" of C++ machine types (such as integral promotion of bool) while allowing for pluggable logical universes:
- Boole: The Boolean Topos ({True, False}).
- Kleene: The Kleene Topos ({True, False, Unknown}).
logic__Structural_Invariants
The shipped logic species (Boole, Kleene, Chain<T>) are De Morgan algebras: a bounded distributive lattice with an order-reversing involution, named by their morphisms AND / OR / RFL. (The bare IsOckhamAlgebra signature admits other logics too, e.g. a future non-involutive intuitionistic species; De Morgan is a property of the shipped family, not of the signature.)
ORis the supremum / join (∨).ANDis the infimum / meet (∧).RFLis the reflection / De Morgan involution (¬); a genuine complement only on the two-chain 𝔹. The shipped species are bounded chains (Boole= 2 grades,Kleene= 3,Chain<T>= |T|), hence Kleene lattices; seeIsDeMorganAlgebra/IsBoundedDeMorganChain/IsBooleanLogicbelow (#901). The former rig (+/*) surface onTruthwas retired: a truth value is a lattice element, not a semiring element.
Textbook defaults in this partition:
- Classical two-valued logic uses C++ operator&& / operator||.
- Kleene K3 uses the value-returning lattice operations Inf / Sup over {-1, 0, 1}.
Wikipedia: Subobject classifier, Topos theory, Kleene logic
- See also
- Rasiowa, H. (1974). An Algebraic Approach to Non-Classical Logics.
- Lambek, J.; Scott, P. J. (1988). Introduction to Higher-Order Categorical Logic.
- Note
- "Every kind of science, if it has only reached a certain degree of maturity, automatically becomes a part of mathematics." – David Hilbert, Axiomatic Thought (1918)
- See also
- #274 Probabilistic Set Membership (work in progress): real or semiring scores beside the chains (
ScoreSet).
