Documentation

Linglib.Logic.Aristotelian.Basic

The Aristotelian relations #

Demey and Smessaert define four relations between elements x, y of a Boolean algebra, the Aristotelian relations:

RelationDefinitionHere
contradictoryx ⊓ y = ⊥ and x ⊔ y = ⊤IsCompl x y
contraryx ⊓ y = ⊥ and x ⊔ y ≠ ⊤IsContrary x y
subcontraryx ⊓ y ≠ ⊥ and x ⊔ y = ⊤IsSubcontrary x y
subalternationx ⊓ y = x and x ⊔ y ≠ xx < y

Contradiction and subalternation are mathlib's IsCompl and <, so only contrariety and subcontrariety are defined here. Taking the algebra to be Set W, the Lindenbaum–Tarski algebra of a logic, or Fin n → Bool gives the relations between propositions, between formulas, and between bitstrings.

Main definitions #

Main results #

Implementation notes #

The definitions follow the Boolean-algebra version of Demey and Smessaert (2024, Definition 1), which does not ask for contingency. At ⊥ and ⊤ a pair can therefore stand in several relations at once: ⊥ is both contrary to and a subaltern of every contingent element, while two contingent elements stand in at most one (De Klerck, Vignero and Demey, Remark 1 and the paragraph after it). Smessaert and Demey's opposition and implication relations are the four cells of (Disjoint x y, Codisjoint x y) and of (x ≤ y, y ≤ x). Every pair falls in exactly one cell of each, so neither gets a type of its own. De Klerck and Demey (2025, Definition 3) give each opposition relation its order form, contrariety being x < yᶜ, and De Klerck, Vignero and Demey (Lemma 1) list how negating a member moves a pair between the two families.

References #

source
def Aristotelian.IsContrary {α : Type u_1} [BooleanAlgebra α] (x y : α) :
Prop

x and y are contrary when they cannot both hold (Disjoint) but can both fail (¬ Codisjoint).

Equations
Instances For
    source
    def Aristotelian.IsSubcontrary {α : Type u_1} [BooleanAlgebra α] (x y : α) :
    Prop

    x and y are subcontrary when they can both hold (¬ Disjoint) but cannot both fail (Codisjoint).

    Equations
    Instances For
      source
      theorem Aristotelian.IsContrary.symm {α : Type u_1} [BooleanAlgebra α] {x y : α} (h : IsContrary x y) :
      IsContrary y x
      source
      theorem Aristotelian.IsSubcontrary.symm {α : Type u_1} [BooleanAlgebra α] {x y : α} (h : IsSubcontrary x y) :
      IsSubcontrary y x
      source
      theorem Aristotelian.disjoint_iff_isCompl_or_isContrary {α : Type u_1} [BooleanAlgebra α] {x y : α} :
      Disjoint x y ↔ IsCompl x y ∨ IsContrary x y

      Two elements that cannot both hold are contradictory or contrary.

      source
      theorem Aristotelian.codisjoint_iff_isCompl_or_isSubcontrary {α : Type u_1} [BooleanAlgebra α] {x y : α} :
      Codisjoint x y ↔ IsCompl x y ∨ IsSubcontrary x y

      Two elements that cannot both fail are contradictory or subcontrary.

      source
      theorem Aristotelian.isContrary_iff_lt_compl {α : Type u_1} [BooleanAlgebra α] {x y : α} :
      IsContrary x y ↔ x < yᶜ

      Contrariety is subalternation into the complement.

      source
      theorem Aristotelian.isSubcontrary_iff_compl_lt {α : Type u_1} [BooleanAlgebra α] {x y : α} :
      IsSubcontrary x y ↔ yᶜ < x

      Subcontrariety is subalternation out of the complement.

      source
      @[simp]
      theorem Aristotelian.isContrary_compl_compl {α : Type u_1} [BooleanAlgebra α] {x y : α} :
      IsContrary xᶜ yᶜ ↔ IsSubcontrary x y
      source
      @[simp]
      theorem Aristotelian.isSubcontrary_compl_compl {α : Type u_1} [BooleanAlgebra α] {x y : α} :
      IsSubcontrary xᶜ yᶜ ↔ IsContrary x y
      source
      @[simp]
      theorem Aristotelian.isContrary_map_orderIso_iff {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] {x y : α} (e : α ≃o β) :
      IsContrary (e x) (e y) ↔ IsContrary x y
      source
      @[simp]
      theorem Aristotelian.isSubcontrary_map_orderIso_iff {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] {x y : α} (e : α ≃o β) :
      IsSubcontrary (e x) (e y) ↔ IsSubcontrary x y