structure Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.SitBinding (W : Type u_1) (Time : Type u_2) : Type (max u_1 u_2)

A situation variable is bound if it was introduced by SUBJ.

In classic DRT, a variable is bound if it was introduced by an existential quantifier or indefinite. Here, SUBJ plays the role of the indefinite.

• boundVar : Situations.SVar

  The variable that was introduced

• bindingSituation : Situation W Time

  The situation where binding occurred

• alternatives : Set (Situation W Time)

  The historical alternatives available at binding

def Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.SitBinding.isValid {W : Type u_1} {Time : Type u_2} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (b : SitBinding W Time) : Prop

Antecedent-contained binding: the bound variable's value is constrained to be in the historical alternatives of the binding situation.

This is the modal analog of the accessibility constraint in DRT.

Equations

• Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.SitBinding.isValid history b = (b.alternatives = Semantics.Tense.BranchingTime.historicalBase history b.bindingSituation)

def Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.modallyAccessible {W : Type u_1} {Time : Type u_2} (s₁ s₂ : Situation W Time) : Prop

Modal accessibility: a situation s₂ can anaphorically access s₁ if they share the same world (same-world constraint from IND).

This is formula (31) from the paper: IND_v = λP.[| w_{s₂} = w_{s₁}]; P(s₂)(s₁)

Equations

• Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.modallyAccessible s₁ s₂ = (s₂.world = s₁.world)

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

Donkey accessibility for situations: s₂ can retrieve s₁ if:

1. s₁ was introduced by SUBJ (in some local context)
2. s₂ satisfies the same-world constraint (IND)

This is the situation-level analog of the donkey accessibility condition.

• antecedent : Situation W Time

  The antecedent situation (introduced by SUBJ)

• consequent : Situation W Time

  The consequent situation (retrieves via IND)

• sameWorld : modallyAccessible self.antecedent self.consequent

  Same-world constraint satisfied

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

Cross-clausal situation binding: situation introduced in one clause can be retrieved in another clause via modal donkey anaphora.

SF in the antecedent of a conditional introduces a situation that the consequent can anaphorically access.

Example: "Se Maria estiver em casa, ela vai atender." ↑ SUBJ introduces s₁ ↑ IND retrieves s₁

Equations

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

