Docs / Semantics / Dynamic / OrderedInformationState

Ordered information states

import Linglib.Semantics.Dynamic.OrderedInformationState · namespace DynamicSemantics

Source

An ordered information state pairs a set of worlds, the information state of propositional update semantics (DynamicSemantics.State.worldOrderIso), with a preorder ranking worlds: Veltman's expectation pattern, the ordering of Portner's To-Do List, or a Kratzer ordering source. The states form a complete lattice whose top is Veltman's minimal state and whose bottom is his absurd state. Asserting φ and normally φ meet a state with their static meanings; a state accepts normally φ when the φ-worlds form a lower set of its pattern, and rules rank worlds as premises do. Presumably φ tests φ at the optimal worlds, where Portner's preferential necessity is evaluated.

Implementation notes

States are ordered by inclusion in both coordinates, so that a state with more information and more expectations lies lower; Veltman orders them the other way. Assertion and promotion never crash. Veltman identifies every state with empty information or an incoherent pattern with the absurd state, and his update with normally φ crashes when no normal world is a φ-world, so on a text that crashes his validity₁ and the one here can differ. His crashing updates are in Studies/Veltman1996.lean, as those of his section 4 on general rules.

TODO

Rank the points of the states of Dynamic/State.lean, world–assignment pairs, rather than bare worlds, so that a default can bind discourse referents, combining Veltman's defaults with the coreference of Groenendijk, Stokhof and Veltman.

References

Declarations

L55–62

The lattice of states

L81–83
L96
L97
L98
L99

Optimal worlds and necessity modals

L114–118
L120–125
L127–134

Updates

L138–140
L142–148
L151–155
L169–173

Acceptance

L182–185

A state accepts normally φ exactly when the φ-worlds form a lower set of its pattern (Preorder.le_ofCriterion_iff_isLowerSet), so that no world outside φ is ranked below a world inside it: a nonempty such φ is what Veltman calls a default of the pattern. A pattern is determined by its defaults, his Proposition 3.7, by Preorder.le_iff_forall_le_ofCriterion.

theorem OrderedInformationState.isFixedPt_promote_iffL187–193
{W : Type u_1} {σ : OrderedInformationState W} {φ : W → Prop} :
Function.IsFixedPt (fun (x : OrderedInformationState W) => x.promote φ) σ ↔ σ.order ≤ Preorder.ofCriterion φ

Built from ,

L195–199
L201–205

Texts of facts and of rules

L209–215

Promoting a list of propositions meets the pattern with the ordering they induce as premises, so that a pattern learnt from the minimal state ranks w below v when every rule that holds at v holds at w, as Veltman glosses patterns.

theorem OrderedInformationState.foldl_promote_orderL223–232
{W : Type u_1} (ps : List (W → Prop)) (σ : OrderedInformationState W) :
(List.foldl promote σ ps).order = σ.order ⊓ Modality.premisePreorder {p : W → Prop | p ∈ ps}

Built from ,