dedekind::category::Kleene Struct Reference

The internal logic of the Kleene Topos. More...

Public Types
using	Ω = Ternary
using	JoinOp = Sup
	The op-types OR / AND / RFL are. Kleene's join / meet are max / min on the K₃ chain, i.e. the value-returning Sup / Inf from :mereology (not the std::ranges::max / min niebloids, which return const T& and fail IsClosedUnder; #912/ #933). ¬ is logic_complement<Kleene>.
using	MeetOp = Inf
using	RflOp = logic_complement<Kleene>

Static Public Member Functions
static constexpr Ternary	AND (Ternary a, Ternary b)
	Kleene Conjunction: Returns the minimum truth value.
static constexpr Ternary	OR (Ternary a, Ternary b)
	Kleene Disjunction: Returns the maximum truth value.
static constexpr Ternary	RFL (Ternary a)
	Kleene reflection: the order-reversing De Morgan involution (fixes U, swaps ⊥/⊤). Implemented as sign-flip on the balanced {-1,0,+1} int8 encoding, so the -x below is the encoding's additive inverse — not a rig inverse: the rig addition is join (max), which is idempotent and has no inverses.

Static Public Attributes
static constexpr Ternary	True = Ternary::True
static constexpr Ternary	False = Ternary::False
static constexpr Ternary	Unknown = Ternary::Unknown

Detailed Description

The internal logic of the Kleene Topos.

Maps logical morphisms to numerical min/max/negation operations over the {-1, 0, 1} lattice. This ensures that 'Unknown' acts as a neutral element in specific contexts while 'False' remains an annihilator for conjunction.

The intention is to allow the type system to say that some predicate is not computable.

Textbook term: Kleene's strong three-valued logic (K3).

Member Typedef Documentation

JoinOp

using dedekind::category::Kleene::JoinOp = Sup

The op-types OR / AND / RFL are. Kleene's join / meet are max / min on the K₃ chain, i.e. the value-returning Sup / Inf from :mereology (not the std::ranges::max / min niebloids, which return const T& and fail IsClosedUnder; #912/ #933). ¬ is logic_complement<Kleene>.

(#923)

---

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

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