Aristotelian diagrams

Per [DKVD24] (Definition 1). An Aristotelian diagram is a fragment of a Boolean algebra: a finite indexed family φ : ι → α. The Aristotelian relations between its members are derived from φ and the algebra (Diagram.opposition / Diagram.implication, or the IsContradictory … predicates of Basic.lean), never stored — the diagram is the pair (φ, α).

The background logic enters as the choice of α (its Lindenbaum–Tarski algebra), so logic-sensitivity ([DF23]) is the failure of relation- preservation under a non-iso Boolean homomorphism — the dual of the opposition_apply_orderIso invariance under isomorphisms.

TODO

Hexagon (ι = Fin 6) and cube (ι = Fin 8) specializations; the opposition/ implication informativity preorders and the morphism category ([DKVD24]).

structure Aristotelian.Diagram (ι : Type u_3) [Fintype ι] (α : Type u_4) [BooleanAlgebra α] : Type (max u_3 u_4)

An Aristotelian diagram ([DKVD24], Definition 1): a finite fragment φ : ι → α of a Boolean algebra. The relations are derived (Diagram.opposition / Diagram.implication); the indexing ι → α stands in for the paper's F ⊆ α.

• φ : ι → α

  The corner-to-formula assignment (the fragment).

def Aristotelian.Diagram.opposition {ι : Type u_1} [Fintype ι] {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] (D : Diagram ι α) (i j : ι) : OppositionRel

The opposition relation between corners i and j (derived from φ).

Equations

• D.opposition i j = Aristotelian.opposition (D.φ i) (D.φ j)

def Aristotelian.Diagram.implication {ι : Type u_1} [Fintype ι] {α : Type u_2} [BooleanAlgebra α] [DecidableLE α] (D : Diagram ι α) (i j : ι) : ImplicationRel

The implication relation between corners i and j (derived from φ).

Equations

• D.implication i j = Aristotelian.implication (D.φ i) (D.φ j)