Necessity and possibility over conversational backgrounds

Kratzer's modal operators are the box and diamond of Logic.Modal over the accessibility relations two conversational backgrounds induce. Simple necessity quantifies over the worlds a modal base makes accessible, and necessity over the best of them under an ordering source. Kratzer's own definition, human necessity, needs no Limit Assumption: each accessible world must see, at least as good, a witness below which only p-worlds occur. It is universal quantification over the best worlds exactly under the Limit Assumption, which every finite frame satisfies. Good possibility asks for one such witness, so p may hold on one branch of the ordering and its rival on another; Portner and Rubinstein call it local necessity. Both are the forces of ordering semantics (OrderingSemantics) over the accessible worlds ranked by the ordering source. When the ordering source is consistent with the modal base, the two backgrounds unify into one and both forces become simple necessity over their union.

Main definitions

• Background.ofRel R: the background whose accessible worlds are the R-successors.
• simpleNecessity f, simplePossibility f: the box and diamond of f.accessible.
• necessity f g, possibility f g: the box and diamond of bestAccessible f g.
• humanNecessity f g, humanPossibility f g, LimitAssumption f g w.
• goodPossibility f g: some accessible world sees only p-worlds at least as good.

Main statements

• humanNecessity_iff_necessity: under the Limit Assumption, human necessity is necessity.
• goodPossibility_iff_simpleNecessity_sup: with the ordering source consistent with the modal base, good possibility is simple necessity over the unified backgrounds.
• isRealistic_iff_simpleNecessity_le_id: a modal base is realistic exactly when simple necessity over it is veridical.
• simpleNecessity_iff_sInf_le: simple necessity is consequence from the premises at the world.

Implementation notes

necessity quantifies over bestWorlds directly, so studies that treat necessity and possibility as the Kratzer pair inherit the Limit Assumption; humanNecessity is the limit-free form. Kratzer's comparative possibility, weak necessity and slight possibility are not formalized here.

References

• [Kra77]
• [Kra81b]
• [Kra12b]
• [PR20]

Accessibility relations

def Modality.Background.accessible {W : Type u_1} (f : Background W) : SetRel W W

Under a modal base, w' is accessible from w when it satisfies every premise of f w, Kratzer's w' ∈ ⋂f(w).

Equations

• f.accessible = SetRel.ofSuccessors f.accessibleWorlds

def Modality.bestAccessible {W : Type u_1} (f g : Background W) : SetRel W W

Under a modal base and an ordering source, w' is best-accessible from w when it is among the best worlds accessible from w.

Equations

• Modality.bestAccessible f g = SetRel.ofSuccessors (Modality.bestWorlds f g)

@[simp]

theorem Modality.Background.mem_accessible {W : Type u_1} {f : Background W} {w w' : W} : (w, w') ∈ f.accessible ↔ w' ∈ f.accessibleWorlds w

def Modality.Background.ofRel {W : Type u_1} (R : SetRel W W) : Background W

The background of a relation, whose one premise at w is to be an R-successor of w.

Equations

• Modality.Background.ofRel R w = {fun (x : W) => (w, x) ∈ R}

@[simp]

theorem Modality.Background.accessibleWorlds_ofRel {W : Type u_1} (R : SetRel W W) (w : W) : (ofRel R).accessibleWorlds w = {v : W | (w, v) ∈ R}

@[simp]

theorem Modality.Background.accessible_ofRel {W : Type u_1} (R : SetRel W W) : (ofRel R).accessible = R

The background of a relation makes accessible exactly the relation's successors.

@[simp]

theorem Modality.mem_bestAccessible {W : Type u_1} {f g : Background W} {w w' : W} : (w, w') ∈ bestAccessible f g ↔ w' ∈ bestWorlds f g w

@[simp]

theorem Modality.bestAccessible_bot {W : Type u_1} (f : Background W) : bestAccessible f ⊥ = f.accessible

With the empty ordering source, best-world accessibility is base accessibility.

Operators

def Modality.simpleNecessity {W : Type u_1} (f : Background W) (p : W → Prop) (w : W) : Prop

Simple necessity holds when p holds at every accessible world, ⟦must⟧_f(p)(w) = ∀w' ∈ ⋂f(w). p(w'), Definition 5 of [Kra77].

Equations

• Modality.simpleNecessity f p w = ModalLogic.Box f.accessible p w

def Modality.simplePossibility {W : Type u_1} (f : Background W) (p : W → Prop) (w : W) : Prop

Simple possibility holds when p holds at some accessible world, ⟦can⟧_f(p)(w) = ∃w' ∈ ⋂f(w). p(w'), Definition 6 of [Kra77].

Equations

• Modality.simplePossibility f p w = ModalLogic.Diamond f.accessible p w

