Situations: Partial Indices

@cite{kratzer-1989} @cite{barwise-perry-1983}

A situation is a partial point of evaluation. Where possible-worlds semantics evaluates propositions at total worlds, situation semantics evaluates them at situations equipped with a parthood preorder s ≤ s' ("s is a part of s'"). Worlds are recovered as the maximal situations.

This module provides the Core-level abstraction. The premise primitives in Premise.lean are already polymorphic over an abstract Index; this file simply refines that index to one carrying a partial order, and gives the parthood structure a name.

Why this is just an order, and lives in Core

Kratzer's situation semantics has many moving parts (lumping, accidental generalizations, persistence-respecting modal bases, ...) but the foundation is tiny: a partial order on indices. Persistence is then literally Monotone : (S → Prop) → Prop from mathlib. Possible-worlds semantics is the special case where ≤ is the discrete order (s ≤ s' ↔ s = s'), so every index is maximal.

Putting the abstraction in Core/Logic/Intensional/ lets all higher modules opt in by adding [PartialOrder Index], without forcing a choice of "worlds vs. situations" anywhere in Frame.

Key definitions

• SituationFrame — a Frame whose Index carries a partial order
• Persistent p — a proposition is true at s' whenever it is true at any s ≤ s' (= mathlib's Monotone)
• IsWorld s — s is maximal under ≤
• discreteSituationFrame — every Frame becomes a situation frame with the discrete order, where every index is a world (PWS reduct)

What lives elsewhere

The relation lumping between propositions and the distinction between accidental and non-accidental generalizations belong in Core/Logic/Intensional/Lumping.lean; those are theory-laden and depend on a chosen modal base. This file keeps only the order-theoretic core.

Situation frames

structure Core.Logic.Intensional.SituationFrameextends Core.Logic.Intensional.Frame : Type 1

A situation frame is an IL frame whose Index is equipped with a partial order (parthood). Worlds are the maximal elements; truly possible-worlds-style frames arise from the discrete order.

• Entity : Type
• Index : Type
• order : PartialOrder self.Index

  The parthood preorder on indices.

def Core.Logic.Intensional.«term_≼_» : Lean.TrailingParserDescr

s ≤ s' — s is a part of s' (situation parthood).

Equations

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

Persistence

@[reducible, inline]

abbrev Core.Logic.Intensional.Persistent {S : Type u_1} [Preorder S] (p : S → Prop) : Prop

A proposition is persistent iff it is monotone in parthood: truth at s carries up to any s' ≽ s.

This is precisely mathlib's Monotone; the abbreviation exists so that linguistic prose (Persistent p) and order-theoretic prose (Monotone p) are the same theorem.

Equations

• Core.Logic.Intensional.Persistent p = Monotone p

theorem Core.Logic.Intensional.Persistent.and {S : Type u_1} [Preorder S] {p q : S → Prop} (hp : Persistent p) (hq : Persistent q) : Persistent fun (s : S) => p s ∧ q s

Conjunction of persistent propositions is persistent.

theorem Core.Logic.Intensional.Persistent.or {S : Type u_1} [Preorder S] {p q : S → Prop} (hp : Persistent p) (hq : Persistent q) : Persistent fun (s : S) => p s ∨ q s

Disjunction of persistent propositions is persistent.

theorem Core.Logic.Intensional.Persistent.const_true {S : Type u_1} [Preorder S] : Persistent fun (x : S) => True

The True proposition is persistent.

Worlds as maximal situations

def Core.Logic.Intensional.IsWorld {S : Type u_1} [Preorder S] (s : S) : Prop

A situation is a world (in Kratzer's sense) iff it is maximal under parthood: nothing properly extends it.

Equations

• Core.Logic.Intensional.IsWorld s = ∀ (s' : S), s ≤ s' → s' ≤ s

def Core.Logic.Intensional.SituationFrame.Worlds (F : SituationFrame) : Set F.Index

The collection of worlds in a situation frame: the maximal indices.

Equations

• F.Worlds = {s : F.Index | Core.Logic.Intensional.IsWorld s}

Possible-worlds semantics as the discrete special case

The discrete partial order on a type makes s ≤ s' equivalent to s = s'. In that order every element is maximal, so every situation is a world — and Persistent p reduces to "no constraint at all." This is the formal sense in which possible-worlds semantics is the degenerate case of situation semantics.

@[reducible]

def Core.Logic.Intensional.discreteOrder (X : Type u_1) : PartialOrder X

The discrete partial order on any type: s ≤ s' ↔ s = s'. Marked @[reducible] so that the ≤ from this instance reduces definitionally to Eq for downstream proofs.

Equations

• Core.Logic.Intensional.discreteOrder X = { le := fun (a b : X) => a = b, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

def Core.Logic.Intensional.Frame.toDiscreteSituationFrame (F : Frame) : SituationFrame

Lift any frame to a situation frame using the discrete order on its index set. This is the formal witness that PWS is a special case of situation semantics.

Equations

• F.toDiscreteSituationFrame = { toFrame := F, order := Core.Logic.Intensional.discreteOrder F.Index }

@[implicit_reducible]

def Core.Logic.Intensional.instPartialOrderIndex (F : Frame) : PartialOrder F.Index

Bring the discrete partial order on F.Index into scope as an instance so the corollaries below can quantify over it without explicit @.

Equations

• Core.Logic.Intensional.instPartialOrderIndex F = Core.Logic.Intensional.discreteOrder F.Index

theorem Core.Logic.Intensional.discrete_isWorld_all (F : Frame) (s : F.Index) : IsWorld s

Under the discrete order, every element of a discrete situation frame is maximal — i.e., a world.

theorem Core.Logic.Intensional.discrete_persistent_all (F : Frame) (p : F.Index → Prop) : Persistent p

Under the discrete order on a frame, every proposition p : Index → Prop is automatically persistent: there's nothing to commute past.