The square of opposition

The square of opposition, in the form Horn surveys, has four corners A, E, I, O in a Boolean algebra, related by contradiction (A–O, E–I), contrariety (A–E), subcontrariety (I–O) and subalternation (A→I, E→O). Its instances for generalized quantifiers, after Barwise and Cooper, and for modals live with those theories.

A square with these relations divides its algebra into three pairwise contrary parts, E, A, and between them the conjunction I ⊓ O of the two particulars: the vertices of Horn's triangle of opposition. Horn traces this trichotomy to De Morgan and to Jespersen's tripartition into all, some and none, whose middle term is neither the I nor the O corner but their conjunction; modally the vertices are the impossible, the contingent and the necessary. Ordered by the affirmative corners they lie in, the vertices form the scale none < some but not all < all.

Main definitions

• Square, SquareRelations: a square and the relations of the square.
• Triangle, Square.triangle: the vertices of the triangle of opposition and the element of a square at each.
• Triangle.corners: the corners of the square as sets of vertices, and the order of the vertices by the affirmative corners they lie in.

Main results

• SquareRelations.subalternAI, SquareRelations.subalternEO, SquareRelations.subcontrIO: the remaining relations of the square.
• SquareRelations.pairwise_disjoint_triangle, SquareRelations.sup_triangle: the vertices of a square are pairwise disjoint and join to ⊤.
• Triangle.squareRelations_corners, Triangle.triangle_corners: the corners as sets of vertices satisfy the relations, and the vertices are the singletons.
• Triangle.mem_corners_I, Triangle.mem_corners_A: some holds above the bottom vertex and all at the top one.

References

• [BC81]
• [Hor01]

The square

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

A square of opposition has four corners.

• A : α

  A is the universal affirmative corner (every, □p, Bel p).

• E : α

  E is the universal negative corner (no, □¬p, Bel ¬p).

• I : α

  I is the particular affirmative corner (some, ◇p).

• O : α

  O is the particular negative corner (not every, ¬□p, ¬Bel p).

inductive Aristotelian.Triangle : Type

The vertices of the triangle of opposition, in scale order, are the universal negative E, the conjunction IO of the two particulars, and the universal affirmative A.

• E : Triangle
• IO : Triangle
• A : Triangle

@[instance_reducible]

instance Aristotelian.instDecidableEqTriangle : DecidableEq Triangle

Equations

• Aristotelian.instDecidableEqTriangle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Aristotelian.instReprTriangle : Repr Triangle

Equations

• Aristotelian.instReprTriangle = { reprPrec := Aristotelian.instReprTriangle.repr }

def Aristotelian.instReprTriangle.repr : Triangle → ℕ → Std.Format

Equations

• Aristotelian.instReprTriangle.repr Aristotelian.Triangle.E prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aristotelian.Triangle.E")).group prec✝
• Aristotelian.instReprTriangle.repr Aristotelian.Triangle.IO prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aristotelian.Triangle.IO")).group prec✝
• Aristotelian.instReprTriangle.repr Aristotelian.Triangle.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aristotelian.Triangle.A")).group prec✝

@[instance_reducible]

instance Aristotelian.instFintypeTriangle : Fintype Triangle

Equations

• Aristotelian.instFintypeTriangle = { elems := { val := ↑Aristotelian.Triangle.enumList, nodup := Aristotelian.Triangle.enumList_nodup }, complete := Aristotelian.instFintypeTriangle._proof_1 }

def Aristotelian.Square.triangle {α : Type u_1} [BooleanAlgebra α] (sq : Square α) : Triangle → α

The element of a square at a vertex of its triangle.

Equations

• sq.triangle Aristotelian.Triangle.E = sq.E
• sq.triangle Aristotelian.Triangle.IO = sq.I ⊓ sq.O
• sq.triangle Aristotelian.Triangle.A = sq.A

def Aristotelian.Triangle.corners : Square (Finset Triangle)

The corners of the square, each given as the set of vertices at which it holds.

Equations

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

theorem Aristotelian.Triangle.triangle_corners (t : Triangle) : corners.triangle t = {t}

The element of corners at each vertex is that vertex's singleton.

@[instance_reducible]

