Ordering semantics in the lower-set topology

In the lower-set topology of a preorder the open sets are the lower sets, so the interior of t is the set of worlds all of whose predecessors are t-worlds, and a set is dense when every world has one of its worlds below it. Necessity in ordering semantics is then truth on a dense open set and good possibility truth on a nonempty open set. Two dense open sets meet in a dense open set, which is why necessities are closed under intersection, while two nonempty open sets can be disjoint, which is why good possibilities are not.

The forces over a domain are the forces over the domain as a preordered type in its own right, so the characterization holds over any domain in the lower-set topology of its restricted order.

Main statements

• OrderingSemantics.isNecessity_iff_dense_interior: necessity is truth on a dense open set.
• OrderingSemantics.isGoodPossibility_iff_nonempty_interior: good possibility is truth on a nonempty open set.

References

• [Lew81]

Over a whole preordered type

theorem OrderingSemantics.interior_eq_setOf_forall_le {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] {t : Set α} : interior t = {a : α | ∀ b ≤ a, b ∈ t}

In the lower-set topology the interior of t is the set of points all of whose predecessors are in t.

theorem OrderingSemantics.dense_iff_forall_exists_le {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] {D : Set α} : Dense D ↔ ∀ (a : α), ∃ d ∈ D, d ≤ a

In the lower-set topology a set is dense exactly when every point has one of its points below it.

theorem OrderingSemantics.isNecessity_univ_iff_dense_interior {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] {t : Set α} : IsNecessity inst✝ Set.univ t ↔ Dense (interior t)

theorem OrderingSemantics.isGoodPossibility_univ_iff_nonempty_interior {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] {t : Set α} : IsGoodPossibility inst✝ Set.univ t ↔ (interior t).Nonempty

Over a domain

theorem OrderingSemantics.isNecessity_iff_subtype {W : Type u_1} (p : Preorder W) (s t : Set W) : IsNecessity p s t ↔ IsNecessity (Preorder.lift Subtype.val) Set.univ (Subtype.val ⁻¹' t)

The necessities over a domain are the necessities over the domain as a preordered type.

theorem OrderingSemantics.isGoodPossibility_iff_subtype {W : Type u_1} (p : Preorder W) (s t : Set W) : IsGoodPossibility p s t ↔ IsGoodPossibility (Preorder.lift Subtype.val) Set.univ (Subtype.val ⁻¹' t)

The good possibilities over a domain are the good possibilities over the domain as a preordered type.

theorem OrderingSemantics.isNecessity_iff_dense_interior {W : Type u_1} (p : Preorder W) (s t : Set W) : IsNecessity p s t ↔ Dense (interior (Subtype.val ⁻¹' t))

t is a necessity over s exactly when its interior in the lower-set topology of s is dense.

theorem OrderingSemantics.isGoodPossibility_iff_nonempty_interior {W : Type u_1} (p : Preorder W) (s t : Set W) : IsGoodPossibility p s t ↔ (interior (Subtype.val ⁻¹' t)).Nonempty

t is a good possibility over s exactly when its interior in the lower-set topology of s is nonempty.