Minimal covering semantics

Booth's semantics for modals over disjunctions ([Boo22a], [Boo22b]): a necessity modal requires the alternatives of its prejacent to form a minimal cover of the relevant worlds, not merely a cover, and a possibility modal requires them to minimally cover some nonempty set of relevant worlds. Each alternative must then contribute a relevant world the others miss, which yields the Independence inferences of free choice and blocks the Ross inference.

The unilateral modals box and dia act on inquisitive propositions (Question W), whose alternatives let a modal see the disjuncts of its prejacent. The bilateral semantics assigns each sentence a pair of inquisitive propositions, the states verifying and the states falsifying it, overlapping only in the inconsistent state ∅. These pairs are Kalman's construction over the inquisitive algebra, BilatInqProp W := Kalman (Question W), so negation swaps the pair and conjunction and disjunction are the Kleene-lattice operations, with the De Morgan laws and double negation for free. The bilateral modals are pairs of unilateral ones, necessity = (box, dia) and possibility = (dia, box) applied to the two coordinates, so the duality of □ and ◇ holds by definition. Truth and falsity are the informative contents of the two coordinates, together the Kleene homomorphism BilatInqProp.info into the partial propositions Kalman (Set W): no sentence is both true and false, but a modal sentence can be neither.

Main definitions

• MinimalCovering.IsMinCover, MinimalCovering.IsSuperCover: minimal covers and the super covers of [Sim05].
• MinimalCovering.box, MinimalCovering.dia: the unilateral modals.
• MinimalCovering.BilatInqProp: bilateral inquisitive propositions; BilatInqProp.info, BilatInqProp.truth, BilatInqProp.falsity.
• MinimalCovering.atom, MinimalCovering.bang, MinimalCovering.necessity, MinimalCovering.possibility, MinimalCovering.updateAccess: the clauses of the semantics.
• MinimalCovering.Formula, MinimalCovering.Formula.eval: the language and its interpretation, the restrictor conditional evaluating its consequent under the updated accessibility.

Main results

• MinimalCovering.isMinCover_iff: a cover is minimal exactly when each member is needed.
• MinimalCovering.IsMinCover.isSuperCover: a minimal cover is a super cover.
• MinimalCovering.possibility_eq_compl_necessity_compl: the duality of the modals.
• MinimalCovering.truth_necessity_of_alt_eq_singleton, MinimalCovering.truth_possibility_of_alt_eq_singleton: over a single alternative the modals have their orthodox truth conditions.

References

• [Boo22a]
• [Boo22b]
• [Sim05]
• [CGR18]
• [Kal58]

Covers

def MinimalCovering.IsMinCover {W : Type u_1} (C : Set (Set W)) (S : Set W) : Prop

C is a minimal cover of S: it covers S, S ⊆ ⋃₀ C, and no proper subfamily does.

Equations

• MinimalCovering.IsMinCover C S = Minimal (fun (X : Set (Set W)) => S ⊆ ⋃₀ X) C

theorem MinimalCovering.IsMinCover.subset_sUnion {W : Type u_1} {C : Set (Set W)} {S : Set W} (h : IsMinCover C S) : S ⊆ ⋃₀ C

theorem MinimalCovering.isMinCover_iff {W : Type u_1} {C : Set (Set W)} {S : Set W} : IsMinCover C S ↔ S ⊆ ⋃₀ C ∧ ∀ c ∈ C, ¬S ⊆ ⋃₀ (C \ {c})

A cover is minimal exactly when each member is needed: dropping it leaves part of S uncovered.

theorem MinimalCovering.isMinCover_empty_iff {W : Type u_1} {C : Set (Set W)} : IsMinCover C ∅ ↔ C = ∅

Only the empty family minimally covers ∅.

theorem MinimalCovering.IsMinCover.nonempty {W : Type u_1} {C : Set (Set W)} {S : Set W} (h : IsMinCover C S) (hC : C.Nonempty) : S.Nonempty

A nonempty family minimally covers only nonempty sets.

theorem MinimalCovering.isMinCover_singleton_iff {W : Type u_1} {X S : Set W} (hS : S.Nonempty) : IsMinCover {X} S ↔ S ⊆ X

A single set minimally covers a nonempty S exactly when it contains it.

