The four Aristotelian relations [DS18a]

Two elements φ, ψ of a Boolean algebra stand in one of four Aristotelian relations ([DS24], Definition 1):

Relation	Condition	mathlib
Contradictory	φ ⊓ ψ = ⊥ and φ ⊔ ψ = ⊤	IsCompl
Contrary	φ ⊓ ψ = ⊥, φ ⊔ ψ ≠ ⊤	Disjoint ∧ ¬ Codisjoint
Subcontrary	φ ⊓ ψ ≠ ⊥, φ ⊔ ψ = ⊤	¬ Disjoint ∧ Codisjoint
Subalternation	φ < ψ	(· < ·)

The collection {CD, C, SC, SA} is the Aristotelian geometry; elements standing in none of the four are unconnected ([SD14]).

The relations are defined over an arbitrary [BooleanAlgebra α] — the abstract "template" of [DS24]. Concrete instances follow by plugging in a Boolean algebra: the powerset Set W, predicate spaces W → Prop / W → Bool, bitvectors Fin n → Bool, or a Lindenbaum–Tarski algebra. The relations are mathlib's IsCompl / Disjoint / Codisjoint / <, so they inherit that API.

Main declarations

• IsContradictory, IsContrary, IsSubcontrary, IsSubaltern, IsUnconnected — the relations as predicates over [BooleanAlgebra α].
• OppositionRel / ImplicationRel, opposition / implication — the two derived relation axes ([DKD25]); each a total classifier with *_eq_* characterizations, jointly recovering IsUnconnected as NCD ∧ NI.
• isContradictory_apply_orderIso and siblings — a Boolean isomorphism (OrderIso) is an Aristotelian isomorphism: it preserves and reflects all four relations ([DKVD24]).
• isContradictory_iff_forall and siblings — the pointwise ∀ w characterization at the W → Bool instance.

Implementation notes

IsContradictory := IsCompl, IsSubaltern := (· < ·), and contrariety / subcontrariety are Disjoint / Codisjoint combinations, so symmetry and the OrderIso transfer come almost entirely from mathlib's order API.

Todo

• A first-class AristotelianMorphism / category of diagrams ([DKVD24]); the OrderIso transfer lemmas are the immediately-useful slice.

inductive Aristotelian.OppositionRel : Type

The opposition relation between two elements of a Boolean algebra ([DKD25]): the four mutually-exclusive, jointly-exhaustive cells of (Disjoint?, Codisjoint?).

• contradictory : OppositionRel

  Disjoint ∧ Codisjoint — complementary (IsCompl).

• contrary : OppositionRel

  Disjoint ∧ ¬ Codisjoint.

• subcontrary : OppositionRel

  ¬ Disjoint ∧ Codisjoint.

• nonContradictory : OppositionRel

  ¬ Disjoint ∧ ¬ Codisjoint — the residual NCD.

@[implicit_reducible]

instance Aristotelian.instDecidableEqOppositionRel : DecidableEq OppositionRel

Equations

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

def Aristotelian.instReprOppositionRel.repr : OppositionRel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Aristotelian.instReprOppositionRel : Repr OppositionRel

Equations

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

@[implicit_reducible]

instance Aristotelian.instInhabitedOppositionRel : Inhabited OppositionRel

Equations

• Aristotelian.instInhabitedOppositionRel = { default := Aristotelian.instInhabitedOppositionRel.default }

inductive Aristotelian.ImplicationRel : Type

The implication relation between two elements ([DKD25]): the four cells of (x ≤ y?, y ≤ x?). left is (proper) subalternation, bi is equality, nonImplication is incomparability.

• bi : ImplicationRel

  x ≤ y ∧ y ≤ x — equal.

• left : ImplicationRel

  x ≤ y ∧ ¬ y ≤ x — subalternation (x strictly entails y).

• right : ImplicationRel

  ¬ x ≤ y ∧ y ≤ x.

• nonImplication : ImplicationRel

  ¬ x ≤ y ∧ ¬ y ≤ x — incomparable.

@[implicit_reducible]

instance Aristotelian.instDecidableEqImplicationRel : DecidableEq ImplicationRel

Equations

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

def Aristotelian.instReprImplicationRel.repr : ImplicationRel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Aristotelian.instReprImplicationRel : Repr ImplicationRel

Equations

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

@[implicit_reducible]

instance Aristotelian.instInhabitedImplicationRel : Inhabited ImplicationRel

Equations

• Aristotelian.instInhabitedImplicationRel = { default := Aristotelian.instInhabitedImplicationRel.default }

The four relations

@[reducible, inline]

abbrev Aristotelian.IsContradictory {α : Type u_2} [BooleanAlgebra α] (φ ψ : α) : Prop