def Modality.necessity {W : Type u_1} (f g : Background W) (p : W → Prop) (w : W) : Prop

Necessity with an ordering source holds when p holds at every best world, ⟦must⟧_{f,g}(p)(w) = ∀w' ∈ Best(f,g,w). p(w'), the Limit Assumption form of humanNecessity.

Equations

• Modality.necessity f g p w = ModalLogic.Box (Modality.bestAccessible f g) p w

def Modality.possibility {W : Type u_1} (f g : Background W) (p : W → Prop) (w : W) : Prop

Possibility with an ordering source holds when p holds at some best world, ⟦can⟧_{f,g}(p)(w) = ∃w' ∈ Best(f,g,w). p(w').

Equations

• Modality.possibility f g p w = ModalLogic.Diamond (Modality.bestAccessible f g) p w

theorem Modality.necessity_mono {W : Type u_1} {f g : Background W} {p q : W → Prop} {w : W} (hpq : p ≤ q) (h : necessity f g p w) : necessity f g q w

Necessity is monotone in the prejacent, so Kratzer's must is closed under entailment (box_mono over the best accessible worlds).

theorem Modality.possibility_mono {W : Type u_1} {f g : Background W} {p q : W → Prop} {w : W} (hpq : p ≤ q) (h : possibility f g p w) : possibility f g q w

Possibility is monotone in the prejacent.

theorem Modality.necessity_and {W : Type u_1} {f g : Background W} {p q : W → Prop} {w : W} : necessity f g (fun (v : W) => p v ∧ q v) w ↔ necessity f g p w ∧ necessity f g q w

Necessity of a conjunction is the conjunction of necessities, box_inf over the best accessible worlds.

theorem Modality.necessity_and_left {W : Type u_1} {f g : Background W} {p q : W → Prop} {w : W} (h : necessity f g (fun (v : W) => p v ∧ q v) w) : necessity f g p w

Kratzer's must eliminates conjunction.

Human necessity

[Kra81b]'s official definition needs no Limit Assumption, asking each accessible world to see, at least as good, a witness below which only p-worlds occur. It is the necessity of ordering semantics over the accessible worlds ranked by the ordering source, and necessity, universal quantification over bestWorlds, is its Limit Assumption collapse.

def Modality.humanNecessity {W : Type u_1} (f g : Background W) (p : W → Prop) (w : W) : Prop

Human necessity holds when every accessible world has an accessible world at least as good, below which p holds throughout ([Kra81b], restated as necessity in [Kra12b]).

Equations

• Modality.humanNecessity f g p w = OrderingSemantics.IsNecessity (Modality.premisePreorder (g w)) (f.accessibleWorlds w) {v : W | p v}

theorem Modality.humanNecessity_iff {W : Type u_1} {f g : Background W} {p : W → Prop} {w : W} : humanNecessity f g p w ↔ ∀ u ∈ f.accessibleWorlds w, ∃ v ∈ f.accessibleWorlds w, v ≤ u ∧ ∀ z ∈ f.accessibleWorlds w, z ≤ v → p z

theorem Modality.necessity_of_humanNecessity {W : Type u_1} {f g : Background W} {p : W → Prop} {w : W} (h : humanNecessity f g p w) : necessity f g p w

Human necessity implies best-worlds necessity, unconditionally.

def Modality.LimitAssumption {W : Type u_1} (f g : Background W) (w : W) : Prop

The Limit Assumption holds at w when every accessible world sees a best world at least as good.

Equations

• Modality.LimitAssumption f g w = ∀ u ∈ f.accessibleWorlds w, ∃ v ∈ Modality.bestWorlds f g w, v ≤ u

theorem Modality.LimitAssumption.of_finite {W : Type u_1} [Finite W] (f g : Background W) (w : W) : LimitAssumption f g w

The Limit Assumption holds on a finite frame, where every accessible world lies above a best one.

theorem Modality.humanNecessity_of_necessity {W : Type u_1} {f g : Background W} {p : W → Prop} {w : W} (hlim : LimitAssumption f g w) (h : necessity f g p w) : humanNecessity f g p w

Under the Limit Assumption, best-worlds necessity implies human necessity.

theorem Modality.humanNecessity_iff_necessity {W : Type u_1} {f g : Background W} {p : W → Prop} {w : W} (hlim : LimitAssumption f g w) : humanNecessity f g p w ↔ necessity f g p w

Under the Limit Assumption, [Kra81b]'s human necessity is exactly universal quantification over the best worlds.

def Modality.humanPossibility {W : Type u_1} (f g : Background W) (p : W → Prop) (w : W) : Prop

Human possibility is the dual of humanNecessity, holding when the negation is not a human necessity ([Kra12b]).

Equations

• Modality.humanPossibility f g p w = ¬Modality.humanNecessity f g (fun (v : W) => ¬p v) w