theorem MinimalCovering.isMinCover_singleton_iff' {W : Type u_1} {X S : Set W} : IsMinCover {X} S ↔ S.Nonempty ∧ S ⊆ X

A single set minimally covers S exactly when S is nonempty and inside it.

theorem MinimalCovering.isMinCover_pair_iff {W : Type u_1} {A B S : Set W} (hAB : A ≠ B) : IsMinCover {A, B} S ↔ S ⊆ A ∪ B ∧ ¬S ⊆ A ∧ ¬S ⊆ B

A pair minimally covers S exactly when it covers S and neither member covers it alone.

theorem MinimalCovering.isMinCover_pair_iff_inter_sdiff {W : Type u_1} {A B S : Set W} (hAB : A ≠ B) : IsMinCover {A, B} S ↔ S ⊆ A ∪ B ∧ (S ∩ (A \ B)).Nonempty ∧ (S ∩ (B \ A)).Nonempty

{A, B} minimally covers S exactly when it covers S and S meets both relative complements: the Independence inferences.

def MinimalCovering.IsSuperCover {W : Type u_1} (C : Set (Set W)) (S : Set W) : Prop

C is a super cover of S ([Sim05]): it covers S and each of its members meets S.

Equations

• MinimalCovering.IsSuperCover C S = (S ⊆ ⋃₀ C ∧ ∀ c ∈ C, (c ∩ S).Nonempty)

theorem MinimalCovering.isSuperCover_pair_iff {W : Type u_1} {A B S : Set W} : IsSuperCover {A, B} S ↔ S ⊆ A ∪ B ∧ (A ∩ S).Nonempty ∧ (B ∩ S).Nonempty

{A, B} super covers S exactly when it covers S and S meets both A and B: the Diversity inferences.

theorem MinimalCovering.IsMinCover.isSuperCover {W : Type u_1} {C : Set (Set W)} {S : Set W} (h : IsMinCover C S) : IsSuperCover C S

A minimal cover is a super cover, since a member missing S could be dropped.

The unilateral modals

def MinimalCovering.box {W : Type u_1} (R : W → Set W) (P : Question W) : Question W

The unilateral necessity modal: □P holds at w when the alternatives of P minimally cover the relevant worlds R w.

Equations

• MinimalCovering.box R P = Question.ofSet {w : W | MinimalCovering.IsMinCover P.alt (R w)}

def MinimalCovering.dia {W : Type u_1} (R : W → Set W) (P : Question W) : Question W

The unilateral possibility modal: ◇P holds at w when the alternatives of P minimally cover a nonempty set of relevant worlds.

Equations