BA-generic contradictoriness: φ and ψ are complementary — mathlib's IsCompl (Disjoint ∧ Codisjoint); in a Boolean algebra, ψ = φᶜ.

Equations

• Aristotelian.IsContradictory φ ψ = IsCompl φ ψ

@[reducible, inline]

abbrev Aristotelian.IsContrary {α : Type u_2} [BooleanAlgebra α] (φ ψ : α) : Prop

BA-generic contrariety: jointly impossible (Disjoint) but not jointly exhaustive (¬ Codisjoint — both can be false).

Equations

• Aristotelian.IsContrary φ ψ = (Disjoint φ ψ ∧ ¬Codisjoint φ ψ)

@[reducible, inline]

abbrev Aristotelian.IsSubcontrary {α : Type u_2} [BooleanAlgebra α] (φ ψ : α) : Prop

BA-generic subcontrariety: not jointly impossible (¬ Disjoint — both can be true) but jointly exhaustive (Codisjoint).

Equations

• Aristotelian.IsSubcontrary φ ψ = (¬Disjoint φ ψ ∧ Codisjoint φ ψ)

@[reducible, inline]

abbrev Aristotelian.IsSubaltern {α : Type u_2} [BooleanAlgebra α] (φ ψ : α) : Prop

BA-generic proper subalternation: φ strictly entails ψ, i.e. φ < ψ.

Equations

• Aristotelian.IsSubaltern φ ψ = (φ < ψ)

@[reducible, inline]

abbrev Aristotelian.IsUnconnected {α : Type u_2} [BooleanAlgebra α] (φ ψ : α) : Prop

BA-generic unconnectedness: φ and ψ stand in none of the four Aristotelian relations. Per [DS24].

Equations

• Aristotelian.IsUnconnected φ ψ = (¬Disjoint φ ψ ∧ ¬Codisjoint φ ψ ∧ ¬φ ≤ ψ ∧ ¬ψ ≤ φ)

Symmetry

IsContradictory is symmetric via IsCompl.symm (h.symm); contrariety and subcontrariety get their own lemmas; IsSubaltern is directional.

theorem Aristotelian.IsContrary.symm {α : Type u_2} [BooleanAlgebra α] {φ ψ : α} (h : IsContrary φ ψ) : IsContrary ψ φ

theorem Aristotelian.IsSubcontrary.symm {α : Type u_2} [BooleanAlgebra α] {φ ψ : α} (h : IsSubcontrary φ ψ) : IsSubcontrary ψ φ

Transfer along a Boolean isomorphism

