Demey and Smessaert 2024

Keynes and Johnson extended the square of opposition to an octagon of categorical statements with subject negation, read in first-order logic with existential import (EFOL). Demey and Smessaert compare it with an octagon of sets from knowledge representation, built from a relation R and a set S, and with a new octagon of deontic formulas in the modal logic KD. All three are Aristotelian isomorphic, but the first two have Boolean closures of 2 ^ 7 elements and the deontic one of 2 ^ 6, so the deontic octagon is not Boolean isomorphic to the others. Every octagon with the same Aristotelian relations, in any Boolean algebra, has six or seven cells, and is Boolean isomorphic to the deontic octagon or to the octagon for subject negation accordingly.

Main definitions

• subjectNegation, deontic, knowledgeRep: the three Keynes–Johnson octagons.

Main results

• card_minterms_subjectNegation, card_minterms_deontic: the octagons induce partitions of seven and of six cells.
• deonticIso, isEmpty_booleanIso_deontic: the deontic octagon is Aristotelian but not Boolean isomorphic to the octagon for subject negation.
• knowledgeRepIso: the octagon for knowledge representation is Boolean isomorphic to it.
• card_minterms_eq_six_or_seven: every octagon Aristotelian isomorphic to these induces six or seven cells.
• nonempty_booleanIso_subjectNegation_iff, nonempty_booleanIso_deontic_iff, nonempty_booleanIso_subjectNegation_or_deontic: the octagons of seven cells form one Boolean subfamily and those of six the other.

Implementation notes

A subject-negation statement depends only on which regions of S and P are inhabited, so a proposition is a set of EFOL patterns, each read on its canonical model; a deontic formula is likewise a set of KD world types. The octagons are indexed by the subject-negation positions, so γ and δ are the identity, and Section 5's generic description is the subject-negation octagon's. The knowledge-representation octagon assumes, as the paper does tacitly, that X realizes every pattern. The paper identifies the Boolean subfamilies with the sizes of the closures; here two octagons of one size are shown to have minterms vanishing at the same polarity assignments, which makes their Aristotelian isomorphism a Boolean one.

References

• [DS24]

Subject negation (Section 2)

def DemeySmessaert2024.IsEFOLPattern (m : Finset (Bool × Bool)) : Prop

A finite set of regions, a region recording whether an individual is S and whether it is P, is an EFOL pattern when S, non-S, P and non-P are each inhabited.

Equations

• DemeySmessaert2024.IsEFOLPattern m = ((∃ r ∈ m, r.1 = true) ∧ (∃ r ∈ m, r.1 = false) ∧ (∃ r ∈ m, r.2 = true) ∧ ∃ r ∈ m, r.2 = false)

@[instance_reducible]

instance DemeySmessaert2024.instDecidablePredFinsetProdBoolIsEFOLPattern : DecidablePred IsEFOLPattern

Equations

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

def DemeySmessaert2024.InS (m : Finset (Bool × Bool)) (r : ↥m) : Prop

In the canonical model of a pattern, whose individuals are its regions, S holds of the regions inside S.

Equations

• DemeySmessaert2024.InS m r = ((↑r).1 = true)

def DemeySmessaert2024.InP (m : Finset (Bool × Bool)) (r : ↥m) : Prop

In the canonical model of a pattern, P holds of the regions inside P.

Equations

• DemeySmessaert2024.InP m r = ((↑r).2 = true)

@[instance_reducible]

instance DemeySmessaert2024.instDecidablePredSubtypeProdBoolMemFinsetInS (m : Finset (Bool × Bool)) : DecidablePred (InS m)

Equations

• DemeySmessaert2024.instDecidablePredSubtypeProdBoolMemFinsetInS m x✝ = DemeySmessaert2024.instDecidablePredSubtypeProdBoolMemFinsetInS._aux_1 m x✝

@[instance_reducible]

instance DemeySmessaert2024.instDecidablePredSubtypeProdBoolMemFinsetInP (m : Finset (Bool × Bool)) : DecidablePred (InP m)

Equations

