Comparison categories as an Aristotelian diagram

The eight comparison categories (Core.Order.Relation) are the elements of the Boolean algebra 𝒫 {lt, eq, gt}; their logical oppositions are exactly the four Aristotelian relations [DS18a] (Core.Logic.Aristotelian). This file is where the two finite-Boolean-algebra developments meet: the comparison/point algebra (with holds its relation-algebra homomorphism) and the theory of opposition (over any [BooleanAlgebra α]).

Because Finset Ordering is a BooleanAlgebra, the Aristotelian relations apply to the named categories with no bridge construction — the classic square of opposition for </=/> is a decide-check over the eight-element carrier. Via Tense.past = before etc. (Semantics/Tense/Defs.lean) these specialise to grammatical tense: past and nonpast are contradictories, past and future contraries, ≤ and ≥ subcontraries.

The square of opposition for </=/>

theorem Core.Order.isContradictory_before_notBefore : Aristotelian.IsContradictory before notBefore

< and ≥ are contradictories: before and notBefore are complementary cells of 𝒫 {lt, eq, gt} — exactly one holds of any pair.

theorem Core.Order.isContradictory_after_notAfter : Aristotelian.IsContradictory after notAfter

> and ≤ are contradictories.

theorem Core.Order.isContrary_before_after : Aristotelian.IsContrary before after

< and > are contraries: disjoint (never both) but not jointly exhaustive — both fail at =.

theorem Core.Order.isSubcontrary_notAfter_notBefore : Aristotelian.IsSubcontrary notAfter notBefore

≤ and ≥ are subcontraries: jointly exhaustive (one always holds) but not disjoint — both hold at =.

theorem Core.Order.isSubaltern_before_notAfter : Aristotelian.IsSubaltern before notAfter

< is subaltern to ≤: strict precedence implies weak precedence.

theorem Core.Order.isSubaltern_after_notBefore : Aristotelian.IsSubaltern after notBefore

> is subaltern to ≥.

theorem Core.Order.opposition_before_notBefore : Aristotelian.opposition before notBefore = Aristotelian.OppositionRel.contradictory

The two-axis classifier agrees: < opposes ≥ as a contradictory.

theorem Core.Order.isContradictory_overlapping_distinct : Aristotelian.IsContradictory overlapping distinct

= and ≠ are contradictories: overlapping and distinct partition the carrier.