Situations: Partial Indices

[Kra89] [BP83]

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 Semantics/Intensional/ lets all higher modules opt in by adding [PartialOrder Index], without forcing a choice of "worlds vs. situations" in the index type.

Key definitions

• SituationFrame — entity/index types 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 E W — a situation frame on E/W 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 Semantics/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 Intensional.SituationFrame : Type 1

A situation frame carries an entity domain and an index set whose indices are equipped with a partial order (parthood). Worlds are the maximal elements; truly possible-worlds-style frames arise from the discrete order.

• Entity : Type

  The domain of individuals.

• Index : Type

  The index set (situations).

• order : PartialOrder self.Index

  The parthood preorder on indices.

@[reducible, inline]

abbrev Intensional.SituationFrame.Denot (F : SituationFrame) : Ty → Type

Denotation domains for a situation frame, computed from its entity and index types.

Equations

• F.Denot = Intensional.Denot F.Entity F.Index

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

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

Equations

• Intensional.«term_≼_» = Lean.ParserDescr.trailingNode `Intensional.«term_≼_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≼ ") (Lean.ParserDescr.cat `term 51))

Persistence

@[reducible, inline]

abbrev 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

• Intensional.Persistent p = Monotone p

theorem 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 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 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 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

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

def 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 | 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 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

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

def Intensional.discreteSituationFrame (E W : Type) : SituationFrame

Build a situation frame from entity and index types using the discrete order on the index set. This is the formal witness that PWS is a special case of situation semantics.

Equations

• Intensional.discreteSituationFrame E W = { Entity := E, Index := W, order := Intensional.discreteOrder W }

@[implicit_reducible]

def Intensional.instPartialOrder_linglib (W : Type) : PartialOrder W

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

Equations

• Intensional.instPartialOrder_linglib W = Intensional.discreteOrder W

theorem Intensional.discrete_isWorld_all (W : Type) (s : W) : IsWorld s

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

theorem Intensional.discrete_persistent_all (W : Type) (p : W → Prop) : Persistent p

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