Possibilities

This file defines a possibility — a world paired with an assignment of discourse referents — and the structure of its partial points, with Part-valued assignments (partial functions V →. M): the descent order, compatibility and union, restriction, and the classification of each stratum as world–assignment pairs.

References

• [GSV96], [ES25a]
• [KvGR11], Def. 0.22
• [Hei82]

structure DynamicSemantics.Possibility (W : Type u_1) (V : Type u_2) (M : Type u_3) : Type (max (max u_1 u_2) u_3)

A possibility is a world paired with an assignment of discourse referents to individuals.

• world : W

  The world coordinate.

• assignment : V → M

  The assignment of discourse referents.

theorem DynamicSemantics.Possibility.ext {W : Type u_1} {V : Type u_2} {M : Type u_3} {x y : Possibility W V M} (world : x.world = y.world) (assignment : x.assignment = y.assignment) : x = y

theorem DynamicSemantics.Possibility.ext_iff {W : Type u_1} {V : Type u_2} {M : Type u_3} {x y : Possibility W V M} : x = y ↔ x.world = y.world ∧ x.assignment = y.assignment

def DynamicSemantics.Possibility.update {W : Type u_1} {V : Type u_2} {M : Type u_3} (p : Possibility W V M) [DecidableEq V] (x : V) (e : M) : Possibility W V M

Update the assignment at a single referent.

Equations

• p.update x e = { world := p.world, assignment := Function.update p.assignment x e }

@[simp]

theorem DynamicSemantics.Possibility.update_world {W : Type u_1} {V : Type u_2} {M : Type u_3} (p : Possibility W V M) [DecidableEq V] (x : V) (e : M) : (p.update x e).world = p.world

@[simp]

theorem DynamicSemantics.Possibility.update_assignment {W : Type u_1} {V : Type u_2} {M : Type u_3} (p : Possibility W V M) [DecidableEq V] (x : V) (e : M) : (p.update x e).assignment = Function.update p.assignment x e

Partial points

@[implicit_reducible]

instance DynamicSemantics.Possibility.instPartialOrderPart {W : Type u_1} {V : Type u_2} {M : Type u_3} : PartialOrder (Possibility W V (Part M))

p ≤ q iff p and q share their world and the assignments grow pointwise in the order of partial values.

Equations

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

theorem DynamicSemantics.Possibility.le_def {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} : p ≤ q ↔ p.world = q.world ∧ ∀ (x : V), p.assignment x ≤ q.assignment x

def DynamicSemantics.Possibility.domain {W : Type u_1} {V : Type u_2} {M : Type u_3} (p : Possibility W V (Part M)) : Set V

The domain of a partial point is the set of referents it defines.

Equations

• p.domain = PFun.Dom p.assignment

@[simp]

theorem DynamicSemantics.Possibility.mem_domain {W : Type u_1} {V : Type u_2} {M : Type u_3} {p : Possibility W V (Part M)} {v : V} : v ∈ p.domain ↔ (p.assignment v).Dom

theorem DynamicSemantics.Possibility.domain_mono {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} (h : p ≤ q) : p.domain ⊆ q.domain

Descent grows the domain.

theorem DynamicSemantics.Possibility.eq_of_le_of_domain_eq {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} (h : p ≤ q) (hdom : p.domain = q.domain) : p = q

On a shared domain, descent is equality — there is no room to grow.

theorem DynamicSemantics.Possibility.domain_eq_empty_iff {W : Type u_1} {V : Type u_2} {M : Type u_3} {p : Possibility W V (Part M)} : p.domain = ∅ ↔ ∀ (v : V), p.assignment v = ⊥

A point defines no referent exactly when its assignment is nowhere defined.

noncomputable def DynamicSemantics.Possibility.union {W : Type u_1} {V : Type u_2} {M : Type u_3} (p q : Possibility W V (Part M)) : Possibility W V (Part M)

The union of two points, defined wherever either is, with the left taking precedence; on compatible points the precedence is immaterial (union_comm).

Equations

• p.union q = { world := p.world, assignment := fun (v : V) => (p.assignment v).or (q.assignment v) }

@[simp]

theorem DynamicSemantics.Possibility.union_world {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} : (p.union q).world = p.world

@[simp]

theorem DynamicSemantics.Possibility.union_assignment {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} (v : V) : (p.union q).assignment v = (p.assignment v).or (q.assignment v)

theorem DynamicSemantics.Possibility.le_union_left {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} : p ≤ p.union q

theorem DynamicSemantics.Possibility.union_le {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q u : Possibility W V (Part M)} (hp : p ≤ u) (hq : q ≤ u) : p.union q ≤ u

theorem DynamicSemantics.Possibility.compat_iff_forall {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} : Compat p q ↔ p.world = q.world ∧ ∀ (v : V), Compat (p.assignment v) (q.assignment v)

Compatibility of partial points is worldwise and pointwise.

