Square of Opposition

@cite{barwise-cooper-1981} @cite{horn-2001}

The Aristotelian Square of Opposition reified as a first-class algebraic object.

The square arranges four operators at its vertices:

       contraries
  A ──────────────── E
  │ │
  │ subalterns subalterns
  │ │
  I ──────────────── O
     subcontraries

The six relations:

• Contraries (A–E): cannot both be true
• Subcontraries (I–O): cannot both be false
• Contradictories (A–O, E–I): exactly one is true
• Subalterns (A→I, E→O): the universal entails the particular

The square unifies quantifiers, modals, connectives, and attitudes:

• Quantifiers: A = every, E = no, I = some, O = not-every
• Modals: A = □, E = □¬, I = ◇, O = ¬□
• Attitudes: A = Bel(p), E = Bel(¬p), I = ◇p, O = ¬Bel(p)

The three duality operations (outer negation, inner negation, dual) generate the square from any single vertex. This module provides the abstract framework; concrete instantiations live in their respective theory modules.

structure Core.Opposition.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))

def Core.Opposition.instReprSquare.repr {α✝ : Type u_1} [Repr α✝] : Square α✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.Opposition.instReprSquare {α✝ : Type u_1} [Repr α✝] : Repr (Square α✝)

Equations

• Core.Opposition.instReprSquare = { reprPrec := Core.Opposition.instReprSquare.repr }

structure Core.Opposition.SquareOps (α : Type u_1) : Type u_1

The three operations that generate the square from a single vertex.

Given a vertex A, the other three are determined by:

• E = innerNeg A (negate the scope / complement)
• O = outerNeg A (negate the result)
• I = dual A = outerNeg (innerNeg A)

• inner : α → α

  Inner negation: A ↦ E, I ↦ O

• outer : α → α

  Outer negation: A ↦ O, E ↦ I

• dual : α → α

  Dual: A ↦ I, E ↦ O. Should equal outer ∘ inner.

def Core.Opposition.Square.fromOps {α : Type u_1} (a : α) (ops : SquareOps α) : Square α

Build a square from a single vertex and the three duality operations.

Equations

• Core.Opposition.Square.fromOps a ops = { A := a, E := ops.inner a, I := ops.dual a, O := ops.outer a }

structure Core.Opposition.SquareRelations {W : Type u_1} (sq : Square (W → Bool)) : Prop

The six logical relations of the Square of Opposition.

Defined over W → Bool (decidable propositions over a domain W). The relations are pointwise: they hold at every point w : W.

• subalternAI (w : W) : sq.A w = true → sq.I w = true

  A entails I (subalternation).

• subalternEO (w : W) : sq.E w = true → sq.O w = true

  E entails O (subalternation).

• contradAO (w : W) : sq.A w = !sq.O w

  A and O are contradictories: A = ¬O.

• contradEI (w : W) : sq.E w = !sq.I w

  E and I are contradictories: E = ¬I.

• contraryAE (w : W) : sq.A w = true → sq.E w = false

  A and E are contraries: cannot both be true.

• subcontrIO (w : W) : sq.I w = false → sq.O w = true

  I and O are subcontraries: cannot both be false.

def Core.Opposition.Square.fromGQOps {α : Type u_1} (q : Quantification.GQ α) : Square (Quantification.GQ α)

Build a square from any operator and the GQ duality operations.

Equations

• Core.Opposition.Square.fromGQOps q = Core.Opposition.Square.fromOps q { inner := Core.Quantification.innerNeg, outer := Core.Quantification.outerNeg, dual := Core.Quantification.dualQ }

def Core.Opposition.gqSquareOps (α : Type u_1) : SquareOps (Quantification.GQ α)

The standard GQ duality operations.

Equations

• Core.Opposition.gqSquareOps α = { inner := Core.Quantification.innerNeg, outer := Core.Quantification.outerNeg, dual := Core.Quantification.dualQ }

The six relations are not independent. Given the two contradiction diagonals (A = ¬O, E = ¬I), the other four relations follow:

• Contraries: A ∧ E → A ∧ ¬I → (by subalternation) A ∧ ¬A → ⊥
• Subcontraries: ¬I ∧ ¬O → E ∧ ¬O → (by subalternation) E ∧ ¬E → ⊥
• Subalternation: derived from contrariety + contradiction

So the contradiction diagonals are the primitive relations; the rest are consequences. This matches Horn's analysis: contradiction is fundamental.

theorem Core.Opposition.contraries_not_both_true {W : Type u_1} (sq : Square (W → Bool)) (rel : SquareRelations sq) (w : W) (hA : sq.A w = true) : sq.E w = false

Contraries cannot both be true.

theorem Core.Opposition.subcontraries_not_both_false {W : Type u_1} (sq : Square (W → Bool)) (rel : SquareRelations sq) (w : W) (hI : sq.I w = false) : sq.O w = true

Subcontraries cannot both be false.

theorem Core.Opposition.subaltern_from_contradictions {W : Type u_1} (sq : Square (W → Bool)) (_hAO : ∀ (w : W), sq.A w = !sq.O w) (hEI : ∀ (w : W), sq.E w = !sq.I w) (hAE : ∀ (w : W), sq.A w = true → sq.E w = false) (w : W) (hA : sq.A w = true) : sq.I w = true

From the contradiction diagonals, derive that A entails I.

