Dynamic mood operators

This file defines the dynamic counterparts of the static mood operators of Mood/Situation.lean: dynIND and dynSUBJ are the two basic operations of the powerset monad on contexts of world-time possibilities — a filter and a Kleisli bind. This eliminative/generative contrast is the classical two-sorted update repertoire of dynamic semantics ([GSV96]), and Grammatical.dynOp assigns an operator to each grammatical mood, so the polarity of a mood is a theorem about the assignment rather than a stipulated feature.

Contexts are level-0 states over Index.Possibility — the world coordinate is the current evaluation index, drefs are indices. dynIND is the spine's lift (test ·); dynIntroduce (the generative primitive behind dynSUBJ) is this file's genuine delta: a world-shifting introduction that extends the assignment at a fresh dref and moves the evaluation index to the introduced situation.

Main statements

• dynSUBJ_realizes_SUBJ: on singleton contexts, dynSUBJ realizes the static existential SUBJ of [Men25].
• dynOp_indicative_isEliminative, dynOp_subjunctive_introduces: the polarity contrast, derived from the dynOp assignment.
• dynIND_after_dynSUBJ_same_var: indicative retrieval of a just-introduced subjunctive variable is vacuous.

References

• [Hei82]: file change semantics — intersection for conditions, file-card creation for indefinites.
• [Vel96]: the eliminative test [φ]σ = {w ∈ σ : w ⊨ φ}.
• [GSV96]: eliminative tests and generative introductions for discourse referents.
• [Cha21], [dG06]: the monadic and continuation-style renderings; here dynIND is Set.filter and dynIntroduce is Set.bind.

def Mood.dynIntroduce {W : Type u_1} {Time : Type u_2} (gen : Intensional.Index W Time → Set (Intensional.Index W Time)) (v : ℕ) (c : Set (Intensional.Index.Possibility W Time)) : Set (Intensional.Index.Possibility W Time)

The generative update behind dynSUBJ: for each entry with assignment g and current index s, produce the entries ⟨s', Function.update g v s'⟩ for every s' ∈ gen s — extend the assignment at v and move the evaluation index to the introduced situation. Unlike a test filter, this is not eliminative: it can produce entries that did not appear in the input context.

Equations

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

theorem Mood.dynIntroduce_binds_current {W : Type u_1} {Time : Type u_2} (gen : Intensional.Index W Time → Set (Intensional.Index W Time)) {v : ℕ} {c : Set (Intensional.Index.Possibility W Time)} {p : Intensional.Index.Possibility W Time} (h : p ∈ dynIntroduce gen v c) : p.assignment v = p.world

After dynIntroduce gen v, looking up v in the assignment always returns the new current index — the structural property that makes a same-variable filter (dynIND v ∘ dynIntroduce gen v) vacuous.

theorem Mood.dynIntroduce_current_in_gen {W : Type u_1} {Time : Type u_2} (gen : Intensional.Index W Time → Set (Intensional.Index W Time)) {v : ℕ} {c : Set (Intensional.Index.Possibility W Time)} {p : Intensional.Index.Possibility W Time} (h : p ∈ dynIntroduce gen v c) : ∃ (s : Intensional.Index W Time), (∃ (g : ℕ → Intensional.Index W Time), { world := s, assignment := g } ∈ c) ∧ p.world ∈ gen s

Every output entry of dynIntroduce has its current index drawn from gen applied to some input index.

def Mood.dynIND {W : Type u_1} {Time : Type u_2} (v : ℕ) : Set (Intensional.Index.Possibility W Time) → Set (Intensional.Index.Possibility W Time)

Dynamic IND: the eliminative update filtering entries whose current index shares its world with the situation bound to v — the spine's test filter at sameWorld.

Equations

• Mood.dynIND v = DynamicSemantics.lift (DynamicSemantics.Update.test fun (p : Intensional.Index.Possibility W Time) => Mood.sameWorld p.world (p.assignment v))

The eliminative side

theorem Mood.dynIND_isEliminative {W : Type u_1} {Time : Type u_2} (v : ℕ) : DynamicSemantics.CCP.IsEliminative (dynIND v)

dynIND is a context filter.

theorem Mood.dynIND_same_world {W : Type u_1} {Time : Type u_2} {v : ℕ} {c : Set (Intensional.Index.Possibility W Time)} {p : Intensional.Index.Possibility W Time} (h : p ∈ dynIND v c) : p.world.world = (p.assignment v).world

