Square of Opposition

[BC81] [Hor01]. The Aristotelian square reified as an algebraic object: four corners A, E, I, O over a Boolean algebra, related by contradiction (A–O, E–I), contrariety (A–E), subcontrariety (I–O), and subalternation (A→I, E→O). Concrete instantiations (quantifiers, modals, attitudes) live in their respective theory modules.

The Square

structure Aristotelian.Square (α : Type u_1) : Type u_1

The four vertices of a Square of Opposition.

• A : α

  A-corner: universal affirmative (every, □, Bel p).

• E : α

  E-corner: universal negative (no, □¬, Bel ¬p).

• I : α

  I-corner: particular affirmative (some, ◇, ◇p).

• O : α

  O-corner: particular negative (not-every, ¬□, ¬Bel p).

Square relations

structure Aristotelian.SquareRelations {α : Type u_1} [BooleanAlgebra α] (sq : Square α) : Prop

The six relations of the Square over a Boolean algebra. Contradiction diagonals are the full IsContradictory; contrariety/subcontrariety give one direction (Disjoint/Codisjoint); subalternations are non-strict (≤). The bridges below recover IsContrary/IsSubaltern from the missing witness.

• subalternAI : sq.A ≤ sq.I

  A entails I.

• subalternEO : sq.E ≤ sq.O

  E entails O.

• contradAO : IsContradictory sq.A sq.O

  A and O are contradictories.

• contradEI : IsContradictory sq.E sq.I

  E and I are contradictories.

• contraryAE : Disjoint sq.A sq.E

  A and E are contraries.

• subcontrIO : Codisjoint sq.I sq.O

  I and O are subcontraries.

Bridges to the Aristotelian predicates

theorem Aristotelian.SquareRelations.toSubalternAI {α : Type u_1} [BooleanAlgebra α] {sq : Square α} (rel : SquareRelations sq) (hne : sq.A ≠ sq.I) : IsSubaltern sq.A sq.I

Lift to IsSubaltern sq.A sq.I given strictness sq.A ≠ sq.I.

theorem Aristotelian.SquareRelations.toContraryAE {α : Type u_1} [BooleanAlgebra α] {sq : Square α} (rel : SquareRelations sq) (hne : sq.A ⊔ sq.E ≠ ⊤) : IsContrary sq.A sq.E

Lift to IsContrary sq.A sq.E given non-exhaustion sq.A ⊔ sq.E ≠ ⊤.