• MinimalCovering.dia R P = Question.ofSet {w : W | ∃ R' ⊆ R w, R'.Nonempty ∧ MinimalCovering.IsMinCover P.alt R'}

@[simp]

theorem MinimalCovering.info_box {W : Type u_1} (R : W → Set W) (P : Question W) : (box R P).info = {w : W | IsMinCover P.alt (R w)}

@[simp]

theorem MinimalCovering.info_dia {W : Type u_1} (R : W → Set W) (P : Question W) : (dia R P).info = {w : W | ∃ R' ⊆ R w, R'.Nonempty ∧ IsMinCover P.alt R'}

theorem MinimalCovering.disjoint_box_dia {W : Type u_1} (R : W → Set W) {P Q : Question W} (h : Disjoint P.info Q.info) : Disjoint (box R P) (dia R Q)

A proposition and its would-be falsifier with disjoint informative contents: the relevant worlds cannot both be minimally covered by the alternatives of the first and have a nonempty part minimally covered by those of the second.

Bilateral inquisitive propositions

@[reducible, inline]

abbrev MinimalCovering.BilatInqProp (W : Type u_2) : Type u_2

A bilateral inquisitive proposition: a pair of inquisitive propositions, the states verifying and the states falsifying a sentence, overlapping only in ∅ (disjoint in Question W, whose bottom is {∅}). This is Kalman's construction over the inquisitive algebra; Kalman.pro and Kalman.con are Booth's ⟦φ⟧⁺ and ⟦φ⟧⁻, and negation, conjunction and disjunction are ᶜ, ⊓ and ⊔.

Equations

• MinimalCovering.BilatInqProp W = Kalman (Question W)

def MinimalCovering.BilatInqProp.info {W : Type u_1} : BoundedLatticeHom (BilatInqProp W) (Kalman (Set W))

The informative contents of the two coordinates, (info ⟦φ⟧⁺, info ⟦φ⟧⁻), as a Kleene homomorphism into the partial propositions.

Equations

• MinimalCovering.BilatInqProp.info = Kalman.map Question.infoHom.toBoundedLatticeHom

@[reducible, inline]

abbrev MinimalCovering.BilatInqProp.truth {W : Type u_1} (φ : BilatInqProp W) : Set W

The worlds at which φ is true, info ⟦φ⟧⁺.

Equations

• φ.truth = (MinimalCovering.BilatInqProp.info φ).pro

@[reducible, inline]

abbrev MinimalCovering.BilatInqProp.falsity {W : Type u_1} (φ : BilatInqProp W) : Set W

The worlds at which φ is false, info ⟦φ⟧⁻.

Equations

• φ.falsity = (MinimalCovering.BilatInqProp.info φ).con

theorem MinimalCovering.BilatInqProp.truth_eq {W : Type u_1} (φ : BilatInqProp W) : φ.truth = (Kalman.pro φ).info

theorem MinimalCovering.BilatInqProp.falsity_eq {W : Type u_1} (φ : BilatInqProp W) : φ.falsity = (Kalman.con φ).info

theorem MinimalCovering.BilatInqProp.mem_truth_iff {W : Type u_1} (φ : BilatInqProp W) {w : W} : w ∈ φ.truth ↔ {w} ∈ Kalman.pro φ

theorem MinimalCovering.BilatInqProp.mem_falsity_iff {W : Type u_1} (φ : BilatInqProp W) {w : W} : w ∈ φ.falsity ↔ {w} ∈ Kalman.con φ

theorem MinimalCovering.BilatInqProp.disjoint_truth_falsity {W : Type u_1} (φ : BilatInqProp W) : Disjoint φ.truth φ.falsity

No sentence is both true and false.

@[simp]

theorem MinimalCovering.BilatInqProp.truth_compl {W : Type u_1} (φ : BilatInqProp W) : φᶜ.truth = φ.falsity

@[simp]

theorem MinimalCovering.BilatInqProp.falsity_compl {W : Type u_1} (φ : BilatInqProp W) : φᶜ.falsity = φ.truth

@[simp]

theorem MinimalCovering.BilatInqProp.truth_sup {W : Type u_1} (φ ψ : BilatInqProp W) : (φ ⊔ ψ).truth = φ.truth ∪ ψ.truth

@[simp]

theorem MinimalCovering.BilatInqProp.falsity_sup {W : Type u_1} (φ ψ : BilatInqProp W) : (φ ⊔ ψ).falsity = φ.falsity ∩ ψ.falsity

@[simp]

theorem MinimalCovering.BilatInqProp.truth_inf {W : Type u_1} (φ ψ : BilatInqProp W) : (φ ⊓ ψ).truth = φ.truth ∩ ψ.truth

@[simp]

theorem MinimalCovering.BilatInqProp.falsity_inf {W : Type u_1} (φ ψ : BilatInqProp W) : (φ ⊓ ψ).falsity = φ.falsity ∪ ψ.falsity

def MinimalCovering.atom {W : Type u_1} (V : Set W) : BilatInqProp W

An atomic sentence true at V: (↓{V}, ↓{Vᶜ}).

Equations

• MinimalCovering.atom V = Kalman.mk (Question.ofSet V) (Question.ofSet Vᶜ) ⋯

@[simp]

theorem MinimalCovering.pro_atom {W : Type u_1} (V : Set W) : Kalman.pro (atom V) = Question.ofSet V

@[simp]

theorem MinimalCovering.con_atom {W : Type u_1} (V : Set W) : Kalman.con (atom V) = Question.ofSet Vᶜ

@[simp]

theorem MinimalCovering.truth_atom {W : Type u_1} (V : Set W) : (atom V).truth = V

@[simp]

theorem MinimalCovering.falsity_atom {W : Type u_1} (V : Set W) : (atom V).falsity = Vᶜ

theorem MinimalCovering.compl_atom {W : Type u_1} (V : Set W) : (atom V)ᶜ = atom Vᶜ

The negation of an atom is the atom of the complement.

theorem MinimalCovering.alt_atom_pro {W : Type u_1} (V : Set W) : (Kalman.pro (atom V)).alt = {V}

theorem MinimalCovering.alt_atom_con {W : Type u_1} (V : Set W) : (Kalman.con (atom V)).alt = {Vᶜ}

theorem MinimalCovering.alt_sup_atom {W : Type u_1} {Vp Vq : Set W} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) Vp Vq) : (Kalman.pro (atom Vp ⊔ atom Vq)).alt = {Vp, Vq}

