Isomorphisms of Aristotelian diagrams

An Aristotelian diagram is a fragment of a Boolean algebra, here an indexed family φ : ι → α. Demey and Smessaert call a bijection of corners an Aristotelian isomorphism when it preserves and reflects the four Aristotelian relations, and a Boolean isomorphism when it extends to an order isomorphism of the Boolean closures. Every Boolean isomorphism is an Aristotelian one but not conversely, as their Keynes–Johnson octagons show. Aristotelian isomorphisms form a groupoid, the core of De Klerck, Vignero and Demey's category of Aristotelian diagrams. Demey and Smessaert's bitstring semantics sends each element of the closure of a diagram to the set of its minterms below it, and carries the diagram to an Aristotelian isomorphic diagram of bitstrings.

Main definitions

• AristotelianIso, with refl, symm and trans.
• BooleanIso, with refl, symm and trans.

Main results

• BooleanIso.toAristotelianIso: every Boolean isomorphism is an Aristotelian isomorphism.
• BooleanIso.ofInjective: a diagram is Boolean isomorphic to its image along an injective homomorphism.
• BooleanIso.ofMintermEqBot: a corner bijection is a Boolean isomorphism when the minterms of the two diagrams vanish at the same polarity assignments.
• AristotelianIso.toSetOfMinterms: a diagram and its bitstrings are Aristotelian isomorphic.

Implementation notes

The family φ : ι → α stands in for the paper's set F ⊆ α, and a corner bijection is a bijection of index types. AristotelianIso asks for Disjoint, Codisjoint and < to be preserved and reflected. This is equivalent to asking it of the four relations, since each of IsCompl, IsContrary, IsSubcontrary and < is a Boolean combination of the three, and conversely (disjoint_iff_isCompl_or_isContrary, codisjoint_iff_isCompl_or_isSubcontrary).

The bitstring semantics is Boolean-algebra theory and lives in Core/Order. Demey and Smessaert's partition induced by a fragment (2018, Definition 5; 2024, Definition 3) is Finpartition.minterms, with anchor formulas minterm; their Lemma 3 is disjoint_minterm and sup_minterm, Lemma 4 Finpartition.minterms_sumElim, Lemma 6 BooleanSubalgebra.minterm_le_or_le_compl, Lemma 7 BooleanSubalgebra.le_iff_forall_mem_minterms, Lemma 9 BooleanSubalgebra.isAtom_iff_mem_minterms, and Theorem 1 BooleanSubalgebra.toSetOfMinterms with BooleanSubalgebra.card_closure. They number the minterms and write a set of them as a string of bits; toSetOfMinterms keeps the set. Their Theorem 2, proved there from Theorem 1 through the Boolean-to-Aristotelian lemma, is proved here directly.

References

• [DS18a]
• [DS24]
• [DKVD24]