instance Aristotelian.Triangle.instLE : LE Triangle

A vertex lies below another when the other lies in every affirmative corner that it does.

Equations

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

@[instance_reducible]

instance Aristotelian.Triangle.instDecidableLE : DecidableLE Triangle

Equations

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

@[instance_reducible]

instance Aristotelian.Triangle.instLinearOrder : LinearOrder Triangle

Equations

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

@[instance_reducible]

instance Aristotelian.Triangle.instBoundedOrder : BoundedOrder Triangle

Equations

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

theorem Aristotelian.Triangle.bot_eq_E : ⊥ = E

theorem Aristotelian.Triangle.top_eq_A : ⊤ = A

theorem Aristotelian.Triangle.mem_corners_I {t : Triangle} : t ∈ corners.I ↔ ⊥ < t

Some holds above the bottom vertex.

theorem Aristotelian.Triangle.mem_corners_A {t : Triangle} : t ∈ corners.A ↔ t = ⊤

All holds at the top vertex.

theorem Aristotelian.Triangle.mem_corners_O {t : Triangle} : t ∈ corners.O ↔ t < ⊤

Not all holds below the top vertex.

theorem Aristotelian.Triangle.mem_corners_E {t : Triangle} : t ∈ corners.E ↔ t = ⊥

None holds at the bottom vertex.

Square relations

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

A square over a Boolean algebra satisfies the relations of the square when both diagonals are contradictory and the universals cannot both hold. Subalternation and subcontrariety follow (subalternAI, subalternEO, subcontrIO).

• contradAO : IsCompl sq.A sq.O

  A and O are contradictories.

• contradEI : IsCompl sq.E sq.I

  E and I are contradictories.

• contraryAE : Disjoint sq.A sq.E

  A and E cannot both hold.

theorem Aristotelian.SquareRelations.subalternAI {α : Type u_1} [BooleanAlgebra α] {sq : Square α} (h : SquareRelations sq) : sq.A ≤ sq.I

A entails I.

theorem Aristotelian.SquareRelations.subalternEO {α : Type u_1} [BooleanAlgebra α] {sq : Square α} (h : SquareRelations sq) : sq.E ≤ sq.O

E entails O.

theorem Aristotelian.SquareRelations.subcontrIO {α : Type u_1} [BooleanAlgebra α] {sq : Square α} (h : SquareRelations sq) : Codisjoint sq.I sq.O

I and O cannot both fail.

theorem Aristotelian.SquareRelations.of_disjoint {α : Type u_1} [BooleanAlgebra α] {sq : Square α} (hI : sq.I = sq.Eᶜ) (hO : sq.O = sq.Aᶜ) (h : Disjoint sq.A sq.E) : SquareRelations sq

When the particulars are the complements of the opposite universals (I = Eᶜ, O = Aᶜ), the diagonals are contradictory outright, so Disjoint A E gives the whole square. Under the Boolean reading contrariety is where existential import lives. It fails when the universals hold vacuously (an empty subject term, or modally a dead-end world), and the assumption ruling that out, a non-empty term or seriality, enters through this hypothesis.

The cells

theorem Aristotelian.SquareRelations.inf_IO_eq {α : Type u_1} [BooleanAlgebra α] {sq : Square α} (h : SquareRelations sq) : sq.I ⊓ sq.O = (sq.A ⊔ sq.E)ᶜ

The middle cell is the complement of the join of the contraries.

theorem Aristotelian.SquareRelations.pairwise_disjoint_triangle {α : Type u_1} [BooleanAlgebra α] {sq : Square α} (h : SquareRelations sq) : Pairwise (Function.onFun Disjoint sq.triangle)

The vertices of a square are pairwise disjoint.

theorem Aristotelian.SquareRelations.sup_triangle {α : Type u_1} [BooleanAlgebra α] {sq : Square α} (h : SquareRelations sq) : sq.triangle Triangle.E ⊔ sq.triangle Triangle.IO ⊔ sq.triangle Triangle.A = ⊤

The vertices of a square join to ⊤.

theorem Aristotelian.Triangle.squareRelations_corners : SquareRelations corners

The corners as sets of vertices satisfy the relations of the square.