Verifies that a binary operator satisfies Leśniewski's mereological axioms. More...

Concept definition

template<typename T, typename Op std::less_equal<T>, typename Ω bool>
concept dedekind::category::IsPartRelation =  requires(Op op, T a, T b, T c) {
  { op(a, b) } -> std::same_as<Ω>;  
 
  
  
  
  requires is_reflexive_v<T, Op>;
  requires is_transitive_v<T, Op>;
  requires is_antisymmetric_v<T, Op>;
}

Detailed Description

Verifies that a binary operator satisfies Leśniewski's mereological axioms.

Textbook term: this is the axiomatic core of a partial-order style parthood relation used in formal mereology.

Template Parameters

Op	The parthood operator (defaults to std::less_equal<T>).
T	The type being reasoned about.
Ω	The truth-value codomain (default: classical two-valued logic).

Note

Textbook alignment:

Parthood/partial-order axioms: reflexive, transitive, antisymmetric.
Default comparator std::less_equal<T> corresponds to the usual order-theoretic relation symbol <=.

See also: Structural mereology overview (Stanford Encyclopedia): https://plato.stanford.edu/entries/mereology/; Lambek & Scott (1988), Introduction to Higher-Order Categorical Logic.; McLarty (1992), Elementary Categories, Elementary Toposes.