For incomparable atoms, the positive alternatives of p ∨ q are the two truth sets.

theorem MinimalCovering.alt_sup_atom_con {W : Type u_1} (Vp Vq : Set W) : (Kalman.con (atom Vp ⊔ atom Vq)).alt = {Vpᶜ ∩ Vqᶜ}

The negative alternative of p ∨ q is the set where both are false.

theorem MinimalCovering.alt_inf_compl_atom {W : Type u_1} (Vp Vq : Set W) : (Kalman.pro (atom Vp ⊓ (atom Vq)ᶜ)).alt = {Vp ∩ Vqᶜ}

The positive alternative of p ∧ ¬q is the set of p-without-q worlds.

def MinimalCovering.bang {W : Type u_1} (φ : BilatInqProp W) : BilatInqProp W

The inquisitive !, erasing the distinctions between alternatives on both sides: (↓{info ⟦φ⟧⁺}, ↓{info ⟦φ⟧⁻}), each coordinate its double pseudocomplement.

Equations

• MinimalCovering.bang φ = Kalman.mk (Kalman.pro φ)ᶜᶜ (Kalman.con φ)ᶜᶜ ⋯

@[simp]

theorem MinimalCovering.truth_bang {W : Type u_1} (φ : BilatInqProp W) : (bang φ).truth = φ.truth

@[simp]

theorem MinimalCovering.falsity_bang {W : Type u_1} (φ : BilatInqProp W) : (bang φ).falsity = φ.falsity

theorem MinimalCovering.alt_bang_pro {W : Type u_1} (φ : BilatInqProp W) : (Kalman.pro (bang φ)).alt = {φ.truth}

!φ offers the single alternative info ⟦φ⟧⁺.

The bilateral modals