theorem DynamicSemantics.Possibility.compat_iff {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} : Compat p q ↔ p.world = q.world ∧ ∀ (v : V) (e e' : M), e ∈ p.assignment v → e' ∈ q.assignment v → e = e'

Two partial points are compatible (Compat: bounded above in the descent order) exactly when they share their world and agree wherever both are defined — the requirement in [KvGR11], Def. 0.26, that the union of chosen points be a function.

theorem DynamicSemantics.Possibility.le_union_right {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} (h : Compat p q) : q ≤ p.union q

theorem DynamicSemantics.Possibility.isLUB_union {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} (h : Compat p q) : IsLUB {p, q} (p.union q)

The union of compatible points is their least upper bound.

theorem DynamicSemantics.Possibility.isLUB_pair_iff {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q u : Possibility W V (Part M)} : IsLUB {p, q} u ↔ Compat p q ∧ u = p.union q

The joins of pairs of points: u bounds {p, q} least exactly when the pair is compatible and u is its union.

theorem DynamicSemantics.Possibility.domain_union {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} : (p.union q).domain = p.domain ∪ q.domain

The union of two points defines the union of their domains.

theorem DynamicSemantics.Possibility.eq_of_compat_of_domain_eq {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} (h : Compat p q) (hdom : p.domain = q.domain) : p = q

On a shared domain, compatibility is equality.

theorem DynamicSemantics.Possibility.union_assoc {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q r : Possibility W V (Part M)} : (p.union q).union r = p.union (q.union r)

@[simp]

theorem DynamicSemantics.Possibility.union_self {W : Type u_1} {V : Type u_2} {M : Type u_3} {p : Possibility W V (Part M)} : p.union p = p

theorem DynamicSemantics.Possibility.union_comm {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} (h : Compat p q) : p.union q = q.union p

On compatible points the left precedence of union is immaterial.

The empty point

def DynamicSemantics.Possibility.bot {W : Type u_1} {V : Type u_2} {M : Type u_3} (w : W) : Possibility W V (Part M)

The empty point at a world: no referent defined.

Equations

• DynamicSemantics.Possibility.bot w = { world := w, assignment := fun (x : V) => ⊥ }

theorem DynamicSemantics.Possibility.bot_le {W : Type u_1} {V : Type u_2} {M : Type u_3} {p : Possibility W V (Part M)} : bot p.world ≤ p

theorem DynamicSemantics.Possibility.bot_le_of_compat {W : Type u_1} {V : Type u_2} {M : Type u_3} {p : Possibility W V (Part M)} {w : W} (h : Compat p (bot w)) : bot w ≤ p

An empty point compatible with p shares its world, hence sits below it.

@[simp]

theorem DynamicSemantics.Possibility.union_bot {W : Type u_1} {V : Type u_2} {M : Type u_3} {p : Possibility W V (Part M)} {w : W} : p.union (bot w) = p

@[simp]

theorem DynamicSemantics.Possibility.domain_bot {W : Type u_1} {V : Type u_2} {M : Type u_3} {w : W} : (bot w).domain = ∅

Restriction and the indexed classification

def DynamicSemantics.Possibility.restrict {W : Type u_1} {V : Type u_2} {M : Type u_3} (X : Set V) (p : Possibility W V (Part M)) : Possibility W V (Part M)

Restrict a partial point to the referents in X.

Equations

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

@[simp]

theorem DynamicSemantics.Possibility.restrict_world {W : Type u_1} {V : Type u_2} {M : Type u_3} {p : Possibility W V (Part M)} {X : Set V} : (restrict X p).world = p.world

theorem DynamicSemantics.Possibility.restrict_le {W : Type u_1} {V : Type u_2} {M : Type u_3} {p : Possibility W V (Part M)} {X : Set V} : restrict X p ≤ p

Restriction descends.

theorem DynamicSemantics.Possibility.domain_restrict {W : Type u_1} {V : Type u_2} {M : Type u_3} {p : Possibility W V (Part M)} {X : Set V} : (restrict X p).domain = X ∩ p.domain

Restriction intersects the domain.

theorem DynamicSemantics.Possibility.le_iff_eq_restrict {W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Part M)} {X : Set V} (hp : p.domain = X) : p ≤ q ↔ p = restrict X q

A point with domain X descends into q exactly when it is q restricted to X.

theorem DynamicSemantics.Possibility.restrict_eq_self {W : Type u_1} {V : Type u_2} {M : Type u_3} {p : Possibility W V (Part M)} {X : Set V} (hp : p.domain = X) : restrict X p = p

A point at its own domain is fixed by restriction.

theorem DynamicSemantics.Possibility.restrict_restrict {W : Type u_1} {V : Type u_2} {M : Type u_3} {p : Possibility W V (Part M)} {X Y : Set V} : restrict X (restrict Y p) = restrict (X ∩ Y) p

Consecutive restrictions restrict to the intersection.

def DynamicSemantics.Possibility.domainEquiv {W : Type u_1} {V : Type u_2} {M : Type u_3} (X : Set V) : { p : Possibility W V (Part M) // p.domain = X } ≃ W × (↑X → M)

Partial points with domain X are exactly world–X-assignment pairs.

Equations

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

theorem DynamicSemantics.Possibility.restrict_domainEquiv_symm {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (h : Y ⊆ X) (e : W × (↑X → M)) : restrict Y ↑((domainEquiv X).symm e) = ↑((domainEquiv Y).symm (e.1, fun (v : ↑Y) => e.2 ⟨↑v, ⋯⟩))

Restricting a classified point restricts its chart.

Instantiations

Update systems share one form — states are sets of points, updates act on states — and differ in the point. The parameters select the system: worlds only gives propositional update semantics ([Vel96]; the ∅-fiber), assignments only gives lifted DPL, and the general form is FCS/DRT's pairs. Propositional inquisitive semantics instead iterates the construction — its points are sets of worlds — a level shift, not a parameter choice.

def DynamicSemantics.Possibility.worldEquiv (W : Type u_4) (M : Type u_5) : Possibility W Empty M ≃ W

Worlds-only points are bare worlds — the points of propositional update semantics.

Equations

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

def DynamicSemantics.Possibility.assignmentEquiv (V : Type u_4) (M : Type u_5) : Possibility Unit V M ≃ (V → M)

Assignment-only points are bare assignments — the points of lifted DPL.

Equations

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