def Semantics.Dynamic.PLA.Formula.might {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) : Update E

Might φ: φ is consistent with the information state.

⟦might φ⟧(s) = s if ⟦φ⟧(s) ≠ ∅, else ∅

This is a TEST: it doesn't eliminate possibilities, it checks if φ is possible.

Equations

• Semantics.Dynamic.PLA.Formula.might M φ s = if Set.Nonempty (Semantics.Dynamic.PLA.Formula.update M φ s) then s else ∅

def Semantics.Dynamic.PLA.Formula.must {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) : Update E

Must φ: φ is supported by the information state.

⟦must φ⟧(s) = s if s ⊫[M] φ, else ∅

This is also a TEST: it passes only if φ is certain.

Equations

• Semantics.Dynamic.PLA.Formula.must M φ s = if s ⊫[M] φ then s else ∅

theorem Semantics.Dynamic.PLA.might_iff_consistent {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) : Formula.might M φ s = s ↔ Set.Nonempty (Formula.update M φ s) ∨ s = ∅

Might as consistency test: might φ passes iff some possibility satisfies φ.

theorem Semantics.Dynamic.PLA.must_iff_supports {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) : Formula.must M φ s = s ↔ (s ⊫[M] φ) ∨ s = ∅

Must as support test: must φ passes iff the state supports φ.

theorem Semantics.Dynamic.PLA.might_preserves_info {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) (h : Set.Nonempty (Formula.update M φ s)) : Formula.might M φ s = s

Testing doesn't change information (when it passes).

theorem Semantics.Dynamic.PLA.must_preserves_info {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) (h : s ⊫[M] φ) : Formula.must M φ s = s

theorem Semantics.Dynamic.PLA.might_subset {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) : Formula.might M φ s ⊆ s

@cite{veltman-1996}: Tests never add possibilities.

theorem Semantics.Dynamic.PLA.must_subset {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) : Formula.must M φ s ⊆ s

theorem Semantics.Dynamic.PLA.update_then_might {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) (s : InfoState E) : Core.CCP.seq (Formula.update M φ) (Formula.might M ψ) s = Formula.might M ψ (Formula.update M φ s)

Asserting then testing: φ; might ψ passes iff φ-update leaves room for ψ.

theorem Semantics.Dynamic.PLA.update_then_must {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) (s : InfoState E) : Core.CCP.seq (Formula.update M φ) (Formula.must M ψ) s = Formula.must M ψ (Formula.update M φ s)

Asserting then requiring: φ; must ψ passes iff φ-update supports ψ.

theorem Semantics.Dynamic.PLA.must_idempotent {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) : Formula.must M φ (Formula.must M φ s) = Formula.must M φ s

Must idempotence: must (must φ) ≡ must φ

Once we've verified certainty, re-checking doesn't change anything.

theorem Semantics.Dynamic.PLA.might_idempotent {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) : Formula.might M φ (Formula.might M φ s) = Formula.might M φ s

Might idempotence: might (might φ) ≡ might φ

Testing for consistency twice is the same as testing once.

theorem Semantics.Dynamic.PLA.supports_implies_might {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) (hs : Set.Nonempty s) (hsup : s ⊫[M] φ) : Formula.might M φ s = s

If s supports φ, then might φ passes.

theorem Semantics.Dynamic.PLA.supports_implies_must {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) (hsup : s ⊫[M] φ) : Formula.must M φ s = s

If s supports φ, then must φ passes.

theorem Semantics.Dynamic.PLA.might_iff_not_must_neg {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) (hs : Set.Nonempty s) : Formula.might M φ s = s ↔ Formula.must M (∼φ) s ≠ s

Modal duality: might φ passes iff must ¬φ fails (on nonempty states).

might φ passes on s ↔ must ¬φ fails on s (i.e., s does not support ¬φ). This is the dynamic version of the classical duality ◇φ ↔ ¬□¬φ.

@[reducible, inline]

abbrev Semantics.Dynamic.PLA.Concept (E : Type u_2) : Type u_2

