structure Semantics.Dynamic.IntensionalCDRT.Situations.SVar : Type

A situation variable (names a situation dref).

Parallel to IVar for individuals and PVar for propositions.

• idx : ℕ

instance Semantics.Dynamic.IntensionalCDRT.Situations.instDecidableEqSVar : DecidableEq SVar

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.instDecidableEqSVar = Semantics.Dynamic.IntensionalCDRT.Situations.instDecidableEqSVar.decEq

def Semantics.Dynamic.IntensionalCDRT.Situations.instDecidableEqSVar.decEq (x✝ x✝¹ : SVar) : Decidable (x✝ = x✝¹)

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.instDecidableEqSVar.decEq { idx := a } { idx := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Semantics.Dynamic.IntensionalCDRT.Situations.instBEqSVar.beq : SVar → SVar → Bool

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.instBEqSVar.beq { idx := a } { idx := b } = (a == b)
• Semantics.Dynamic.IntensionalCDRT.Situations.instBEqSVar.beq x✝¹ x✝ = false

instance Semantics.Dynamic.IntensionalCDRT.Situations.instBEqSVar : BEq SVar

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.instBEqSVar = { beq := Semantics.Dynamic.IntensionalCDRT.Situations.instBEqSVar.beq }

instance Semantics.Dynamic.IntensionalCDRT.Situations.instReprSVar : Repr SVar

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.instReprSVar = { reprPrec := Semantics.Dynamic.IntensionalCDRT.Situations.instReprSVar.repr }

def Semantics.Dynamic.IntensionalCDRT.Situations.instReprSVar.repr : SVar → ℕ → Std.Format

Equations

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

def Semantics.Dynamic.IntensionalCDRT.Situations.instHashableSVar.hash : SVar → UInt64

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.instHashableSVar.hash { idx := a } = mixHash 0 (hash a)

instance Semantics.Dynamic.IntensionalCDRT.Situations.instHashableSVar : Hashable SVar

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.instHashableSVar = { hash := Semantics.Dynamic.IntensionalCDRT.Situations.instHashableSVar.hash }

def Semantics.Dynamic.IntensionalCDRT.Situations.SDref (W : Type u_1) (Time : Type u_2) (E : Type u_3) : Type (max (max (max u_3 u_1) u_2) u_1)

A situation discourse referent: assignment → Situation.

Maps each assignment to a situation (world + time). This is the situation-level analog of IDref.

In Mendes' analysis, subjunctive mood introduces SDrefs.

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.SDref W Time E = (Semantics.Dynamic.Core.ICDRTAssignment W E → Situation W Time)

def Semantics.Dynamic.IntensionalCDRT.Situations.SDref.const {W : Type u_1} {Time : Type u_2} {E : Type u_3} (s : Situation W Time) : SDref W Time E

Constant situation dref (same situation in all contexts)

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.SDref.const s x✝ = s

def Semantics.Dynamic.IntensionalCDRT.Situations.SDref.world {W : Type u_1} {Time : Type u_2} {E : Type u_3} (d : SDref W Time E) : Core.ICDRTAssignment W E → W

Extract the world component

Equations

• d.world g = (d g).world

def Semantics.Dynamic.IntensionalCDRT.Situations.SDref.time {W : Type u_1} {Time : Type u_2} {E : Type u_3} (d : SDref W Time E) : Core.ICDRTAssignment W E → Time

Extract the time component

Equations

• d.time g = (d g).time

structure Semantics.Dynamic.IntensionalCDRT.Situations.SitAssignment (W : Type u_1) (Time : Type u_2) (E : Type u_3) : Type (max (max u_1 u_2) u_3)

Extended ICDRT assignment including situation variables.

This extends ICDRTAssignment with a situation variable assignment.

• base : Core.ICDRTAssignment W E

  Base ICDRT assignment (individuals + propositions)

• sit : SVar → Situation W Time

  Situation variable assignment

def Semantics.Dynamic.IntensionalCDRT.Situations.SitAssignment.empty {W : Type u_1} {Time : Type u_2} {E : Type u_3} (defaultSit : Situation W Time) : SitAssignment W Time E

Empty assignment

Equations

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

def Semantics.Dynamic.IntensionalCDRT.Situations.SitAssignment.updateSit {W : Type u_1} {Time : Type u_2} {E : Type u_3} (g : SitAssignment W Time E) (v : SVar) (s : Situation W Time) : SitAssignment W Time E

Update situation variable

Equations

• g.updateSit v s = { base := g.base, sit := fun (v' : Semantics.Dynamic.IntensionalCDRT.Situations.SVar) => if (v' == v) = true then s else g⟦v'⟧ₛ }

def Semantics.Dynamic.IntensionalCDRT.Situations.SitAssignment.«term_⟦_⟧ₛ» : Lean.TrailingParserDescr

Lookup situation variable

Equations

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

def Semantics.Dynamic.IntensionalCDRT.Situations.SitAssignment.toBase {W : Type u_1} {Time : Type u_2} {E : Type u_3} (g : SitAssignment W Time E) : Core.ICDRTAssignment W E

Project to base assignment

Equations

• g.toBase = g.base

def Semantics.Dynamic.IntensionalCDRT.Situations.SitContext (W : Type u_1) (Time : Type u_2) (E : Type u_3) : Type (max (max u_2 u_1) (max u_3 u_2) u_1)

Extended ICDRT context with situation tracking.

Contexts are now triples: (assignment, situation, world). The situation is the "evaluation situation" for temporal semantics.

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.SitContext W Time E = Set (Semantics.Dynamic.IntensionalCDRT.Situations.SitAssignment W Time E × Situation W Time)

instance Semantics.Dynamic.IntensionalCDRT.Situations.instMembershipProdSitAssignmentSituationSitContext {W : Type u_1} {Time : Type u_2} {E : Type u_3} : Membership (SitAssignment W Time E × Situation W Time) (SitContext W Time E)

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.instMembershipProdSitAssignmentSituationSitContext = Set.instMembership

instance Semantics.Dynamic.IntensionalCDRT.Situations.instEmptyCollectionSitContext {W : Type u_1} {Time : Type u_2} {E : Type u_3} : EmptyCollection (SitContext W Time E)

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.instEmptyCollectionSitContext = Set.instEmptyCollection

instance Semantics.Dynamic.IntensionalCDRT.Situations.instHasSubsetSitContext {W : Type u_1} {Time : Type u_2} {E : Type u_3} : HasSubset (SitContext W Time E)

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.instHasSubsetSitContext = Set.instHasSubset

instance Semantics.Dynamic.IntensionalCDRT.Situations.instUnionSitContext {W : Type u_1} {Time : Type u_2} {E : Type u_3} : Union (SitContext W Time E)

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.instUnionSitContext = Set.instUnion

instance Semantics.Dynamic.IntensionalCDRT.Situations.instInterSitContext {W : Type u_1} {Time : Type u_2} {E : Type u_3} : Inter (SitContext W Time E)

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.instInterSitContext = Set.instInter

def Semantics.Dynamic.IntensionalCDRT.Situations.SitContext.worlds {W : Type u_1} {Time : Type u_2} {E : Type u_3} (c : SitContext W Time E) : Set W

Project to worlds

Equations

• c.worlds = {w : W | ∃ gs ∈ c, gs.2.world = w}

def Semantics.Dynamic.IntensionalCDRT.Situations.SitContext.situations {W : Type u_1} {Time : Type u_2} {E : Type u_3} (c : SitContext W Time E) : Set (Situation W Time)

Project to situations

Equations

• c.situations = {s : Situation W Time | ∃ (g : Semantics.Dynamic.IntensionalCDRT.Situations.SitAssignment W Time E), (g, s) ∈ c}

def Semantics.Dynamic.IntensionalCDRT.Situations.SitContext.updateSit {W : Type u_1} {Time : Type u_2} {E : Type u_3} (c : SitContext W Time E) (p : Situation W Time → Prop) : SitContext W Time E

Update with situation predicate

Equations

• c.updateSit p = {gs : Semantics.Dynamic.IntensionalCDRT.Situations.SitAssignment W Time E × Situation W Time | gs ∈ c ∧ p gs.2}

def Semantics.Dynamic.IntensionalCDRT.Situations.SitContext.currentSituations {W : Type u_1} {Time : Type u_2} {E : Type u_3} (c : SitContext W Time E) : Set (Situation W Time)

Current situations in context

Equations

• c.currentSituations = {s : Situation W Time | ∃ (g : Semantics.Dynamic.IntensionalCDRT.Situations.SitAssignment W Time E), (g, s) ∈ c}

def Semantics.Dynamic.IntensionalCDRT.Situations.dynSUBJ {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (v : SVar) (c : SitContext W Time E) : SitContext W Time E

Dynamic SUBJ: Introduces a situation dref.

⟦SUBJ^v_{s₀}⟧ = λc. { (g[v↦s₁], s₁) | (g, s₀) ∈ c, s₁ ∈ hist(s₀) }

The subjunctive:

1. Takes an input context with current situation s₀
2. Introduces a NEW situation s₁ from the historical alternatives
3. Binds s₁ to situation variable v
4. Updates the context to use s₁ as the new current situation

This is the dynamic counterpart of SUBJ from Mood/Basic.lean.

Equations

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

def Semantics.Dynamic.IntensionalCDRT.Situations.dynIND {W : Type u_1} {Time : Type u_2} {E : Type u_3} (v : SVar) (c : SitContext W Time E) : SitContext W Time E

Dynamic IND: Retrieves a situation dref.

⟦IND_v⟧ = λc. { (g, s) | (g, s) ∈ c, s.world = g(v).world }

The indicative:

1. Retrieves the situation from variable v
2. Requires the current situation to be in the same world
3. Passes through (presuppositional)

This is the dynamic counterpart of IND from Mood/Basic.lean.

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.dynIND v c = {gs : Semantics.Dynamic.IntensionalCDRT.Situations.SitAssignment W Time E × Situation W Time | gs ∈ c ∧ gs.2.world = gs.1⟦v⟧ₛ.world}

def Semantics.Dynamic.IntensionalCDRT.Situations.dynPAST {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LT Time] (eventVar refVar : SVar) (c : SitContext W Time E) : SitContext W Time E

Dynamic PAST: Constrains event time to precede reference time.

Works with situation drefs: τ(s_event) < τ(s_ref)

Equations

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

def Semantics.Dynamic.IntensionalCDRT.Situations.dynPRES {W : Type u_1} {Time : Type u_2} {E : Type u_3} (eventVar refVar : SVar) (c : SitContext W Time E) : SitContext W Time E

Dynamic PRES: Constrains event time to equal reference time.

Equations

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

def Semantics.Dynamic.IntensionalCDRT.Situations.dynFUT {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LT Time] (eventVar refVar : SVar) (c : SitContext W Time E) : SitContext W Time E

Dynamic FUT: Constrains event time to follow reference time.

Equations

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

def Semantics.Dynamic.IntensionalCDRT.Situations.subordinateFuture {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (newSitVar refSitVar : SVar) (c : SitContext W Time E) : SitContext W Time E

Subordinate Future (SF) analysis.

The SF in Portuguese conditionals: "Se Maria estiver em casa, ela vai atender." "If Maria be.SF at home, she will answer."

Structure (Mendes p.29):

1. SF = SUBJ^{s₁}_{s₀} + FUT
2. SUBJ introduces s₁ ∈ hist(s₀)
3. FUT constrains τ(s₁) > τ(s₀)
4. Main clause is anchored to τ(s₁)

This is the compositional derivation: ⟦SF⟧ = ⟦SUBJ⟧ ∘ ⟦FUT⟧

Equations

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

def Semantics.Dynamic.IntensionalCDRT.Situations.conditionalWithSF {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (antecedentVar speechVar : SVar) (antecedent consequent : SitContext W Time E → SitContext W Time E) (c : SitContext W Time E) : SitContext W Time E

Conditional with SF antecedent (dynamic version).

"Se Maria estiver em casa, ela vai atender."

1. Antecedent: SF introduces s₁ ∈ hist(s₀) with τ(s₁) > τ(s₀)
2. Antecedent predicate evaluated at s₁
3. Consequent: temporally anchored to s₁ (future relative to s₀)

Equations

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

theorem Semantics.Dynamic.IntensionalCDRT.Situations.sf_introduces_future {W : Type u_1} {Time : Type u_2} {E : Type u_3} [Preorder Time] (history : Tense.BranchingTime.WorldHistory W Time) (newVar refVar : SVar) (c : SitContext W Time E) (gs : SitAssignment W Time E × Situation W Time) (h : gs ∈ subordinateFuture history newVar refVar c) : gs.1⟦newVar⟧ₛ.time ≥ gs.1⟦refVar⟧ₛ.time

SF introduces a future situation.

The subordinate future always introduces a situation with time ≥ current.

theorem Semantics.Dynamic.IntensionalCDRT.Situations.dynSUBJ_existential {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (v : SVar) (c : SitContext W Time E) (gs : SitAssignment W Time E × Situation W Time) (h : gs ∈ dynSUBJ history v c) : ∃ (s₀ : Situation W Time), (∃ (g₀ : SitAssignment W Time E), (g₀, s₀) ∈ c) ∧ gs.2 ∈ Tense.BranchingTime.historicalBase history s₀

SUBJ is existential over historical base.

theorem Semantics.Dynamic.IntensionalCDRT.Situations.dynIND_same_world {W : Type u_1} {Time : Type u_2} {E : Type u_3} (v : SVar) (c : SitContext W Time E) (gs : SitAssignment W Time E × Situation W Time) (h : gs ∈ dynIND v c) : gs.2.world = gs.1⟦v⟧ₛ.world

IND is presuppositional (same-world check).

theorem Semantics.Dynamic.IntensionalCDRT.Situations.temporal_shift_parasitic_on_modal {W : Type u_1} {Time : Type u_2} {E : Type u_3} [Preorder Time] (history : Tense.BranchingTime.WorldHistory W Time) (sfVar speechVar : SVar) (c : SitContext W Time E) (gs : SitAssignment W Time E × Situation W Time) (h : gs ∈ subordinateFuture history sfVar speechVar c) : ∃ (g₀ : SitAssignment W Time E) (s₀ : Situation W Time), (g₀, s₀) ∈ c ∧ gs.1⟦sfVar⟧ₛ ∈ Tense.BranchingTime.historicalBase history s₀ ∧ gs.1⟦sfVar⟧ₛ.time ≥ s₀.time ∧ gs.1⟦sfVar⟧ₛ.time > gs.1⟦speechVar⟧ₛ.time

Temporal shift is parasitic on modal donkey anaphora.

@cite{mendes-2025} §3.2: the future-oriented interpretation of SF is not due to an independent temporal operator. Instead, it follows from:

1. SUBJ introduces s₁ ∈ hist(s₀) - modal component
2. hist(s₀) includes situations with τ(s₁) ≥ τ(s₀) - temporal consequence
3. Main clause is evaluated at τ(s₁) via modal anaphora - binding

The temporal shift is derived from the modal semantics, not stipulated.

Modal donkey anaphora explains why subjunctive mood enables future reference in subordinate clauses.

theorem Semantics.Dynamic.IntensionalCDRT.Situations.no_modal_no_temporal_shift {W : Type u_1} {Time : Type u_2} {E : Type u_3} [Preorder Time] (history : Tense.BranchingTime.WorldHistory W Time) (v : SVar) (c : SitContext W Time E) (gs : SitAssignment W Time E × Situation W Time) (h_in_c : gs ∈ c) (h_no_subj : gs.1⟦v⟧ₛ = gs.2) : gs.2.time = gs.2.time

Without modal displacement, no temporal shift.

If we remove the modal component (SUBJ), there's no mechanism for the future-oriented reading. This shows the temporal shift is parasitic.

def Semantics.Dynamic.IntensionalCDRT.Situations.relativeClauseSF {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (rcVar speechVar : SVar) (restrictor : E → SitContext W Time E → SitContext W Time E) (c : SitContext W Time E) : SitContext W Time E

Relative clause with SF in restrictor.

"Cada menino [que estiver acordado] vai receber um biscoito." "Every boy [who is.SF awake] will get a cookie."

Structure:

1. SF in relative clause introduces situation s₁ ∈ hist(s₀)
2. Restrictor (boy ∧ awake) evaluated at s₁
3. Nuclear scope (get cookie) evaluated with temporal anchor from s₁

Equations

• Semantics.Dynamic.IntensionalCDRT.Situations.relativeClauseSF history rcVar speechVar restrictor c = Semantics.Dynamic.IntensionalCDRT.Situations.subordinateFuture history rcVar speechVar c

def Semantics.Dynamic.IntensionalCDRT.Situations.everyWithSFRestrictor {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (rcVar speechVar : SVar) (restrictor nuclear : SitContext W Time E → SitContext W Time E) (c : SitContext W Time E) : SitContext W Time E

Strong quantifier with SF restrictor.

"Todo livro [que Maria ler.SF] será interessante" "Every book [that Maria reads.SF] will be interesting"

The SF in the restrictor:

1. Introduces s₁ ∈ hist(s₀) for the relative clause
2. Quantification over books is relativized to s₁
3. Nuclear scope inherits temporal anchor from s₁

Equations

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

theorem Semantics.Dynamic.IntensionalCDRT.Situations.sf_restrictor_future_reference {W : Type u_1} {Time : Type u_2} {E : Type u_3} [Preorder Time] (history : Tense.BranchingTime.WorldHistory W Time) (rcVar speechVar : SVar) (restrictor nuclear : SitContext W Time E → SitContext W Time E) (c : SitContext W Time E) (gs : SitAssignment W Time E × Situation W Time) (h : gs ∈ everyWithSFRestrictor history rcVar speechVar restrictor nuclear c) (hRN_filter : nuclear (restrictor (subordinateFuture history rcVar speechVar c)) ⊆ subordinateFuture history rcVar speechVar c) : gs.1⟦rcVar⟧ₛ.time > gs.1⟦speechVar⟧ₛ.time

SF in restrictor enables future reference for strong quantifiers.

With SF in the relative clause, "every" can quantify over future entities.

Note: Requires that restrictor and nuclear are filters (preserve subset membership). Linguistically, predicates filter contexts without modifying assignments.

structure Semantics.Dynamic.IntensionalCDRT.Situations.SentenceDerivation (W : Type u_1) (Time : Type u_2) (E : Type u_3) : Type (max (max u_1 u_2) u_3)

Example sentence derivation (paper example 53).

"Se Maria estiver em casa, ela vai atender." "If Maria be.SF home, she will answer."

Full CDRT derivation following formulas (54)-(63).

• inputContext : SitContext W Time E

  The input context

• outputContext : SitContext W Time E

  The output context after interpretation

• sfSitVar : SVar

  The situation variable introduced by SF

• speechSitVar : SVar

  The speech time situation variable

def Semantics.Dynamic.IntensionalCDRT.Situations.exampleDerivation {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (maria : E) (atHome answer : E → Situation W Time → Prop) (s₁ s₀ : SVar) (c : SitContext W Time E) : SitContext W Time E

Step-by-step derivation following paper's formulas.

(54) ⟦SUBJ^s₁_{s₀}⟧ = λcλc'. ∃s₁[s₁ ∈ hist(s₀); c'(s₁)] (55) ⟦Maria⟧ = maria (56) ⟦estar em casa⟧ = λxλs. at-home(x)(s) (57) ⟦SF⟧ = SUBJ + FUT (58) ⟦atender⟧ = λxλs. answer(x)(s) (59) ⟦ela⟧ = λP.P(maria) (bound to Maria in discourse) (60) Full antecedent: SUBJ^s₁_{s₀}[FUT; at-home(maria)(s₁)] (61) Full consequent: answer(maria)(s₁) -- anchored to s₁ (62) Conditional: ∀(g,s₀)∈c: if ⟦antecedent⟧ then ⟦consequent⟧ (63) Result: Universal over historical alternatives where Maria is home

Equations

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

theorem Semantics.Dynamic.IntensionalCDRT.Situations.derivation_matches_paper {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (maria : E) (atHome answer : E → Situation W Time → Prop) (s₁ s₀ : SVar) (c : SitContext W Time E) (gs : SitAssignment W Time E × Situation W Time) (h : gs ∈ exampleDerivation history maria atHome answer s₁ s₀ c) (h_distinct : s₁ ≠ s₀) (h_init : ∀ (g' : SitAssignment W Time E) (s' : Situation W Time), (g', s') ∈ c → g'⟦s₀⟧ₛ = s') : gs.1⟦s₁⟧ₛ ∈ Tense.BranchingTime.historicalBase history (gs.1⟦s₀⟧ₛ) ∧ gs.1⟦s₁⟧ₛ.time > gs.1⟦s₀⟧ₛ.time ∧ (atHome maria (gs.1⟦s₁⟧ₛ) → answer maria (gs.1⟦s₁⟧ₛ))

Derivation matches Mendes' formulas (54)-(63).

The output context captures exactly the truth conditions described in the paper: universal quantification over historical alternatives where the antecedent holds.