theorem Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.cross_clausal_same_world {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (v : Situations.SVar) (c : Situations.SitContext W Time E) (gs : Situations.SitAssignment W Time E × Situation W Time) (h : gs ∈ crossClausualBinding history v v c) : gs.2.world = gs.1⟦v⟧ₛ.world

Cross-clausal binding preserves world identity.

When a situation is introduced in the antecedent and retrieved in the consequent, the two clauses are evaluated at the same world.

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

The SUBJ-IND anaphoric chain.

This represents the complete anaphoric dependency:

1. SUBJ^v introduces situation s₁ ∈ hist(s₀)
2. Antecedent predicate P is evaluated at s₁
3. IND_v retrieves s₁ for the consequent
4. Consequent Q is evaluated at the same world as s₁

The result: temporal properties of the consequent are "inherited" from the situation introduced by the subjunctive.

Equations

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

theorem Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.subj_ind_chain_modal_donkey {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (v : Situations.SVar) (P Q : Situations.SitContext W Time E → Situations.SitContext W Time E) (c : Situations.SitContext W Time E) (gs : Situations.SitAssignment W Time E × Situation W Time) (h : gs ∈ subjIndChain history v P Q c) (hQ_filter : Q (Situations.dynIND v (P (Situations.dynSUBJ history v c))) ⊆ Situations.dynIND v (P (Situations.dynSUBJ history v c))) : gs.2.world = gs.1⟦v⟧ₛ.world

The SUBJ-IND chain establishes modal donkey anaphora.

The consequent is evaluated at a world that agrees with the antecedent world up to the introduction time.

Note: Requires that Q is a filter (preserves subset membership and assignments). Linguistically, predicates filter contexts without modifying assignments.

structure Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.ClassicDonkey (E : Type u_1) : Type u_1

Classic donkey anaphora structure (for comparison).

"If a farmer owns a donkey, he beats it."

The indefinite "a donkey" introduces an individual dref that is accessible in the consequent despite being outside its c-command domain.

• boundIndivVar : Core.IVar

  The introduced individual variable

• boundEntity : E

  The entity it binds to

structure Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.ModalDonkey (W : Type u_1) (Time : Type u_2) : Type (max u_1 u_2)

Modal donkey anaphora structure (Mendes' contribution).

"If Maria be.SF home, she will answer."

The subjunctive introduces a situation dref that is accessible in the consequent despite being outside its c-command domain.

• boundSitVar : Situations.SVar

  The introduced situation variable

• boundSituation : Situation W Time

  The situation it binds to

• historicalBase : Set (Situation W Time)

  Historical alternatives at binding

def Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.structuralParallel : Prop

Both classic and modal donkey anaphora share:

1. Existential introduction in a subordinate position
2. Anaphoric retrieval outside c-command domain
3. Universal-like interpretation over domain

The difference:

• Classic: quantifies over individuals
• Modal: quantifies over situations (and their times)

Equations

• Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.structuralParallel = True

inductive Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.SituationBindingStrategy : Type

E-type vs unselective binding for situations.

Mendes follows the DRT/dynamic tradition where binding is "unselective": the situation variable is directly bound, not via an E-type pronoun.

This is crucial: SF doesn't introduce a description "the situation where..." but directly binds a situation variable that IND retrieves.

• unselective : SituationBindingStrategy
• eType : SituationBindingStrategy

instance Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.instDecidableEqSituationBindingStrategy : DecidableEq SituationBindingStrategy

Equations

• Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.instDecidableEqSituationBindingStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.instReprSituationBindingStrategy.repr : SituationBindingStrategy → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.instReprSituationBindingStrategy : Repr SituationBindingStrategy

Equations

• Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.instReprSituationBindingStrategy = { reprPrec := Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.instReprSituationBindingStrategy.repr }

def Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.mendesBindingStrategy : SituationBindingStrategy

Mendes uses unselective binding.

The SF directly binds a situation variable, and IND retrieves it. This is parallel to how indefinites work in DRT.

Equations

• Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.mendesBindingStrategy = Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.SituationBindingStrategy.unselective

theorem Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.unselective_universal_force {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (v : Situations.SVar) (antecedent consequent : Situation W Time → Prop) (c : Situations.SitContext W Time E) (gs : Situations.SitAssignment W Time E × Situation W Time) : gs ∈ subjIndChain history v (fun (c' : Situations.SitContext W Time E) => {gs' : Situations.SitAssignment W Time E × Situation W Time | gs' ∈ c' ∧ antecedent gs'.2}) (fun (c' : Situations.SitContext W Time E) => {gs' : Situations.SitAssignment W Time E × Situation W Time | gs' ∈ c' ∧ consequent gs'.2}) c → antecedent gs.2 → consequent gs.2

Unselective binding gives universal force.

When SUBJ introduces a situation in a conditional antecedent, the conditional quantifies universally over situations satisfying the antecedent in the historical base.

This is the modal analog of donkey universals.

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

Modal donkey anaphora enables temporal shift.

The future-oriented interpretation of SF follows from modal donkey anaphora:

1. SUBJ introduces s₁ ∈ hist(s₀) with τ(s₁) ≥ τ(s₀)
2. The consequent is evaluated at s₁'s time via IND's retrieval
3. Therefore, the consequent can refer to times after τ(s₀)

This is the foundation for Theorem temporal_shift_parasitic_on_modal (formalized in Situations.lean extension).

theorem Semantics.Dynamic.IntensionalCDRT.ModalDonkeyAnaphora.donkey_accessibility_transitive {W : Type u_1} {Time : Type u_2} (s₀ s₁ s₂ : Situation W Time) (h₁ : modallyAccessible s₀ s₁) (h₂ : modallyAccessible s₁ s₂) : modallyAccessible s₀ s₂

Donkey accessibility is transitive within a discourse.

If s₁ is accessible from s₀, and s₂ is accessible from s₁, then s₂ is accessible from s₀ (within the same world).