theorem Modality.humanPossibility_iff_possibility {W : Type u_1} {f g : Background W} {p : W → Prop} {w : W} (hlim : LimitAssumption f g w) : humanPossibility f g p w ↔ possibility f g p w

Under the Limit Assumption, human possibility is existential quantification over the best worlds.

theorem Modality.humanNecessity_bot_iff {W : Type u_1} (f : Background W) (p : W → Prop) (w : W) : humanNecessity f ⊥ p w ↔ simpleNecessity f p w

With the empty ordering source, human necessity is simple necessity, [Kra81b]'s equivalence for arbitrary f and empty g.

Good possibility

def Modality.goodPossibility {W : Type u_1} (f g : Background W) (p : W → Prop) (w : W) : Prop

Good possibility holds when some accessible world sees only p-worlds among the accessible worlds at least as good as itself, so that p holds throughout a branch of the ordering.

Equations

• Modality.goodPossibility f g p w = OrderingSemantics.IsGoodPossibility (Modality.premisePreorder (g w)) (f.accessibleWorlds w) {v : W | p v}

theorem Modality.goodPossibility_iff {W : Type u_1} {f g : Background W} {p : W → Prop} {w : W} : goodPossibility f g p w ↔ ∃ u ∈ f.accessibleWorlds w, ∀ v ∈ f.accessibleWorlds w, v ≤ u → p v

theorem Modality.goodPossibility_mono {W : Type u_1} {f g : Background W} {p q : W → Prop} {w : W} (h : ∀ (v : W), p v → q v) : goodPossibility f g p w → goodPossibility f g q w

theorem Modality.goodPossibility_of_humanNecessity {W : Type u_1} {f g : Background W} {p : W → Prop} {w : W} (hne : (f.accessibleWorlds w).Nonempty) (h : humanNecessity f g p w) : goodPossibility f g p w

Over a modal base with an accessible world, human necessity implies good possibility.

theorem Modality.goodPossibility_bot_iff {W : Type u_1} (f : Background W) (p : W → Prop) (w : W) : goodPossibility f ⊥ p w ↔ (f.accessibleWorlds w).Nonempty ∧ simpleNecessity f p w

With the empty ordering source, good possibility is simple necessity over a modal base with an accessible world.

Unified backgrounds

When some accessible world verifies every premise of the ordering source, it is at least as good as every accessible world, the worlds at least as good as it are those accessible under the unified background f ⊔ g, and the forces that read the ordering collapse to simple necessity over the unified background.

theorem Modality.simpleNecessity_sup_of_goodPossibility {W : Type u_1} {f g : Background W} {p : W → Prop} {w : W} (h : goodPossibility f g p w) : simpleNecessity (f ⊔ g) p w

Good possibility implies simple necessity over the unified backgrounds.

theorem Modality.simpleNecessity_sup_of_humanNecessity {W : Type u_1} {f g : Background W} {p : W → Prop} {w : W} (h : humanNecessity f g p w) : simpleNecessity (f ⊔ g) p w

Human necessity implies simple necessity over the unified backgrounds.

theorem Modality.goodPossibility_iff_simpleNecessity_sup {W : Type u_1} {f g : Background W} {p : W → Prop} {w : W} (h : ((f ⊔ g).accessibleWorlds w).Nonempty) : goodPossibility f g p w ↔ simpleNecessity (f ⊔ g) p w

When the ordering source is consistent with the modal base, good possibility is simple necessity over the unified backgrounds.

theorem Modality.humanNecessity_iff_simpleNecessity_sup {W : Type u_1} {f g : Background W} {p : W → Prop} {w : W} (h : ((f ⊔ g).accessibleWorlds w).Nonempty) : humanNecessity f g p w ↔ simpleNecessity (f ⊔ g) p w

When the ordering source is consistent with the modal base, human necessity is simple necessity over the unified backgrounds.

theorem Modality.goodPossibility_iff_humanNecessity {W : Type u_1} {f g : Background W} {p : W → Prop} {w : W} (h : ((f ⊔ g).accessibleWorlds w).Nonempty) : goodPossibility f g p w ↔ humanNecessity f g p w

When the ordering source is consistent with the modal base, good possibility is human necessity.

Characterization lemmas

@[simp]

theorem Modality.simpleNecessity_iff {W : Type u_1} (f : Background W) (p : W → Prop) (w : W) : simpleNecessity f p w ↔ ∀ w' ∈ f.accessibleWorlds w, p w'

@[simp]

theorem Modality.simplePossibility_iff {W : Type u_1} (f : Background W) (p : W → Prop) (w : W) : simplePossibility f p w ↔ ∃ w' ∈ f.accessibleWorlds w, p w'

@[simp]