def MinimalCovering.necessity {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : BilatInqProp W

Necessity: true where the positive alternatives of the prejacent minimally cover the relevant worlds, false where its negative alternatives minimally cover a nonempty part of them.

Equations

• MinimalCovering.necessity R φ = Kalman.mk (MinimalCovering.box R (Kalman.pro φ)) (MinimalCovering.dia R (Kalman.con φ)) ⋯

def MinimalCovering.possibility {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : BilatInqProp W

Possibility: true where the positive alternatives of the prejacent minimally cover a nonempty part of the relevant worlds, false where its negative alternatives minimally cover them.

Equations

• MinimalCovering.possibility R φ = Kalman.mk (MinimalCovering.dia R (Kalman.pro φ)) (MinimalCovering.box R (Kalman.con φ)) ⋯

theorem MinimalCovering.possibility_eq_compl_necessity_compl {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : possibility R φ = (necessity R φᶜ)ᶜ

The duality of the modals: ◇φ = ¬□¬φ.

theorem MinimalCovering.necessity_eq_compl_possibility_compl {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : necessity R φ = (possibility R φᶜ)ᶜ

The duality of the modals: □φ = ¬◇¬φ.

@[simp]

theorem MinimalCovering.truth_necessity {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : (necessity R φ).truth = {w : W | IsMinCover (Kalman.pro φ).alt (R w)}

@[simp]

theorem MinimalCovering.falsity_necessity {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : (necessity R φ).falsity = {w : W | ∃ R' ⊆ R w, R'.Nonempty ∧ IsMinCover (Kalman.con φ).alt R'}

@[simp]

theorem MinimalCovering.truth_possibility {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : (possibility R φ).truth = {w : W | ∃ R' ⊆ R w, R'.Nonempty ∧ IsMinCover (Kalman.pro φ).alt R'}

@[simp]

theorem MinimalCovering.falsity_possibility {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : (possibility R φ).falsity = {w : W | IsMinCover (Kalman.con φ).alt (R w)}

theorem MinimalCovering.truth_necessity_of_alt_eq_singleton {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) {A : Set W} (h : (Kalman.pro φ).alt = {A}) : (necessity R φ).truth = {w : W | (R w).Nonempty ∧ R w ⊆ A}

Over a single alternative A, necessity is orthodox: true where the relevant worlds are nonempty and inside A.

theorem MinimalCovering.truth_possibility_of_alt_eq_singleton {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) {A : Set W} (h : (Kalman.pro φ).alt = {A}) : (possibility R φ).truth = {w : W | (R w ∩ A).Nonempty}

Over a single alternative A, possibility is orthodox: true where some relevant world lies in A.

theorem MinimalCovering.falsity_necessity_of_alt_eq_singleton {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) {B : Set W} (h : (Kalman.con φ).alt = {B}) : (necessity R φ).falsity = {w : W | (R w ∩ B).Nonempty}

Over a single negative alternative B, necessity is false where some relevant world lies in B.

theorem MinimalCovering.falsity_possibility_of_alt_eq_singleton {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) {B : Set W} (h : (Kalman.con φ).alt = {B}) : (possibility R φ).falsity = {w : W | (R w).Nonempty ∧ R w ⊆ B}

Over a single negative alternative B, possibility is false where the relevant worlds are nonempty and inside B.

Conditionals and the language

def MinimalCovering.updateAccess {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) (w : W) : Set W

The accessibility update by φ: the relevant worlds at which φ is true.

Equations

• MinimalCovering.updateAccess R φ w = R w ∩ φ.truth

inductive MinimalCovering.Formula (At : Type u_2) : Type u_2

The language: atoms, negation, conjunction, disjunction, the inquisitive !, the restrictor conditional, and the two modals.

• atom {At : Type u_2} (p : At) : Formula At
• neg {At : Type u_2} (φ : Formula At) : Formula At
• conj {At : Type u_2} (φ ψ : Formula At) : Formula At
• disj {At : Type u_2} (φ ψ : Formula At) : Formula At
• bang {At : Type u_2} (φ : Formula At) : Formula At
• cond {At : Type u_2} (φ ψ : Formula At) : Formula At
• box {At : Type u_2} (φ : Formula At) : Formula At
• diamond {At : Type u_2} (φ : Formula At) : Formula At

def MinimalCovering.Formula.eval {W : Type u_1} {At : Type u_2} (V : At → Set W) : (W → Set W) → Formula At → BilatInqProp W

The interpretation of a sentence in the model ⟨W, R, V⟩. The restrictor conditional evaluates its consequent under the accessibility updated by its antecedent.

Equations

• MinimalCovering.Formula.eval V x✝ (MinimalCovering.Formula.atom p) = MinimalCovering.atom (V p)
• MinimalCovering.Formula.eval V x✝ φ.neg = (MinimalCovering.Formula.eval V x✝ φ)ᶜ
• MinimalCovering.Formula.eval V x✝ (φ.conj ψ) = MinimalCovering.Formula.eval V x✝ φ ⊓ MinimalCovering.Formula.eval V x✝ ψ
• MinimalCovering.Formula.eval V x✝ (φ.disj ψ) = MinimalCovering.Formula.eval V x✝ φ ⊔ MinimalCovering.Formula.eval V x✝ ψ
• MinimalCovering.Formula.eval V x✝ φ.bang = MinimalCovering.bang (MinimalCovering.Formula.eval V x✝ φ)
• MinimalCovering.Formula.eval V x✝ (φ.cond ψ) = MinimalCovering.Formula.eval V (MinimalCovering.updateAccess x✝ (MinimalCovering.Formula.eval V x✝ φ)) ψ
• MinimalCovering.Formula.eval V x✝ φ.box = MinimalCovering.necessity x✝ (MinimalCovering.Formula.eval V x✝ φ)
• MinimalCovering.Formula.eval V x✝ φ.diamond = MinimalCovering.possibility x✝ (MinimalCovering.Formula.eval V x✝ φ)