Surviving dynIND means the current and bound situations share a world.

theorem Mood.dynIND_idempotent {W : Type u_1} {Time : Type u_2} (v : ℕ) (c : Set (Intensional.Index.Possibility W Time)) : dynIND v (dynIND v c) = dynIND v c

dynIND is idempotent.

def Mood.dynSUBJ {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (v : ℕ) : Set (Intensional.Index.Possibility W Time) → Set (Intensional.Index.Possibility W Time)

Dynamic SUBJ: the generative update sending each entry to its extensions at every historically accessible situation.

Equations

• Mood.dynSUBJ history v = Mood.dynIntroduce history.historicalBase v

The generative side

theorem Mood.dynSUBJ_existential {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (v : ℕ) (c : Set (Intensional.Index.Possibility W Time)) (p : Intensional.Index.Possibility W Time) (h : p ∈ dynSUBJ history v c) : ∃ (s₀ : Intensional.Index W Time), (∃ (g₀ : ℕ → Intensional.Index W Time), { world := s₀, assignment := g₀ } ∈ c) ∧ p.world ∈ history.historicalBase s₀

Every dynSUBJ output situation is drawn from the historical base of some input situation.

theorem Mood.dynSUBJ_binds_current {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (v : ℕ) (c : Set (Intensional.Index.Possibility W Time)) (p : Intensional.Index.Possibility W Time) (h : p ∈ dynSUBJ history v c) : p.assignment v = p.world

After dynSUBJ, looking up v returns the current situation.

Static ↔ dynamic bridge

theorem Mood.dynSUBJ_singleton_eq {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (v : ℕ) (g : ℕ → Intensional.Index W Time) (s₀ : Intensional.Index W Time) : dynSUBJ history v {{ world := s₀, assignment := g }} = {p : Intensional.Index.Possibility W Time | ∃ s₁ ∈ history.historicalBase s₀, p = { world := s₁, assignment := Function.update g v s₁ }}

The exact output of dynSUBJ on a singleton context: ⟨s₁, g[v↦s₁]⟩ for each s₁ in the historical base of s₀.

theorem Mood.dynSUBJ_realizes_SUBJ {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (v : ℕ) (g : ℕ → Intensional.Index W Time) (s₀ : Intensional.Index W Time) (P : SitPred W Time) : (∃ p ∈ dynSUBJ history v {{ world := s₀, assignment := g }}, P (p.assignment v) s₀) ↔ SUBJ history P s₀

dynSUBJ realizes the static SUBJ: on a singleton context, some output satisfies P at the bound variable iff SUBJ holds.

theorem Mood.dynIND_after_dynSUBJ_same_var {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (v : ℕ) (c : Set (Intensional.Index.Possibility W Time)) : dynIND v (dynSUBJ history v c) = dynSUBJ history v c

Indicative retrieval of a just-introduced subjunctive variable is vacuous: the filter's projections are forced equal by dynSUBJ.

Mood as update polarity

def Mood.Grammatical.dynOp {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) : Grammatical → ℕ → Set (Intensional.Index.Possibility W Time) → Set (Intensional.Index.Possibility W Time)

The dynamic operator each grammatical mood denotes: indicative the eliminative dynIND, subjunctive the generative dynSUBJ.

Equations

• Mood.Grammatical.dynOp history Mood.Grammatical.indicative = Mood.dynIND
• Mood.Grammatical.dynOp history Mood.Grammatical.subjunctive = Mood.dynSUBJ history

theorem Mood.dynOp_indicative_isEliminative {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (v : ℕ) : DynamicSemantics.CCP.IsEliminative (Grammatical.dynOp history Grammatical.indicative v)

Indicative's dynamic operator is eliminative: a context filter.

theorem Mood.dynOp_subjunctive_introduces {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (v : ℕ) (c : Set (Intensional.Index.Possibility W Time)) (p : Intensional.Index.Possibility W Time) (h : p ∈ Grammatical.dynOp history Grammatical.subjunctive v c) : p.assignment v = p.world ∧ ∃ (s₀ : Intensional.Index W Time), (∃ (g₀ : ℕ → Intensional.Index W Time), { world := s₀, assignment := g₀ } ∈ c) ∧ p.world ∈ history.historicalBase s₀

Subjunctive's dynamic operator is generative: every output entry carries a freshly introduced situation, bound to v.