Mendes (2025): The Subordinate Future

@cite{mendes-2025}

The Subordinate Future (SF) in Portuguese is a mood form (subjunctive with future morphology) that:

1. Enables modal donkey anaphora — subjunctive binds situation variables across clause boundaries (§3.1)
2. Weakens existential presuppositions of strong quantifiers in restrictors (§2.2)
3. Has a future-oriented temporal interpretation that is parasitic on the modal anaphora — not stipulated by an independent temporal operator (§3.2, following @cite{crouch-1993} @cite{crouch-1994})

Organization

• §1 The SF operator (§3.2): subordinateFuture := dynSUBJ ∘ dynFUT, plus its conditional and relative-clause specializations.
• §2 Temporal properties (§3.2): theorems showing the future shift is derived from the modal component, not stipulated.
• §3 Compositional CDRT derivations (§4.3.1): lexical entries and end-to-end derivation of "Se Maria estiver em casa, ela vai atender".
• §4 Presupposition weakening (§2.2): SF in restrictors of strong quantifiers, formalized as modal displacement.

The dynamic primitives are imported from co-located dynamic operator files: dynSUBJ/dynIND from Theories/Semantics/Mood/Dynamic.lean (siblings of static Mood.SUBJ/IND), dynFUT from Theories/Semantics/Tense/Dynamic.lean, and SitContext/SVar from Theories/Semantics/Dynamic/Core/{ContextFilter,DiscourseRef}.lean.