theorem Modality.necessity_iff {W : Type u_1} (f g : Background W) (p : W → Prop) (w : W) : necessity f g p w ↔ ∀ w' ∈ bestWorlds f g w, p w'

@[simp]

theorem Modality.possibility_iff {W : Type u_1} (f g : Background W) (p : W → Prop) (w : W) : possibility f g p w ↔ ∃ w' ∈ bestWorlds f g w, p w'

theorem Modality.simpleNecessity_iff_sInf_le {W : Type u_1} (f : Background W) (p : W → Prop) (w : W) : simpleNecessity f p w ↔ sInf (f w) ≤ p

Simple necessity is consequence from the premises at the world, ⋂f(w) ⊆ p, Definition 5 of [Kra77].

theorem Modality.simplePossibility_iff_not_disjoint {W : Type u_1} (f : Background W) (p : W → Prop) (w : W) : simplePossibility f p w ↔ ¬Disjoint (sInf (f w)) p

Simple possibility is compatibility with the premises at the world, ⋂f(w) ∩ p ≠ ∅, Definition 6 of [Kra77].

@[simp]

theorem Modality.necessity_bot_iff {W : Type u_1} (f : Background W) (p : W → Prop) (w : W) : necessity f ⊥ p w ↔ simpleNecessity f p w

Necessity with the empty ordering source is simple necessity.

Monotonicity in the modal base

theorem Modality.simpleNecessity_mono {W : Type u_1} {f f' : Background W} {p : W → Prop} {w : W} (h : f w ⊆ f' w) (hNec : simpleNecessity f p w) : simpleNecessity f' p w

Premise growth preserves simple necessity, since more evidence leaves fewer accessible worlds and so at least as many necessities. This is [Kra12b]'s point about epistemic change over time, the approaching-man dialogue, where one conversational background represents evidence that grows as time goes by, and what must hold on the earlier evidence still must on the later.

theorem Modality.not_necessity_insert {W : Type u_1} {f g : Background W} {p q r : W → Prop} {w u : W} (hq : q ∈ g w) (hpq : ∀ (v : W), q v → ¬p v) (hu : u ∈ bestWorlds f g w) (huq : q u) (hur : ¬r u) : ¬necessity f (fun (v : W) => insert p (g v)) r w

Adding p to an ordering source that holds a proposition incompatible with p makes nothing necessary that a best world verifying the latter fails.

Frame conditions on Background.accessible

theorem Modality.Background.IsRealistic.refl {W : Type u_1} {f : Background W} (h : f.IsRealistic) : f.accessible.IsRefl

A realistic modal base gives reflexive accessibility.

theorem Modality.Background.IsRealistic.isSerial {W : Type u_1} {f : Background W} (h : f.IsRealistic) : ModalLogic.IsSerial f.accessible

A realistic base gives serial accessibility.

theorem Modality.isRealistic_iff_refl {W : Type u_1} {f : Background W} : f.IsRealistic ↔ f.accessible.IsRefl

A modal base is realistic exactly when its accessibility relation is reflexive.

theorem Modality.isRealistic_iff_simpleNecessity_le_id {W : Type u_1} {f : Background W} : f.IsRealistic ↔ simpleNecessity f ≤ id

A modal base is realistic exactly when simple necessity over it is veridical, what must be the case being the case, so T defines realism.

theorem Modality.isRealistic_iff_id_le_simplePossibility {W : Type u_1} {f : Background W} : f.IsRealistic ↔ id ≤ simplePossibility f

A modal base is realistic exactly when what is actual is possible over it. Read epistemically, an asserted fact can be a might; read deontically, everything actual is permitted.

theorem Modality.accessible_bot {W : Type u_1} (w w' : W) : (w, w') ∈ ⊥.accessible

Under the empty modal base, every world is accessible.

Modal axioms

theorem Modality.duality {W : Type u_1} (f g : Background W) (p : W → Prop) (w : W) : necessity f g p w ↔ ¬possibility f g (fun (w' : W) => ¬p w') w

Modal duality, □p ↔ ¬◇¬p, is the box-diamond duality (ModalLogic.not_diamond), since necessity is □[bestAccessible f g].

theorem Modality.necessity_K {W : Type u_1} (f g : Background W) (p q : W → Prop) (w : W) (hImpl : necessity f g (fun (w' : W) => p w' → q w') w) (hP : necessity f g p w) : necessity f g q w

Necessity distributes over implication, the K axiom □(p → q) → □p → □q.

theorem Modality.Background.IsTotallyRealistic.necessity_le_id {W : Type u_1} {f : Background W} (hTotal : f.IsTotallyRealistic) (g : Background W) : necessity f g ≤ id

Over a totally realistic base, necessity is veridical whatever the ordering source, the T axiom for full necessity.