Docs / Semantics / Dynamic / Possibility

Possibilities

import Linglib.Semantics.Dynamic.Possibility · namespace DynamicSemantics

This file defines a possibility — a world paired with an assignment of discourse referents — and the structure of its partial points, whose assignments are PartialAssigns, Flat-valued: the descent order, compatibility and union, restriction, and the classification of each stratum as world–assignment pairs.

References

Groenendijk et al. 1996, Coreference and Modality
Kamp et al. 2011, Discourse Representation Theory formalized
Heim 1982, The Semantics of Definite and Indefinite Noun Phrases formalized

Declarations

Partial points

Two partial points are compatible iff they share their world and agree where both are defined (Kamp et al. 2011, Def. 26).

theorem Possibility.compat_iff L141–148

{W : Type u_1} {V : Type u_2} {M : Type u_3} {p q : Possibility W V (Flat M)} :

Compat p q ↔ p.world = q.world ∧ ∀ (v : V) (e e' : M), p.assignment v = ↑e → q.assignment v = ↑e' → e = e'

Built from

The empty point

Restriction and the indexed classification

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 (Veltman 1996; 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.

L315–321

L323–329