def Mendes2025.subordinateFuture {W : Type u_1} {Time : Type u_2} [LE Time] [LT Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (newSitVar refSitVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

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 (@cite{mendes-2025} §3.2):

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

• Mendes2025.subordinateFuture history newSitVar refSitVar c = Semantics.Tense.dynFUT newSitVar refSitVar (Semantics.Mood.dynSUBJ history newSitVar c)

def Mendes2025.conditionalWithSF {W : Type u_1} {Time : Type u_2} [LE Time] [LT Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (antecedentVar speechVar : Semantics.Dynamic.Core.SVar) (antecedent consequent : Semantics.Dynamic.Core.SitContext W Time → Semantics.Dynamic.Core.SitContext W Time) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

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

• Mendes2025.conditionalWithSF history antecedentVar speechVar antecedent consequent c = consequent (antecedent (Mendes2025.subordinateFuture history antecedentVar speechVar c))

def Mendes2025.relativeClauseSF {W : Type u_1} {Time : Type u_2} [LE Time] [LT Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (rcVar speechVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

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

• Mendes2025.relativeClauseSF history rcVar speechVar c = Mendes2025.subordinateFuture history rcVar speechVar c

def Mendes2025.everyWithSFRestrictor {W : Type u_1} {Time : Type u_2} [LE Time] [LT Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (rcVar speechVar : Semantics.Dynamic.Core.SVar) (restrictor nuclear : Semantics.Dynamic.Core.SitContext W Time → Semantics.Dynamic.Core.SitContext W Time) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

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

• Mendes2025.everyWithSFRestrictor history rcVar speechVar restrictor nuclear c = nuclear (restrictor (Mendes2025.subordinateFuture history rcVar speechVar c))

theorem Mendes2025.sf_introduces_future {W : Type u_1} {Time : Type u_2} [Preorder Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (newVar refVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) (gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex 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 Mendes2025.temporal_shift_parasitic_on_modal {W : Type u_1} {Time : Type u_2} [Preorder Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (sfVar speechVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) (gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time) (h : gs ∈ subordinateFuture history sfVar speechVar c) : ∃ (g₀ : Core.Assignment (Core.WorldTimeIndex W Time)) (s₀ : Core.WorldTimeIndex W Time), (g₀, s₀) ∈ c ∧ gs.1 sfVar ∈ Core.Modality.HistoricalAlternatives.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 Mendes2025.sf_restrictor_future_reference {W : Type u_1} {Time : Type u_2} [Preorder Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (rcVar speechVar : Semantics.Dynamic.Core.SVar) (restrictor nuclear : Semantics.Dynamic.Core.SitContext W Time → Semantics.Dynamic.Core.SitContext W Time) (c : Semantics.Dynamic.Core.SitContext W Time) (gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time) (h : gs ∈ everyWithSFRestrictor history rcVar speechVar restrictor nuclear c) (hR : Semantics.Dynamic.Core.IsContextFilter restrictor) (hN : Semantics.Dynamic.Core.IsContextFilter nuclear) : (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.

Restrictor and nuclear must be context filters (IsContextFilter). Linguistically, predicates filter contexts without modifying assignments.

def Mendes2025.lexMaria {W : Type u_1} {Time : Type u_2} {E : Type u_3} (maria : E) (P : E → Semantics.Dynamic.Core.SitContext W Time → Semantics.Dynamic.Core.SitContext W Time) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

Maria — proper name. ⟦Maria⟧ = λP.P(maria)

Equations

• Mendes2025.lexMaria maria P c = P maria c

def Mendes2025.lexAtHome {W : Type u_1} {Time : Type u_2} {E : Type u_3} (atHomeRel : E → Core.WorldTimeIndex W Time → Prop) (x : E) (sitVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

estar em casa — "be at home". ⟦estar em casa⟧ = λxλsλc. [| at-home(x)(s)]; c

Equations

• Mendes2025.lexAtHome atHomeRel x sitVar c = {gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time | gs ∈ c ∧ atHomeRel x (gs.1 sitVar)}

def Mendes2025.lexAnswer {W : Type u_1} {Time : Type u_2} {E : Type u_3} (answerRel : E → Core.WorldTimeIndex W Time → Prop) (x : E) (sitVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

atender — "answer (the door)". ⟦atender⟧ = λxλsλc. [| answer(x)(s)]; c

Equations

• Mendes2025.lexAnswer answerRel x sitVar c = {gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time | gs ∈ c ∧ answerRel x (gs.1 sitVar)}

def Mendes2025.lexSF {W : Type u_1} {Time : Type u_2} [LE Time] [LT Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (newSitVar refSitVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

SF (Subordinate Future). ⟦SF⟧ = SUBJ ∘ FUT

Equations

• Mendes2025.lexSF = Mendes2025.subordinateFuture

def Mendes2025.lexShe {W : Type u_1} {Time : Type u_2} {E : Type u_3} (maria : E) (P : E → Semantics.Dynamic.Core.SitContext W Time → Semantics.Dynamic.Core.SitContext W Time) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

ela — "she" (pronoun bound to Maria). ⟦ela⟧ = λP.P(maria)

Equations

• Mendes2025.lexShe maria P c = P maria c

def Mendes2025.lexWill {W : Type u_1} {Time : Type u_2} (VP : Semantics.Dynamic.Core.SVar → Semantics.Dynamic.Core.SitContext W Time → Semantics.Dynamic.Core.SitContext W Time) (sitVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

vai — future auxiliary "will". ⟦vai⟧ = λVPλsλc. VP(s)(c) — transparent; future comes from SF via modal anaphora.

Equations

• Mendes2025.lexWill VP sitVar c = VP sitVar c

def Mendes2025.seqUpdate {W : Type u_1} {Time : Type u_2} (antecedent consequent : Semantics.Dynamic.Core.SitContext W Time → Semantics.Dynamic.Core.SitContext W Time) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

Sequential context update: feeds antecedent output into consequent.

Note: the paper's ⟦if⟧ is dynamic implication (a test: [| P ⇒ Q]), but the derivation theorems here require extracting properties from the output context, which a test semantics cannot provide (tests preserve input unchanged). Sequential composition is appropriate because the universal force comes from SUBJ's quantification over historical alternatives, not from the conditional operator itself.

Equations

• Mendes2025.seqUpdate antecedent consequent c = consequent (antecedent c)

def Mendes2025.deriveAntecedent {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (maria : E) (atHomeRel : E → Core.WorldTimeIndex W Time → Prop) (sfVar speechVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

Antecedent derivation: ⟦Maria estiver em casa⟧ = SUBJ^{s₁}_{s₀}[FUT; [| at-home(maria)(s₁)]]

Introduces s₁ ∈ hist(s₀), constrains τ(s₁) > τ(s₀), asserts Maria at home.

Equations

• Mendes2025.deriveAntecedent history maria atHomeRel sfVar speechVar c = Mendes2025.lexAtHome atHomeRel maria sfVar (Mendes2025.lexSF history sfVar speechVar c)

def Mendes2025.deriveConsequent {W : Type u_1} {Time : Type u_2} {E : Type u_3} (maria : E) (answerRel : E → Core.WorldTimeIndex W Time → Prop) (sfVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

Consequent derivation: ⟦ela vai atender⟧ = [| answer(maria)(s₁)] — s₁ retrieved via IND.

Equations

• Mendes2025.deriveConsequent maria answerRel sfVar c = Mendes2025.lexAnswer answerRel maria sfVar (Semantics.Mood.dynIND sfVar c)

def Mendes2025.deriveFullSentence {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (maria : E) (atHomeRel answerRel : E → Core.WorldTimeIndex W Time → Prop) (sfVar speechVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

Full sentence derivation: ⟦Se Maria estiver em casa, ela vai atender⟧

Equations

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

theorem Mendes2025.derivation_in_historical_base {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (maria : E) (atHomeRel answerRel : E → Core.WorldTimeIndex W Time → Prop) (sfVar speechVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) (gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time) (h : gs ∈ deriveFullSentence history maria atHomeRel answerRel sfVar speechVar c) : ∃ (s₀ : Core.WorldTimeIndex W Time), (∃ (g₀ : Core.Assignment (Core.WorldTimeIndex W Time)), (g₀, s₀) ∈ c) ∧ gs.1 sfVar ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀

The situation introduced by SF is in the historical alternatives.

theorem Mendes2025.derivation_future_ordering {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (maria : E) (atHomeRel answerRel : E → Core.WorldTimeIndex W Time → Prop) (sfVar speechVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) (gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time) (h : gs ∈ deriveFullSentence history maria atHomeRel answerRel sfVar speechVar c) : (gs.1 sfVar).time > (gs.1 speechVar).time

The derivation enforces future ordering: τ(s₁) > τ(s₀).

theorem Mendes2025.derivation_conditional_holds {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (maria : E) (atHomeRel answerRel : E → Core.WorldTimeIndex W Time → Prop) (sfVar speechVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) (gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time) (h : gs ∈ deriveFullSentence history maria atHomeRel answerRel sfVar speechVar c) : atHomeRel maria (gs.1 sfVar) → answerRel maria (gs.1 sfVar)

If Maria is at home at s₁, she answers at s₁.

def Mendes2025.deriveCounterfactual {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (maria : E) (atHomeRel answerRel : E → Core.WorldTimeIndex W Time → Prop) (cfVar speechVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

Counterfactual conditional (for comparison). "Se Maria estivesse em casa, ela atenderia." Uses SUBJ without FUT — allows past/present alternatives.

Equations

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

theorem Mendes2025.sf_vs_counterfactual_temporal {W : Type u_4} {Time : Type u_5} [Preorder Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) {E : Type u_6} (maria : E) (atHomeRel answerRel : E → Core.WorldTimeIndex W Time → Prop) (sitVar speechVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) (gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time) : gs ∈ deriveFullSentence history maria atHomeRel answerRel sitVar speechVar c → (gs.1 sitVar).time > (gs.1 speechVar).time

SF constrains to future; counterfactual allows past/present.

Key data (Portuguese)

With indicative, strong quantifiers presuppose existence: (17) #Cada/todo livro que a Maria ler será interessante. "Every book that Maria reads.IND will be interesting" → Presupposes Maria will read books (fails if uncertain)

With SF, the presupposition is weakened: (18) Cada/todo livro que a Maria ler será interessante. "Every book that Maria reads.SF will be interesting" → No existence presupposition (felicitous even if uncertain)

def Mendes2025.existentialPresup {W : Type u_4} {E : Type u_5} (restrictor : E → W → Prop) : W → Prop

Existential presupposition: the restrictor is non-empty.

Equations

• Mendes2025.existentialPresup restrictor w = ∃ (x : E), restrictor x w

def Mendes2025.indicativeRestrictor {W : Type u_4} {Time : Type u_5} {E : Type u_6} (restrictor : E → Core.WorldTimeIndex W Time → Prop) (s : Core.WorldTimeIndex W Time) : E → Prop

Indicative restrictor: evaluates at the actual world. "Every book that Maria reads.IND..." → presupposes books exist that Maria reads.

Equations

• Mendes2025.indicativeRestrictor restrictor s x = restrictor x s

def Mendes2025.sfRestrictor {W : Type u_4} {Time : Type u_5} {E : Type u_6} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (restrictor : E → Core.WorldTimeIndex W Time → Prop) (s₀ : Core.WorldTimeIndex W Time) : E → Prop

SF restrictor: quantifies over historical alternatives. "Every book that Maria reads.SF..." → no categorical existence presupposition.

Equations

• Mendes2025.sfRestrictor history restrictor s₀ x = ∃ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, restrictor x s₁

theorem Mendes2025.indicative_preserves_presup {W : Type u_4} {Time : Type u_5} {E : Type u_6} (restrictor : E → Core.WorldTimeIndex W Time → Prop) (s : Core.WorldTimeIndex W Time) (h_presup : ∃ (x : E), indicativeRestrictor restrictor s x) : ∃ (x : E), restrictor x s

Indicative preserves existential presupposition.

theorem Mendes2025.sf_weakens_presup {W : Type u_4} {Time : Type u_5} {E : Type u_6} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (restrictor : E → Core.WorldTimeIndex W Time → Prop) (s₀ : Core.WorldTimeIndex W Time) (h_no_actual : ¬∃ (x : E), restrictor x s₀) (h_possible : ∃ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, ∃ (x : E), restrictor x s₁) : ∃ (x : E), sfRestrictor history restrictor s₀ x

SF weakens existential presupposition: even without actual existence at s₀, the SF restrictor can be satisfied in alternative situations.

theorem Mendes2025.sf_felicitous_under_uncertainty {W : Type u_4} {Time : Type u_5} {E : Type u_6} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (restrictor : E → Core.WorldTimeIndex W Time → Prop) (s₀ : Core.WorldTimeIndex W Time) (h_uncertainty : (∃ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, ∃ (x : E), restrictor x s₁) ∧ ∃ s₂ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, ¬∃ (x : E), restrictor x s₂) : (∃ (x : E), sfRestrictor history restrictor s₀ x) ∧ ∃ s ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, ¬∃ (x : E), restrictor x s

SF makes strong quantifiers felicitous under uncertainty.

def Mendes2025.relClauseSF {W : Type u_4} {Time : Type u_5} {E : Type u_6} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (noun relClause : E → Core.WorldTimeIndex W Time → Prop) (s₀ : Core.WorldTimeIndex W Time) : E → Prop

Relative clause with SF weakens strong quantifier presupposition. This is the formal version of the indicative-vs-SF contrast in restrictors.

Equations

• Mendes2025.relClauseSF history noun relClause s₀ x = ∃ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, noun x s₁ ∧ relClause x s₁

theorem Mendes2025.relClause_sf_weakens_quantifier {W : Type u_4} {Time : Type u_5} {E : Type u_6} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (noun relClause : E → Core.WorldTimeIndex W Time → Prop) (s₀ : Core.WorldTimeIndex W Time) (h_none_actual : ¬∃ (x : E), noun x s₀ ∧ relClause x s₀) (h_some_possible : ∃ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, ∃ (x : E), noun x s₁ ∧ relClause x s₁) : ∃ (x : E), relClauseSF history noun relClause s₀ x

def Mendes2025.modalDisplacement {W : Type u_4} {Time : Type u_5} {E : Type u_6} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (restrictor nuclear : E → Core.WorldTimeIndex W Time → Prop) (s₀ : Core.WorldTimeIndex W Time) : Prop

Modal displacement: SF introduces quantification over situations, "displacing" the existential presupposition to be local within each situation.

Equations

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

theorem Mendes2025.sf_is_modal_displacement {W : Type u_4} {Time : Type u_5} {E : Type u_6} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (restrictor nuclear : E → Core.WorldTimeIndex W Time → Prop) (s₀ : Core.WorldTimeIndex W Time) : modalDisplacement history restrictor nuclear s₀ ↔ ∀ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, ∀ (x : E), restrictor x s₁ → nuclear x s₁

SF semantics is equivalent to modal displacement.

theorem Mendes2025.modal_displacement_weaker_than_accommodation {W : Type u_4} {Time : Type u_5} {E : Type u_6} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (restrictor : E → Core.WorldTimeIndex W Time → Prop) (s₀ : Core.WorldTimeIndex W Time) (h_global : ∀ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, ∃ (x : E), restrictor x s₁) (h_nonempty : ∃ (s : Core.WorldTimeIndex W Time), s ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀) : ∃ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, ∃ (x : E), restrictor x s₁

Modal displacement is weaker than global accommodation.

The central theoretical insight of @cite{mendes-2025} §3.1: SF enables modal donkey anaphora — subjunctive binds situation variables across clause boundaries, just like indefinites bind individual variables in classic donkey sentences.

Classic donkey anaphora: "If a farmer owns a donkey, he beats it."

• "a donkey" introduces individual dref x
• "it" retrieves x outside the syntactic scope of "a"

Modal donkey anaphora: "Se Maria estiver em casa, ela vai atender."

• SF introduces situation dref s₁
• Main clause retrieves s₁ for temporal anchoring

Correspondence with the dynamic primitives in Theories/Semantics/Mood/Dynamic.lean:

• SUBJ introduces: dynSUBJ history v = dynIntroduce (historicalBase history) v
• IND retrieves: dynIND v = dynRelationOn (·.2) (·.1 v) sameWorld

def Mendes2025.crossClausalBinding {W : Type u_4} {Time : Type u_5} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (antecedentVar _consequentVar : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

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

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

Equations

• Mendes2025.crossClausalBinding history antecedentVar _consequentVar c = Semantics.Mood.dynIND antecedentVar (Semantics.Mood.dynSUBJ history antecedentVar c)

theorem Mendes2025.cross_clausal_same_world {W : Type u_4} {Time : Type u_5} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (v : Semantics.Dynamic.Core.SVar) (c : Semantics.Dynamic.Core.SitContext W Time) (gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time) (h : gs ∈ crossClausalBinding 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 Mendes2025.subjIndChain {W : Type u_4} {Time : Type u_5} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (v : Semantics.Dynamic.Core.SVar) (antecedentPred consequentPred : Semantics.Dynamic.Core.SitContext W Time → Semantics.Dynamic.Core.SitContext W Time) (c : Semantics.Dynamic.Core.SitContext W Time) : Semantics.Dynamic.Core.SitContext W Time

The SUBJ-IND anaphoric chain: SUBJ introduces s₁, the antecedent predicate filters at s₁, IND retrieves s₁ (same-world check), and the consequent inherits the temporal anchor from s₁.

Equations

• Mendes2025.subjIndChain history v antecedentPred consequentPred c = consequentPred (Semantics.Mood.dynIND v (antecedentPred (Semantics.Mood.dynSUBJ history v c)))

theorem Mendes2025.subj_ind_chain_modal_donkey {W : Type u_4} {Time : Type u_5} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (v : Semantics.Dynamic.Core.SVar) (P Q : Semantics.Dynamic.Core.SitContext W Time → Semantics.Dynamic.Core.SitContext W Time) (c : Semantics.Dynamic.Core.SitContext W Time) (gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time) (h : gs ∈ subjIndChain history v P Q c) (hQ : Semantics.Dynamic.Core.IsContextFilter Q) : 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 bound situation's world.

Q must be a context filter — predicates filter contexts without modifying assignments.

theorem Mendes2025.unselective_universal_force {W : Type u_4} {Time : Type u_5} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (v : Semantics.Dynamic.Core.SVar) (antecedent consequent : Core.WorldTimeIndex W Time → Prop) (c : Semantics.Dynamic.Core.SitContext W Time) (gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time) : gs ∈ subjIndChain history v (fun (c' : Semantics.Dynamic.Core.SitContext W Time) => {gs' : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time | gs' ∈ c' ∧ antecedent gs'.2}) (fun (c' : Semantics.Dynamic.Core.SitContext W Time) => {gs' : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex 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 — the modal analog of donkey universals.

Pipeline characterization

The full pipeline SUBJ → filter(P) → IND → filter(Q) on a singleton context is equivalent to a static existential conjunction over historical alternatives. The dynamic pipeline gives conjunction (P ∧ Q), not implication (P → Q); sequential composition gives the stronger conjunctive reading, while the static conditionalSF uses implication.

theorem Mendes2025.subjIndChain_singleton {W : Type u_4} {Time : Type u_5} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (v : Semantics.Dynamic.Core.SVar) (g : Core.Assignment (Core.WorldTimeIndex W Time)) (s₀ : Core.WorldTimeIndex W Time) (P Q : Core.WorldTimeIndex W Time → Prop) : (∃ (gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time), gs ∈ subjIndChain history v (fun (c : Semantics.Dynamic.Core.SitContext W Time) => {gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time | gs ∈ c ∧ P gs.2}) (fun (c : Semantics.Dynamic.Core.SitContext W Time) => {gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time | gs ∈ c ∧ Q gs.2}) {(g, s₀)}) ↔ ∃ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, P s₁ ∧ Q s₁

The SUBJ-IND chain with predication filters on a singleton context characterizes the static existential conjunction ∃ s₁ ∈ historicalBase(s₀), P(s₁) ∧ Q(s₁).

theorem Mendes2025.subjIndChain_entails_conditionalSF {W : Type u_4} {Time : Type u_5} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (v : Semantics.Dynamic.Core.SVar) (g : Core.Assignment (Core.WorldTimeIndex W Time)) (s₀ : Core.WorldTimeIndex W Time) (P : Core.WorldTimeIndex W Time → Prop) (Q : Core.WorldTimeIndex W Time → Core.WorldTimeIndex W Time → Prop) (h : ∃ (gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time), gs ∈ subjIndChain history v (fun (c : Semantics.Dynamic.Core.SitContext W Time) => {gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time | gs ∈ c ∧ P gs.2}) (fun (c : Semantics.Dynamic.Core.SitContext W Time) => {gs : Core.Assignment (Core.WorldTimeIndex W Time) × Core.WorldTimeIndex W Time | gs ∈ c ∧ Q gs.2 gs.2}) {(g, s₀)}) : Semantics.Mood.conditionalSF history P (fun (s₁ x : Core.WorldTimeIndex W Time) => Q s₁ s₁) s₀

The dynamic pipeline entails the static conditional (conditionalSF). Conjunction is stronger than implication: if the dynamic pipeline finds an s₁ satisfying both P and Q, then P(s₁) → Q(s₁) holds trivially.

Bridge to Hofmann (2025) accessibility

The same-world constraint enforced by dynIND (via the sameWorld kernel in Mood/Basic.lean) parallels @cite{hofmann-2025}'s veridicality-based accessibility for individual drefs:

• Situation level (this file, @cite{mendes-2025}): dynIND retrieves s₁ via s₂.world = s₁.world. Governs cross-clausal situation binding (modal donkey anaphora).
• Propositional dref level (Phenomena/Anaphora/Studies/Hofmann2025.lean, @cite{hofmann-2025}): a dref is accessible iff it has a referent in all worlds of the local context, plus a discourse-consistency condition. Governs individual dref accessibility across negation, disjunction, and attitude contexts.

Both enforce the structural pattern that the retrieval context must be compatible with the introduction context. For situations, this is world identity; for individual drefs, this is the subset-plus- existence condition (Hofmann 2025 Definition 39).