Ordering semantics

Ordering semantics evaluates a modal or a conditional by ranking the worlds of a domain under a preorder, v ≤ u meaning that v comes at least as close as u to an ideal or to the world of evaluation. Lewis's truth condition needs neither comparability nor the Limit Assumption: t is a necessity over the domain when every world of the domain has one at least as close below which every world of the domain is a t-world. Kratzer's necessity over a modal base and an ordering source is this condition, and good possibility, which Portner and Rubinstein take from Kratzer as local necessity, asks for a single such world. The necessities over a domain are closed under intersection, the good possibilities are not.

Under the Limit Assumption necessity is truth at the minimal worlds, on a total preorder it is good possibility, and when the domain has a closest world all three coincide. The domain is the accessible worlds of Kratzer's modals, the antecedent-worlds of Lewis's counterfactuals, and the information of Veltman's expectation states.

Main definitions

• OrderingSemantics.IsNecessity p s t: every world of s has one at least as close all of whose worlds of s at least as close are in t.
• OrderingSemantics.IsGoodPossibility p s t: some world of s has only t-worlds among the worlds of s at least as close.

Main statements

• OrderingSemantics.isNecessity_iff_minimals_subset: under the Limit Assumption necessity is truth at the minimal worlds.
• OrderingSemantics.isNecessity_iff_isGoodPossibility_of_total: on a total preorder necessity is good possibility.
• OrderingSemantics.isGoodPossibility_iff_isNecessity_of_least: when the domain has a closest world the two coincide.
• OrderingSemantics.exists_not_isGoodPossibility_inter: the good possibilities are not closed under intersection; OrderingSemantics/Topology.lean reads both forces in the lower-set topology.

References

• [Lew81]
• [Lew73b]
• [Kra12b]
• [PR20]

def OrderingSemantics.IsNecessity {W : Type u_1} (p : Preorder W) (s t : Set W) : Prop

t is a necessity over s when every world of s has a world of s at least as close, all of whose worlds of s at least as close are in t.

Equations

• OrderingSemantics.IsNecessity p s t = ∀ u ∈ s, ∃ v ∈ s, v ≤ u ∧ ∀ w ∈ s, w ≤ v → w ∈ t

def OrderingSemantics.IsGoodPossibility {W : Type u_1} (p : Preorder W) (s t : Set W) : Prop

t is a good possibility over s when some world of s has only t-worlds among the worlds of s at least as close.

Equations

• OrderingSemantics.IsGoodPossibility p s t = ∃ v ∈ s, ∀ w ∈ s, w ≤ v → w ∈ t

Closure properties

theorem OrderingSemantics.IsNecessity.mono {W : Type u_1} {p : Preorder W} {s t t' : Set W} (h : IsNecessity p s t) (htt' : t ⊆ t') : IsNecessity p s t'

theorem OrderingSemantics.isNecessity_univ {W : Type u_1} (p : Preorder W) (s : Set W) : IsNecessity p s Set.univ

theorem OrderingSemantics.IsNecessity.inter {W : Type u_1} {p : Preorder W} {s t t' : Set W} (h : IsNecessity p s t) (h' : IsNecessity p s t') : IsNecessity p s (t ∩ t')

The necessities over a domain are closed under intersection.

theorem OrderingSemantics.IsGoodPossibility.mono {W : Type u_1} {p : Preorder W} {s t t' : Set W} (h : IsGoodPossibility p s t) (htt' : t ⊆ t') : IsGoodPossibility p s t'

theorem OrderingSemantics.exists_not_isGoodPossibility_inter : ∃ (p : Preorder Bool) (t : Set Bool) (t' : Set Bool), IsGoodPossibility p Set.univ t ∧ IsGoodPossibility p Set.univ t' ∧ ¬IsGoodPossibility p Set.univ (t ∩ t')

The good possibilities are not closed under intersection. Under the identity order on Bool each world is a branch of its own, so {true} and {false} are good possibilities and their empty intersection is not.

Necessity and the minimal worlds

theorem OrderingSemantics.IsNecessity.minimals_subset {W : Type u_1} {p : Preorder W} {s t : Set W} (h : IsNecessity p s t) : p.minimals s ⊆ t

A necessity holds at every minimal world.

theorem OrderingSemantics.isNecessity_of_minimals_subset {W : Type u_1} {p : Preorder W} {s t : Set W} (hlim : ∀ u ∈ s, ∃ v ∈ p.minimals s, v ≤ u) (h : p.minimals s ⊆ t) : IsNecessity p s t

Under the Limit Assumption, what holds at every minimal world is a necessity.

theorem OrderingSemantics.isNecessity_iff_minimals_subset {W : Type u_1} {p : Preorder W} {s t : Set W} (hlim : ∀ u ∈ s, ∃ v ∈ p.minimals s, v ≤ u) : IsNecessity p s t ↔ p.minimals s ⊆ t

Necessity and good possibility

theorem OrderingSemantics.IsNecessity.isGoodPossibility {W : Type u_1} {p : Preorder W} {s t : Set W} (h : IsNecessity p s t) (hs : s.Nonempty) : IsGoodPossibility p s t

Over a nonempty domain a necessity is a good possibility.

theorem OrderingSemantics.IsGoodPossibility.isNecessity_of_total {W : Type u_1} {p : Preorder W} {s t : Set W} (htot : Std.Total LE.le) (h : IsGoodPossibility p s t) : IsNecessity p s t

On a total preorder a good possibility is a necessity.

theorem OrderingSemantics.isNecessity_iff_isGoodPossibility_of_total {W : Type u_1} {p : Preorder W} {s t : Set W} (htot : Std.Total LE.le) (hs : s.Nonempty) : IsNecessity p s t ↔ IsGoodPossibility p s t

A closest world

When some world of the domain is at least as close as every world of the domain, necessity, good possibility and truth at the minimal worlds all reduce to truth at the worlds at least as close as it.

theorem OrderingSemantics.isGoodPossibility_iff_of_least {W : Type u_1} {p : Preorder W} {s t : Set W} {b : W} (hb : b ∈ s) (hleast : ∀ v ∈ s, b ≤ v) : IsGoodPossibility p s t ↔ ∀ w ∈ s, w ≤ b → w ∈ t

theorem OrderingSemantics.isNecessity_iff_of_least {W : Type u_1} {p : Preorder W} {s t : Set W} {b : W} (hb : b ∈ s) (hleast : ∀ v ∈ s, b ≤ v) : IsNecessity p s t ↔ ∀ w ∈ s, w ≤ b → w ∈ t

theorem OrderingSemantics.minimals_subset_iff_of_least {W : Type u_1} {p : Preorder W} {s t : Set W} {b : W} (hb : b ∈ s) (hleast : ∀ v ∈ s, b ≤ v) : p.minimals s ⊆ t ↔ ∀ w ∈ s, w ≤ b → w ∈ t

theorem OrderingSemantics.isGoodPossibility_iff_isNecessity_of_least {W : Type u_1} {p : Preorder W} {s t : Set W} {b : W} (hb : b ∈ s) (hleast : ∀ v ∈ s, b ≤ v) : IsGoodPossibility p s t ↔ IsNecessity p s t