A Boolean isomorphism — an OrderIso of Boolean algebras — is an Aristotelian isomorphism: it preserves and reflects all four relations ([DKVD24], [DS24]; the abstract content of [DS18a]'s bitstring transfer). Each lemma is a direct consequence of mathlib's OrderIso order-preservation API.

theorem Aristotelian.isContradictory_apply_orderIso {α : Type u_2} [BooleanAlgebra α] {β : Type u_3} [BooleanAlgebra β] (e : α ≃o β) {φ ψ : α} : IsContradictory (e φ) (e ψ) ↔ IsContradictory φ ψ

theorem Aristotelian.isContrary_apply_orderIso {α : Type u_2} [BooleanAlgebra α] {β : Type u_3} [BooleanAlgebra β] (e : α ≃o β) {φ ψ : α} : IsContrary (e φ) (e ψ) ↔ IsContrary φ ψ

theorem Aristotelian.isSubcontrary_apply_orderIso {α : Type u_2} [BooleanAlgebra α] {β : Type u_3} [BooleanAlgebra β] (e : α ≃o β) {φ ψ : α} : IsSubcontrary (e φ) (e ψ) ↔ IsSubcontrary φ ψ

theorem Aristotelian.isSubaltern_apply_orderIso {α : Type u_2} [BooleanAlgebra α] {β : Type u_3} [BooleanAlgebra β] (e : α ≃o β) {φ ψ : α} : IsSubaltern (e φ) (e ψ) ↔ IsSubaltern φ ψ

Two-axis classifiers (opposition × implication)

The relation between two elements factors into a (Disjoint?, Codisjoint?) opposition and a (≤?, ≥?) implication — each a total, mutually-exclusive classifier ([DKD25]), so no contingency hypothesis is needed.

def Aristotelian.opposition {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] (x y : α) : OppositionRel

The opposition relation of x, y, from the meet/join tests.

Equations

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

def Aristotelian.implication {α : Type u_2} [BooleanAlgebra α] [DecidableLE α] (x y : α) : ImplicationRel

The implication relation of x, y, from the order tests.

Equations

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

@[simp]

theorem Aristotelian.opposition_eq_contradictory {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] {x y : α} : opposition x y = OppositionRel.contradictory ↔ IsContradictory x y

@[simp]

theorem Aristotelian.opposition_eq_contrary {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] {x y : α} : opposition x y = OppositionRel.contrary ↔ IsContrary x y

@[simp]

theorem Aristotelian.opposition_eq_subcontrary {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] {x y : α} : opposition x y = OppositionRel.subcontrary ↔ IsSubcontrary x y

@[simp]

theorem Aristotelian.opposition_eq_nonContradictory {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] {x y : α} : opposition x y = OppositionRel.nonContradictory ↔ ¬Disjoint x y ∧ ¬Codisjoint x y

@[simp]

theorem Aristotelian.implication_eq_bi {α : Type u_2} [BooleanAlgebra α] [DecidableLE α] {x y : α} : implication x y = ImplicationRel.bi ↔ x ≤ y ∧ y ≤ x

@[simp]

theorem Aristotelian.implication_eq_left {α : Type u_2} [BooleanAlgebra α] [DecidableLE α] {x y : α} : implication x y = ImplicationRel.left ↔ IsSubaltern x y

@[simp]

theorem Aristotelian.implication_eq_right {α : Type u_2} [BooleanAlgebra α] [DecidableLE α] {x y : α} : implication x y = ImplicationRel.right ↔ IsSubaltern y x

@[simp]

theorem Aristotelian.implication_eq_nonImplication {α : Type u_2} [BooleanAlgebra α] [DecidableLE α] {x y : α} : implication x y = ImplicationRel.nonImplication ↔ ¬x ≤ y ∧ ¬y ≤ x

theorem Aristotelian.isUnconnected_iff_classify {α : Type u_2} [BooleanAlgebra α] [DecidableEq α] [DecidableLE α] {x y : α} : IsUnconnected x y ↔ opposition x y = OppositionRel.nonContradictory ∧ implication x y = ImplicationRel.nonImplication

IsUnconnected is exactly the (NCD, NI) cell of the opposition × implication product ([DKD25]).

theorem Aristotelian.opposition_apply_orderIso {α : Type u_2} [BooleanAlgebra α] {β : Type u_3} [BooleanAlgebra β] [DecidableEq α] [DecidableEq β] (e : α ≃o β) (x y : α) : opposition (e x) (e y) = opposition x y

A Boolean isomorphism preserves the opposition relation.

theorem Aristotelian.implication_apply_orderIso {α : Type u_2} [BooleanAlgebra α] {β : Type u_3} [BooleanAlgebra β] [DecidableLE α] [DecidableLE β] (e : α ≃o β) (x y : α) : implication (e x) (e y) = implication x y

A Boolean isomorphism preserves the implication relation.

Pointwise characterization for W → Bool

A W → Bool predicate is an element of the Boolean algebra W → Bool; the abstract relations unfold to the familiar model-theoretic ∀ w conditions (validity ⊨ φ := ∀ w, φ w = true).

theorem Aristotelian.disjoint_iff_forall {W : Type u_1} {φ ψ : W → Bool} : Disjoint φ ψ ↔ ∀ (w : W), ¬(φ w = true ∧ ψ w = true)

theorem Aristotelian.codisjoint_iff_forall {W : Type u_1} {φ ψ : W → Bool} : Codisjoint φ ψ ↔ ∀ (w : W), φ w = true ∨ ψ w = true

theorem Aristotelian.le_iff_forall {W : Type u_1} {φ ψ : W → Bool} : φ ≤ ψ ↔ ∀ (w : W), φ w = true → ψ w = true

theorem Aristotelian.isContradictory_iff_forall {W : Type u_1} {φ ψ : W → Bool} : IsContradictory φ ψ ↔ (∀ (w : W), ¬(φ w = true ∧ ψ w = true)) ∧ ∀ (w : W), φ w = true ∨ ψ w = true

theorem Aristotelian.isContrary_iff_forall {W : Type u_1} {φ ψ : W → Bool} : IsContrary φ ψ ↔ (∀ (w : W), ¬(φ w = true ∧ ψ w = true)) ∧ ¬∀ (w : W), φ w = true ∨ ψ w = true

theorem Aristotelian.isSubcontrary_iff_forall {W : Type u_1} {φ ψ : W → Bool} : IsSubcontrary φ ψ ↔ (¬∀ (w : W), ¬(φ w = true ∧ ψ w = true)) ∧ ∀ (w : W), φ w = true ∨ ψ w = true

theorem Aristotelian.isSubaltern_iff_forall {W : Type u_1} {φ ψ : W → Bool} : IsSubaltern φ ψ ↔ (∀ (w : W), φ w = true → ψ w = true) ∧ ¬∀ (w : W), ψ w = true → φ w = true