The SquareRelations axioms above are deliberately weaker than the Aristotelian-relation predicates from Aristotelian.lean: each field asserts just one direction (e.g., subalternAI asserts A → I but not its strictness; contraryAE asserts impossibility of joint truth but not impossibility of joint falsity). This is intentional — it lets users provide minimal axioms and have the rest derived via subaltern_from_contradictions etc.

The bridge lemmas below convert those weaker axioms into the full Aristotelian predicates, when the necessary side conditions (proper-subalternation witnesses, etc.) are provided.

theorem Core.Opposition.SquareRelations.toContradictoryAO {W : Type u_1} {sq : Square (W → Bool)} (rel : SquareRelations sq) : Contradictory sq.A sq.O

The contradAO axiom is exactly Contradictory sq.A sq.O.

theorem Core.Opposition.SquareRelations.toContradictoryEI {W : Type u_1} {sq : Square (W → Bool)} (rel : SquareRelations sq) : Contradictory sq.E sq.I

The contradEI axiom is exactly Contradictory sq.E sq.I.

theorem Core.Opposition.SquareRelations.toSubalternAI {W : Type u_1} {sq : Square (W → Bool)} (rel : SquareRelations sq) (w : W) (hwI : sq.I w = true) (hwA : sq.A w = false) : Subaltern sq.A sq.I

A SquareRelations lifts to Subaltern sq.A sq.I when given a witness w showing I does not entail A. The witness is needed because Aristotelian.Subaltern is proper subalternation (strict).

theorem Core.Opposition.SquareRelations.toContraryAE {W : Type u_1} {sq : Square (W → Bool)} (rel : SquareRelations sq) (w : W) (hwA : sq.A w = false) (hwE : sq.E w = false) : Contrary sq.A sq.E

A SquareRelations lifts to Contrary sq.A sq.E when given a witness w where neither A nor E holds (the joint-non-exhaustion condition that distinguishes Aristotelian Contrary from mere "cannot both be true").

theorem Core.Opposition.outerNeg_contradiction {α : Type u_1} (q : Quantification.GQ α) (R S : α → Prop) : q R S ↔ ¬Quantification.outerNeg q R S

From the outer/inner negation structure, the contradiction diagonals hold definitionally: A ↔ ¬(outerNeg A) and innerNeg A ↔ ¬(dual A).

theorem Core.Opposition.innerNeg_dual_contradiction {α : Type u_1} (q : Quantification.GQ α) (R S : α → Prop) : Quantification.innerNeg q R S ↔ ¬Quantification.dualQ q R S

def Core.Opposition.Square.fromBox {W : Type u_1} (box : (W → Bool) → W → Bool) (p : W → Bool) : Square (W → Bool)

Build a square of propositions from a box-like operator.

Given box : (W → Bool) → W → Bool (e.g., □ = "all accessible worlds satisfy"), and a proposition p, produce the four corners:

• A = box p (□p: necessarily p)
• E = box (¬p) (□¬p: necessarily not-p)
• I = ¬(box (¬p)) (◇p: possibly p)
• O = ¬(box p) (¬□p: not necessarily p)

Equations

• Core.Opposition.Square.fromBox box p = { A := box p, E := box fun (w : W) => !p w, I := fun (w : W) => !box (fun (w' : W) => !p w') w, O := fun (w : W) => !box p w }

theorem Core.Opposition.fromBox_contradAO {W : Type u_1} (box : (W → Bool) → W → Bool) (p : W → Bool) (w : W) : (Square.fromBox box p).A w = !(Square.fromBox box p).O w

The box-derived square always satisfies the contradiction diagonals.

theorem Core.Opposition.fromBox_contradEI {W : Type u_1} (box : (W → Bool) → W → Bool) (p : W → Bool) (w : W) : (Square.fromBox box p).E w = !(Square.fromBox box p).I w

Subalternation is the entailment relation that underlies Horn scales.

The I–A edge of the quantifier square (some → every) is precisely the ⟨some, all⟩ Horn scale from Core.Scale. More generally:

• The weak member of a Horn scale sits at I (particular/existential)
• The strong member sits at A (universal)
• Scalar implicature from I negates A: "some" implicates "not all" (= O)

This means the square of opposition IS the algebraic structure underlying scalar implicature: using the weak term (I) implicates the negation of the strong term (¬A = O). The "O-corner gap" — the non-lexicalization of O — is pragmatically explained: O is always recoverable as the implicature of I.

TODO: Open conjectures (previously stubbed in deleted Core/Conjectures.lean):

• O-corner lexicalization gap: across natural languages, A/E/I are lexicalized but O is always periphrastic (¬A): lexicalized A ∧ lexicalized E ∧ lexicalized I ∧ ¬lexicalized O. Requires a cross-linguistic lexicalization registry.
• Pragmatic explanation of the gap (@cite{horn-2001}, §4.5): the scalar implicature of the I-corner recovers the O-corner's content, making lexicalization of O communicatively redundant.

theorem Core.Opposition.subalternation_is_scale_ordering {W : Type u_1} (sq : Square (W → Bool)) (rel : SquareRelations sq) (w : W) : sq.A w = true → sq.I w = true

Subalternation A→I is equivalent to the Horn-scale ordering: the A-corner entails the I-corner, which is the scale ⟨I, A⟩.