dedekind::category::IsPst Concept Reference

A truth-object that is a bounded chain: an IsΩ classifier whose values are totally ordered. More...

Concept definition

template<typename T>
concept dedekind::category::IsPst =  IsΩ<T> && std::totally_ordered<T>

Detailed Description

A truth-object that is a bounded chain: an IsΩ classifier whose values are totally ordered.

\(\mathbf{Pst} := \mathbf{Jlt} \cap \mathbf{Chain}\) (named for Post's many-valued logics): the IsΩ truth-objects whose order is total, so \(\wedge = \min\), \(\vee = \max\) on the chain \(\bot < \cdots < \top\), and \(\neg\) is the order-reversing reflection. bool ( \(\mathbb{B}\), the two-chain) and Ternary (Kleene \(K_3\), the three-chain) both satisfy it; a truth-object valued in a non-chain lattice (a four-element Boolean algebra, Belnap's bilattice) would be IsΩ but not IsPst. This is the classifier layer's carrier constraint: IsPst pins which chains can serve as \(\Omega\) from a type constraint alone (see lift_logic for the dominance \(\Sigma \hookrightarrow \Omega\) these chains support).

Note

This is a shape gate, exactly as IsΩ is: it certifies the surface (a truth-object that is std::totally_ordered), the definitional \(\mathbf{Jlt} \cap \mathbf{Chain}\). It admits any bounded chain, of any cardinality: order alone makes the chain well-behaved, so finiteness is not required. bool and Ternary are the shipped (finite) chains; a purpose-built \([0,1]\) fuzzy/G"odel carrier under \(\min/\max\) would satisfy it too. A truly non-chain logic (a four-element Boolean algebra, Belnap's bilattice) is excluded because it is not std::totally_ordered.

What the concept does not gate is the semantic chain law: that this order is the truth-order, so AND / OR are \(\min/\max\) under it, RFL is the order-reversing reflection, and the bounds are \(\bot/\top\). That law quantifies over values, so it cannot be a concept; it is witnessed at compile time by the chain-law static_asserts below (bool and Ternary) and by the §3.1 listing. The residual gap is only a pathological type carrying an unrelated total order. FIXME(#854): the principled gate (a consolidated faithful-semilattice primitive tying AND / OR to \(\min/\max\) under the order and supplying the bounds/reflection law) supersedes this shape gate; #854's acceptance criteria are extended to cover the IsPst chain case.