A concept is a way of identifying entities across possibilities.

PLA-specific instance of Core.Intension: the index is an (Assignment E × WitnessSeq E) pair (a PLA possibility), and the value is an entity. This is the entity-side counterpart of Abusch 1997's Intension (KContext W E P T) T time-concept (Theories/Semantics/Tense/DeRe.lean).

Equations

• Semantics.Dynamic.PLA.Concept E = Core.Intension (Semantics.Dynamic.PLA.Assignment E × Semantics.Dynamic.PLA.WitnessSeq E) E

@[reducible, inline]

abbrev Semantics.Dynamic.PLA.Concept.isRigid {E : Type u_1} (c : Concept E) : Prop

A rigid concept identifies the same entity in all possibilities. Alias for Core.Intension.IsRigid at the PLA index.

Equations

• c.isRigid = Core.Intension.IsRigid c

def Semantics.Dynamic.PLA.Concept.isDescriptive {E : Type u_1} (c : Concept E) : Prop

A descriptive concept may identify different entities.

Equations

• c.isDescriptive = ¬c.isRigid

@[reducible, inline]

abbrev Semantics.Dynamic.PLA.Concept.const {E : Type u_1} (e : E) : Concept E

Constant concept: always refers to the same entity (proper names). Alias for Core.Intension.rigid at the PLA index.

Equations

• Semantics.Dynamic.PLA.Concept.const e = Core.Intension.rigid e

theorem Semantics.Dynamic.PLA.const_is_rigid {E : Type u_1} (e : E) : (Concept.const e).isRigid

def Semantics.Dynamic.PLA.Concept.fromVar {E : Type u_1} (i : VarIdx) : Concept E

Variable concept: looks up a variable in the assignment.

Equations

• Semantics.Dynamic.PLA.Concept.fromVar i p = p.1 i

def Semantics.Dynamic.PLA.Concept.fromPron {E : Type u_1} (i : PronIdx) : Concept E

Pronoun concept: looks up a pronoun in the witness sequence.

Equations

• Semantics.Dynamic.PLA.Concept.fromPron i p = p.2 i

Relationship to @cite{kratzer-1981} Modal Semantics

@cite{kratzer-1981}

PLA's epistemic operators share deep structure with Kratzer's modal semantics from Semantics.Modality.Kratzer. Both frameworks implement:

Common Pattern: Necessity as Universal Quantification

Framework	Necessity	Domain
Kratzer	∀w' ∈ accessible(w). φ(w')	Worlds
PLA	∀(g,ê) ∈ s. φ.sat M g ê	(Assignment, Witness) pairs

Key Structural Similarities

1. Modal base ≈ information state

   • Kratzer: Modal base f(w) determines accessible worlds via ∩f(w)
   • PLA: Information state s is the set of live possibilities

2. Necessity as test

   • Kratzer: □φ tests if φ holds at all best worlds
   • PLA: must φ tests if state supports φ (all possibilities satisfy φ)

3. Possibility as consistency

   • Kratzer: ◇φ tests if some accessible world satisfies φ
   • PLA: might φ tests if some possibility in s satisfies φ

4. Duality

   • Both satisfy: might φ ≈ ¬must ¬φ

Key Difference: Dynamic Dimension

PLA adds state transformation that Kratzer's propositional semantics lacks:

• Kratzer modals are purely propositional (World → Bool)
• PLA operators are state transformers (InfoState → InfoState)

This allows PLA to model:

• Discourse referent introduction
• Cross-sentential anaphora
• Dynamic conjunction (non-commutative)

Theoretical Unification

The relationship can be made precise: if we "freeze" the assignment and witness sequence, PLA's support relation reduces to Kratzer-style necessity over the remaining possibilities.

See Semantics.Modality.Kratzer for the full Kratzer framework with:

• Modal base and ordering source
• Preorder on worlds (kratzerPreorder)
• Frame correspondence theorems (T, D, 4, B, 5 axioms)
• Galois connection (extension/intension duality)