• DemeySmessaert2024.instDecidablePredSubtypeProdBoolMemFinsetInP m x✝ = DemeySmessaert2024.instDecidablePredSubtypeProdBoolMemFinsetInP._aux_1 m x✝

def DemeySmessaert2024.subjectNegation : Fin 8 → Finset { m : Finset (Bool × Bool) // IsEFOLPattern m }

The Keynes–Johnson octagon for subject negation lists all, some, no and not all S are P, then the same with non-S (Definition 2).

Equations

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

theorem DemeySmessaert2024.card_minterms_subjectNegation : (Finpartition.minterms subjectNegation).parts.card = 7

The octagon for subject negation induces a partition of seven cells, so its Boolean closure has 2 ^ 7 elements.

Deontic logic (Section 4)

@[reducible, inline]

abbrev DemeySmessaert2024.KDType : Type

A KD world type records the value of p at a world and the nonempty set of its values at the world's successors.

Equations

• DemeySmessaert2024.KDType = (Bool × { s : Finset Bool // s.Nonempty })

def DemeySmessaert2024.Succ (t : KDType) : Option Bool → Option Bool → Prop

In the canonical model of a type, the evaluation world none sees one world for each value at its successors, and each of those sees itself.

Equations

• DemeySmessaert2024.Succ t none (some v) = (v ∈ ↑t.2)
• DemeySmessaert2024.Succ t (some v) (some v') = (v = v')
• DemeySmessaert2024.Succ t x✝ none = False

@[instance_reducible]

instance DemeySmessaert2024.instDecidableSucc (t : KDType) (w v : Option Bool) : Decidable (Succ t w v)

Equations

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

def DemeySmessaert2024.access (t : KDType) : SetRel (Option Bool) (Option Bool)

The accessibility relation of the canonical model of a type.

Equations

• DemeySmessaert2024.access t = {wv : Option Bool × Option Bool | DemeySmessaert2024.Succ t wv.1 wv.2}

@[instance_reducible]

instance DemeySmessaert2024.instDecidableMemProdOptionBoolSetRelAccessMk (t : KDType) (w v : Option Bool) : Decidable ((w, v) ∈ access t)

Equations

• DemeySmessaert2024.instDecidableMemProdOptionBoolSetRelAccessMk t w v = DemeySmessaert2024.instDecidableMemProdOptionBoolSetRelAccessMk._aux_1 t w v

def DemeySmessaert2024.Val (t : KDType) : Option Bool → Prop

The valuation of p in the canonical model of a type.

Equations

• DemeySmessaert2024.Val t none = (t.1 = true)
• DemeySmessaert2024.Val t (some v) = (v = true)

@[instance_reducible]

instance DemeySmessaert2024.instDecidablePredOptionBoolVal (t : KDType) : DecidablePred (Val t)

Equations

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

def DemeySmessaert2024.deontic : Fin 8 → Finset KDType

The Keynes–Johnson octagon for deontic logic, with permission ◇ and obligation □, each formula at the position of the subject-negation statement δ sends to it (Definition 8).

Equations

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

theorem DemeySmessaert2024.card_minterms_deontic : (Finpartition.minterms deontic).parts.card = 6

The deontic octagon induces a partition of six cells, so its Boolean closure has 2 ^ 6 elements.

def DemeySmessaert2024.deonticIso : Aristotelian.AristotelianIso subjectNegation deontic

The deontic octagon is Aristotelian isomorphic to the octagon for subject negation, by the map δ.

Equations

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

theorem DemeySmessaert2024.isEmpty_booleanIso_deontic : IsEmpty (Aristotelian.BooleanIso subjectNegation deontic)

The deontic octagon is not Boolean isomorphic to the octagon for subject negation, since their closures have 2 ^ 6 and 2 ^ 7 elements.

Knowledge representation (Section 3)

def DemeySmessaert2024.knowledgeRep {X : Type u_1} {Y : Type u_2} (R : SetRel X Y) (S : Set Y) : Fin 8 → Set X

The Keynes–Johnson octagon for knowledge representation (Definition 5), each set at the position of the subject-negation statement γ sends to it; R.preimage S is R(S) and Rᶜ is R̄.

Equations

• DemeySmessaert2024.knowledgeRep R S = ![(Rᶜ.preimage S)ᶜ, R.preimage S, (R.preimage S)ᶜ, Rᶜ.preimage S, (Rᶜ.preimage Sᶜ)ᶜ, R.preimage Sᶜ, (R.preimage Sᶜ)ᶜ, Rᶜ.preimage Sᶜ]

noncomputable def DemeySmessaert2024.pattern {X : Type u_1} {Y : Type u_2} {R : SetRel X Y} {S : Set Y} (hS : S.Nonempty) (hSc : Sᶜ.Nonempty) (hR : ∀ (x : X), ∃ (y : Y), (x, y) ∈ R) (hRc : ∀ (x : X), ∃ (y : Y), (x, y) ∉ R) (x : X) : { m : Finset (Bool × Bool) // IsEFOLPattern m }

The pattern of x records which regions of S and R[x] are inhabited. The assumptions of the paper, that S is nontrivial and that R and its complement are serial, make it an EFOL pattern.

Equations

• DemeySmessaert2024.pattern hS hSc hR hRc x = ⟨{r : Bool × Bool | ∃ (y : Y), (y ∈ S ↔ r.1 = true) ∧ ((x, y) ∈ R ↔ r.2 = true)}, ⋯⟩

theorem DemeySmessaert2024.mem_pattern {X : Type u_1} {Y : Type u_2} {R : SetRel X Y} {S : Set Y} (hS : S.Nonempty) (hSc : Sᶜ.Nonempty) (hR : ∀ (x : X), ∃ (y : Y), (x, y) ∈ R) (hRc : ∀ (x : X), ∃ (y : Y), (x, y) ∉ R) {x : X} {r : Bool × Bool} : r ∈ ↑(pattern hS hSc hR hRc x) ↔ ∃ (y : Y), (y ∈ S ↔ r.1 = true) ∧ ((x, y) ∈ R ↔ r.2 = true)

noncomputable def DemeySmessaert2024.pullback {X : Type u_1} {Y : Type u_2} {R : SetRel X Y} {S : Set Y} (hS : S.Nonempty) (hSc : Sᶜ.Nonempty) (hR : ∀ (x : X), ∃ (y : Y), (x, y) ∈ R) (hRc : ∀ (x : X), ∃ (y : Y), (x, y) ∉ R) : BoundedLatticeHom (Finset { m : Finset (Bool × Bool) // IsEFOLPattern m }) (Set X)

Pulling a set of patterns back along pattern is a Boolean homomorphism.

Equations

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

theorem DemeySmessaert2024.knowledgeRep_eq {X : Type u_1} {Y : Type u_2} {R : SetRel X Y} {S : Set Y} (hS : S.Nonempty) (hSc : Sᶜ.Nonempty) (hR : ∀ (x : X), ∃ (y : Y), (x, y) ∈ R) (hRc : ∀ (x : X), ∃ (y : Y), (x, y) ∉ R) : knowledgeRep R S = ⇑(pullback hS hSc hR hRc) ∘ subjectNegation

The octagon for knowledge representation is the octagon for subject negation pulled back along pattern, so x lies in a set iff the canonical model of its pattern makes the corresponding statement true.

noncomputable def DemeySmessaert2024.knowledgeRepIso {X : Type u_1} {Y : Type u_2} {R : SetRel X Y} {S : Set Y} (hS : S.Nonempty) (hSc : Sᶜ.Nonempty) (hR : ∀ (x : X), ∃ (y : Y), (x, y) ∈ R) (hRc : ∀ (x : X), ∃ (y : Y), (x, y) ∉ R) (h : Function.Surjective (pattern hS hSc hR hRc)) : Aristotelian.BooleanIso subjectNegation (knowledgeRep R S)

When every pattern is realized, the octagon for knowledge representation is Boolean isomorphic to the octagon for subject negation, by the map γ.

Equations

• DemeySmessaert2024.knowledgeRepIso hS hSc hR hRc h = ⋯ ▸ Aristotelian.BooleanIso.ofInjective (DemeySmessaert2024.pullback hS hSc hR hRc) ⋯

theorem DemeySmessaert2024.card_minterms_knowledgeRep {X : Type u_1} {Y : Type u_2} {R : SetRel X Y} {S : Set Y} (hS : S.Nonempty) (hSc : Sᶜ.Nonempty) (hR : ∀ (x : X), ∃ (y : Y), (x, y) ∈ R) (hRc : ∀ (x : X), ∃ (y : Y), (x, y) ∉ R) (h : Function.Surjective (pattern hS hSc hR hRc)) : (Finpartition.minterms (knowledgeRep R S)).parts.card = 7

When every pattern is realized, the octagon for knowledge representation induces a partition of seven cells.

The family of Keynes–Johnson octagons (Section 5)

def DemeySmessaert2024.Consistent (σ : Fin 8 → Bool) : Prop

A polarity assignment is consistent with the Keynes–Johnson configuration when its meet contains no two contrary or contradictory literals (Definition 9). No two true corners are disjoint, no two false corners are jointly exhaustive, and no true corner lies below a false one.

Equations

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

@[instance_reducible]

instance DemeySmessaert2024.instDecidablePredForallFinOfNatNatBoolConsistent : DecidablePred Consistent

Equations

• DemeySmessaert2024.instDecidablePredForallFinOfNatNatBoolConsistent x✝ = id inferInstance

theorem DemeySmessaert2024.card_filter_consistent : (Finset.filter Consistent Finset.univ).card = 7

Seven polarity assignments are consistent with the Keynes–Johnson configuration.

theorem DemeySmessaert2024.card_minterms_eq_six_or_seven {α : Type u_1} [BooleanAlgebra α] {φ : Fin 8 → α} [DecidableEq α] (e : Aristotelian.AristotelianIso subjectNegation φ) : (Finpartition.minterms φ).parts.card = 6 ∨ (Finpartition.minterms φ).parts.card = 7

Every Keynes–Johnson octagon, in any Boolean algebra, induces a partition of six or of seven cells. Its nonzero minterms are among the seven consistent ones, six of which are meets of two corners and so nonzero; the seventh may or may not vanish.

theorem DemeySmessaert2024.nonempty_booleanIso_subjectNegation_iff {α : Type u_1} [BooleanAlgebra α] {φ : Fin 8 → α} [DecidableEq α] (e : Aristotelian.AristotelianIso subjectNegation φ) : Nonempty (Aristotelian.BooleanIso subjectNegation φ) ↔ (Finpartition.minterms φ).parts.card = 7

A Keynes–Johnson octagon is Boolean isomorphic to the octagon for subject negation iff it induces seven cells, its nonzero minterms then being the seven consistent ones.

theorem DemeySmessaert2024.nonempty_booleanIso_deontic_iff {α : Type u_1} [BooleanAlgebra α] {φ : Fin 8 → α} [DecidableEq α] (e : Aristotelian.AristotelianIso subjectNegation φ) : Nonempty (Aristotelian.BooleanIso deontic φ) ↔ (Finpartition.minterms φ).parts.card = 6

A Keynes–Johnson octagon is Boolean isomorphic to the deontic octagon iff it induces six cells, its nonzero minterms then being the six meets of two corners.

theorem DemeySmessaert2024.nonempty_booleanIso_subjectNegation_or_deontic {α : Type u_1} [BooleanAlgebra α] {φ : Fin 8 → α} (e : Aristotelian.AristotelianIso subjectNegation φ) : Nonempty (Aristotelian.BooleanIso subjectNegation φ) ∨ Nonempty (Aristotelian.BooleanIso deontic φ)

The Keynes–Johnson octagons form exactly two Boolean subfamilies, each octagon being Boolean isomorphic to the octagon for subject negation or to the deontic octagon, which are not Boolean isomorphic to each other (isEmpty_booleanIso_deontic).