structure Aristotelian.AristotelianIso {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] (φ : ι → α) (φ' : ι' → α') extends ι ≃ ι' : Type (max u_1 u_2)

An Aristotelian isomorphism is a corner bijection preserving and reflecting Disjoint, Codisjoint and <, and hence the four Aristotelian relations (map_isCompl and siblings).

• toFun : ι → ι'
• invFun : ι' → ι
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_disjoint (i j : ι) : Disjoint (φ i) (φ j) ↔ Disjoint (φ' (self.toFun i)) (φ' (self.toFun j))

  Joint inconsistency (⊓ = ⊥) is preserved and reflected.

• map_codisjoint (i j : ι) : Codisjoint (φ i) (φ j) ↔ Codisjoint (φ' (self.toFun i)) (φ' (self.toFun j))

  Joint exhaustiveness (⊔ = ⊤) is preserved and reflected.

• map_lt (i j : ι) : φ i < φ j ↔ φ' (self.toFun i) < φ' (self.toFun j)

  Subalternation (<) is preserved and reflected.

@[instance_reducible]

instance Aristotelian.AristotelianIso.instEquivLike {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} {φ' : ι' → α'} : EquivLike (AristotelianIso φ φ') ι ι'

Equations

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

@[simp]

theorem Aristotelian.AristotelianIso.coe_fn_toEquiv {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} {φ' : ι' → α'} (e : AristotelianIso φ φ') : ⇑e.toEquiv = ⇑e

theorem Aristotelian.AristotelianIso.ext {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} {φ' : ι' → α'} {e e' : AristotelianIso φ φ'} (h : ∀ (i : ι), e i = e' i) : e = e'

theorem Aristotelian.AristotelianIso.ext_iff {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} {φ' : ι' → α'} {e e' : AristotelianIso φ φ'} : e = e' ↔ ∀ (i : ι), e i = e' i

def Aristotelian.AristotelianIso.refl {ι : Type u_1} {α : Type u_4} [BooleanAlgebra α] (φ : ι → α) : AristotelianIso φ φ

The identity Aristotelian isomorphism.

Equations

• Aristotelian.AristotelianIso.refl φ = { toEquiv := Equiv.refl ι, map_disjoint := ⋯, map_codisjoint := ⋯, map_lt := ⋯ }

def Aristotelian.AristotelianIso.symm {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} {φ' : ι' → α'} (e : AristotelianIso φ φ') : AristotelianIso φ' φ

The inverse Aristotelian isomorphism.

Equations

• e.symm = { toEquiv := e.symm, map_disjoint := ⋯, map_codisjoint := ⋯, map_lt := ⋯ }

def Aristotelian.AristotelianIso.trans {ι : Type u_1} {ι' : Type u_2} {ι'' : Type u_3} {α : Type u_4} {α' : Type u_5} {α'' : Type u_6} [BooleanAlgebra α] [BooleanAlgebra α'] [BooleanAlgebra α''] {φ : ι → α} {φ' : ι' → α'} {φ'' : ι'' → α''} (e : AristotelianIso φ φ') (e' : AristotelianIso φ' φ'') : AristotelianIso φ φ''

Composition of Aristotelian isomorphisms.

Equations

• e.trans e' = { toEquiv := e.trans e'.toEquiv, map_disjoint := ⋯, map_codisjoint := ⋯, map_lt := ⋯ }

theorem Aristotelian.AristotelianIso.map_isCompl {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} {φ' : ι' → α'} (e : AristotelianIso φ φ') (i j : ι) : IsCompl (φ i) (φ j) ↔ IsCompl (φ' (e i)) (φ' (e j))

An Aristotelian isomorphism preserves and reflects contradiction.

theorem Aristotelian.AristotelianIso.map_isContrary {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} {φ' : ι' → α'} (e : AristotelianIso φ φ') (i j : ι) : IsContrary (φ i) (φ j) ↔ IsContrary (φ' (e i)) (φ' (e j))

An Aristotelian isomorphism preserves and reflects contrariety.

theorem Aristotelian.AristotelianIso.map_isSubcontrary {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} {φ' : ι' → α'} (e : AristotelianIso φ φ') (i j : ι) : IsSubcontrary (φ i) (φ j) ↔ IsSubcontrary (φ' (e i)) (φ' (e j))

An Aristotelian isomorphism preserves and reflects subcontrariety.

Boolean isomorphism (Definition 7) and the nesting

def Aristotelian.corner {ι : Type u_1} {α : Type u_4} [BooleanAlgebra α] (φ : ι → α) (i : ι) : ↥(BooleanSubalgebra.closure (Set.range φ))

The i-th corner of a diagram, viewed inside its Boolean closure.

Equations

• Aristotelian.corner φ i = ⟨φ i, ⋯⟩

@[simp]

theorem Aristotelian.coe_corner {ι : Type u_1} {α : Type u_4} [BooleanAlgebra α] (φ : ι → α) (i : ι) : ↑(corner φ i) = φ i

structure Aristotelian.BooleanIso {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] (φ : ι → α) (φ' : ι' → α') : Type (max (max (max u_1 u_2) u_4) u_5)

A Boolean isomorphism is a corner bijection that extends to an order isomorphism of the Boolean closures.

• toEquiv : ι ≃ ι'

  The underlying corner bijection.

• closureIso : ↥(BooleanSubalgebra.closure (Set.range φ)) ≃o ↥(BooleanSubalgebra.closure (Set.range φ'))

  The order-isomorphism of Boolean closures extending it.

• extends_corners (i : ι) : self.closureIso (corner φ i) = corner φ' (self.toEquiv i)

  closureIso carries corners to corners.

theorem Aristotelian.BooleanIso.ext_iff {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} {inst✝ : BooleanAlgebra α} {inst✝¹ : BooleanAlgebra α'} {φ : ι → α} {φ' : ι' → α'} {x y : BooleanIso φ φ'} : x = y ↔ x.toEquiv = y.toEquiv ∧ x.closureIso = y.closureIso

theorem Aristotelian.BooleanIso.ext {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} {inst✝ : BooleanAlgebra α} {inst✝¹ : BooleanAlgebra α'} {φ : ι → α} {φ' : ι' → α'} {x y : BooleanIso φ φ'} (toEquiv : x.toEquiv = y.toEquiv) (closureIso : x.closureIso = y.closureIso) : x = y

def Aristotelian.BooleanIso.refl {ι : Type u_1} {α : Type u_4} [BooleanAlgebra α] (φ : ι → α) : BooleanIso φ φ

The identity Boolean isomorphism.

Equations

• Aristotelian.BooleanIso.refl φ = { toEquiv := Equiv.refl ι, closureIso := OrderIso.refl ↥(BooleanSubalgebra.closure (Set.range φ)), extends_corners := ⋯ }

def Aristotelian.BooleanIso.symm {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} {φ' : ι' → α'} (e : BooleanIso φ φ') : BooleanIso φ' φ

The inverse Boolean isomorphism.

Equations

• e.symm = { toEquiv := e.toEquiv.symm, closureIso := e.closureIso.symm, extends_corners := ⋯ }

def Aristotelian.BooleanIso.trans {ι : Type u_1} {ι' : Type u_2} {ι'' : Type u_3} {α : Type u_4} {α' : Type u_5} {α'' : Type u_6} [BooleanAlgebra α] [BooleanAlgebra α'] [BooleanAlgebra α''] {φ : ι → α} {φ' : ι' → α'} {φ'' : ι'' → α''} (e : BooleanIso φ φ') (e' : BooleanIso φ' φ'') : BooleanIso φ φ''

Composition of Boolean isomorphisms.

Equations

• e.trans e' = { toEquiv := e.toEquiv.trans e'.toEquiv, closureIso := e.closureIso.trans e'.closureIso, extends_corners := ⋯ }

noncomputable def Aristotelian.BooleanIso.ofInjective {ι : Type u_1} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} (g : BoundedLatticeHom α α') (hg : Function.Injective ⇑g) : BooleanIso φ (⇑g ∘ φ)

A diagram is Boolean isomorphic to its image along an injective homomorphism.

Equations

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

noncomputable def Aristotelian.BooleanIso.ofMintermEqBot {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} {φ' : ι' → α'} [Fintype ι] [DecidableEq ι] [DecidableEq α] [DecidableEq α'] (e : ι ≃ ι') (h : ∀ (σ : ι → Bool), minterm φ σ = ⊥ ↔ minterm (φ' ∘ ⇑e) σ = ⊥) : BooleanIso φ φ'

A corner bijection is a Boolean isomorphism when the minterms of the two diagrams, matched along it, vanish together.

Equations

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

def Aristotelian.BooleanIso.toAristotelianIso {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} {φ' : ι' → α'} (bi : BooleanIso φ φ') : AristotelianIso φ φ'

Every Boolean isomorphism is an Aristotelian isomorphism.

Equations

• bi.toAristotelianIso = { toEquiv := bi.toEquiv, map_disjoint := ⋯, map_codisjoint := ⋯, map_lt := ⋯ }

@[instance_reducible]

instance Aristotelian.BooleanIso.instCoeOutAristotelianIso {ι : Type u_1} {ι' : Type u_2} {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {φ : ι → α} {φ' : ι' → α'} : CoeOut (BooleanIso φ φ') (AristotelianIso φ φ')

Forget a Boolean isomorphism down to its underlying Aristotelian isomorphism.

Equations

• Aristotelian.BooleanIso.instCoeOutAristotelianIso = { coe := Aristotelian.BooleanIso.toAristotelianIso }

Bitstrings

noncomputable def Aristotelian.AristotelianIso.toSetOfMinterms {ι : Type u_1} {α : Type u_4} [BooleanAlgebra α] (φ : ι → α) [Fintype ι] [DecidableEq ι] [DecidableEq α] : AristotelianIso φ fun (i : ι) => (BooleanSubalgebra.toSetOfMinterms φ) (corner φ i)

The bitstrings of the elements of a diagram form a diagram Aristotelian isomorphic to it ([DS18a] Theorem 2).

Equations

• Aristotelian.AristotelianIso.toSetOfMinterms φ = { toEquiv := Equiv.refl ι, map_disjoint := ⋯, map_codisjoint := ⋯, map_lt := ⋯ }