inductive Semantics.Dynamic.IntensionalCDRT.MendesDerivations.CDRTType : Type

Basic CDRT types following @cite{muskens-1996} and @cite{mendes-2025}.

Type	Interpretation
e	Entities
t	Truth values
s	Situations
c	Contexts (SitContext)

• e : CDRTType
• t : CDRTType
• s : CDRTType
• c : CDRTType
• arr : CDRTType → CDRTType → CDRTType

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqCDRTType.decEq (x✝ x✝¹ : CDRTType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqCDRTType.decEq Semantics.Dynamic.IntensionalCDRT.MendesDerivations.CDRTType.e (a ⇒ a_1) = isFalse ⋯
• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqCDRTType.decEq Semantics.Dynamic.IntensionalCDRT.MendesDerivations.CDRTType.t (a ⇒ a_1) = isFalse ⋯
• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqCDRTType.decEq Semantics.Dynamic.IntensionalCDRT.MendesDerivations.CDRTType.s (a ⇒ a_1) = isFalse ⋯
• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqCDRTType.decEq Semantics.Dynamic.IntensionalCDRT.MendesDerivations.CDRTType.c (a ⇒ a_1) = isFalse ⋯
• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqCDRTType.decEq (a ⇒ a_1) Semantics.Dynamic.IntensionalCDRT.MendesDerivations.CDRTType.e = isFalse ⋯
• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqCDRTType.decEq (a ⇒ a_1) Semantics.Dynamic.IntensionalCDRT.MendesDerivations.CDRTType.t = isFalse ⋯
• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqCDRTType.decEq (a ⇒ a_1) Semantics.Dynamic.IntensionalCDRT.MendesDerivations.CDRTType.s = isFalse ⋯
• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqCDRTType.decEq (a ⇒ a_1) Semantics.Dynamic.IntensionalCDRT.MendesDerivations.CDRTType.c = isFalse ⋯

instance Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqCDRTType : DecidableEq CDRTType

Equations

• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqCDRTType = Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqCDRTType.decEq

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instReprCDRTType.repr : CDRTType → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instReprCDRTType : Repr CDRTType

Equations

• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instReprCDRTType = { reprPrec := Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instReprCDRTType.repr }

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.«term_⇒_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.vpType : CDRTType

Verb phrase type: entity → situation → context → context

Equations

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

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.sentType : CDRTType

Sentence type: situation → context → context

Equations

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

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.npType : CDRTType

NP type: (entity → context → context) → context → context

Equations

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

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

(54) Maria -- proper name.

⟦Maria⟧ = λP.P(maria)

Type: ((e ⇒ c ⇒ c) ⇒ c ⇒ c)

Equations

• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.lexMaria maria P c = P maria c

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.lexAtHome {W : Type u_1} {Time : Type u_2} {E : Type u_3} (atHomeRel : E → Situation W Time → Prop) (x : E) (sitVar : Situations.SVar) (c : Situations.SitContext W Time E) : Situations.SitContext W Time E

(55) estar em casa -- "be at home".

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

Type: e ⇒ s ⇒ c ⇒ c

Equations

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

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.lexAnswer {W : Type u_1} {Time : Type u_2} {E : Type u_3} (answerRel : E → Situation W Time → Prop) (x : E) (sitVar : Situations.SVar) (c : Situations.SitContext W Time E) : Situations.SitContext W Time E

(56) atender -- "answer (the door)".

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

Type: e ⇒ s ⇒ c ⇒ c

Equations

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

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

(57) SF (Subordinate Future).

⟦SF⟧ = SUBJ ∘ FUT = λv_new λv_ref λc. SUBJ^{v_new}_{v_ref}[FUT(v_new, v_ref); c]

Type: SVar ⇒ SVar ⇒ c ⇒ c

Equations

• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.lexSF = Semantics.Dynamic.IntensionalCDRT.Situations.subordinateFuture

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

(58) ela -- "she" (pronoun bound to Maria in discourse).

⟦ela⟧ = λP.P(maria) -- In this context, bound to Maria

Type: ((e ⇒ c ⇒ c) ⇒ c ⇒ c)

Equations

• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.lexShe maria P c = P maria c

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.lexWill {W : Type u_1} {Time : Type u_2} {E : Type u_3} (VP : Situations.SVar → Situations.SitContext W Time E → Situations.SitContext W Time E) (sitVar : Situations.SVar) (c : Situations.SitContext W Time E) : Situations.SitContext W Time E

(59) vai -- future auxiliary "will".

⟦vai⟧ = λVPλsλc. VP(s)(c) -- Transparent, temporal info from SF

In this analysis, "vai" doesn't independently contribute future; the future comes from SF in the antecedent via modal anaphora.

Equations

• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.lexWill VP sitVar c = VP sitVar c

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.lexIf {W : Type u_1} {Time : Type u_2} {E : Type u_3} (antecedent consequent : Situations.SitContext W Time E → Situations.SitContext W Time E) (c : Situations.SitContext W Time E) : Situations.SitContext W Time E

(60) Conditional "se" -- "if".

⟦se⟧ = λAntλConsλsλc. ∀(g,s₀)∈c: Ant(s)(c) ⊆ Cons(s)(c)

Dynamic conditional: filters contexts.

Equations

• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.lexIf antecedent consequent c = consequent (antecedent c)

structure Semantics.Dynamic.IntensionalCDRT.MendesDerivations.PFTree (W : Type u_4) (Time : Type u_5) (E : Type u_6) : Type (max (max u_4 u_5) u_6)

Step 1: parse tree.

[S [Cond se [S_ant Maria estiver.SF em casa]] [S_cons ela vai atender]]

Antecedent: Maria + SF + em casa Consequent: ela + vai + atender

• antecedentSubject : E
• antecedentVP : E → Situation W Time → Prop
• consequentSubject : E
• consequentVP : E → Situation W Time → Prop

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.deriveAntecedent {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (maria : E) (atHomeRel : E → Situation W Time → Prop) (sfVar speechVar : Situations.SVar) (c : Situations.SitContext W Time E) : Situations.SitContext W Time E

Step 2: antecedent derivation.

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

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

Equations

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

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.deriveConsequent {W : Type u_1} {Time : Type u_2} {E : Type u_3} (maria : E) (answerRel : E → Situation W Time → Prop) (sfVar : Situations.SVar) (c : Situations.SitContext W Time E) : Situations.SitContext W Time E

Step 3: consequent derivation.

⟦ela vai atender⟧ = ⟦ela⟧(λx.⟦vai⟧(⟦atender⟧(x))) = [| answer(maria)(s₁)] -- s₁ retrieved via IND

The temporal anchor s₁ comes from the antecedent via modal anaphora.

Equations

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

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.deriveFullSentence {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (maria : E) (atHomeRel answerRel : E → Situation W Time → Prop) (sfVar speechVar : Situations.SVar) (c : Situations.SitContext W Time E) : Situations.SitContext W Time E

Step 4: full sentence derivation.

⟦Se Maria estiver em casa, ela vai atender⟧ = ⟦se⟧(⟦Maria estiver em casa⟧)(⟦ela vai atender⟧)

Result type: c ⇒ c (context transformer)

Equations

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

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.formula61 {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (maria : E) (atHomeRel : E → Situation W Time → Prop) (sfVar speechVar : Situations.SVar) : Situations.SitContext W Time E → Situations.SitContext W Time E

Formula (61): antecedent LF.

[SUBJ^{s₁}_{s₀} [FUT [Maria em casa(s₁)]]]

Logical form after composition.

Equations

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

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.formula62 {W : Type u_1} {Time : Type u_2} {E : Type u_3} (maria : E) (answerRel : E → Situation W Time → Prop) (sfVar : Situations.SVar) : Situations.SitContext W Time E → Situations.SitContext W Time E

Formula (62): consequent LF (anchored).

[IND_{s₁} [ela atender(s₁)]]

The situation s₁ is retrieved from the antecedent.

Equations

• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.formula62 maria answerRel sfVar = Semantics.Dynamic.IntensionalCDRT.MendesDerivations.deriveConsequent maria answerRel sfVar

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.formula63 {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (maria : E) (atHomeRel answerRel : E → Situation W Time → Prop) (sfVar speechVar : Situations.SVar) (c : Situations.SitContext W Time E) : Situations.SitContext W Time E

Formula (63): full conditional.

⟦(53)⟧^c = { (g, s₀) ∈ c | ∀s₁ ∈ hist(s₀): τ(s₁) > τ(s₀) → (at-home(maria)(s₁) → answer(maria)(s₁)) }

This is the truth condition: universal over futures where Maria is home.

Equations

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

theorem Semantics.Dynamic.IntensionalCDRT.MendesDerivations.derivation_in_historical_base {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (maria : E) (atHomeRel answerRel : E → Situation W Time → Prop) (sfVar speechVar : Situations.SVar) (c : Situations.SitContext W Time E) (gs : Situations.SitAssignment W Time E × Situation W Time) (h : gs ∈ deriveFullSentence history maria atHomeRel answerRel sfVar speechVar c) : ∃ (s₀ : Situation W Time), (∃ (g₀ : Situations.SitAssignment W Time E), (g₀, s₀) ∈ c) ∧ gs.1⟦sfVar⟧ₛ ∈ Tense.BranchingTime.historicalBase history s₀

Derivation introduces situation in historical base.

The situation s₁ introduced by SF is in the historical alternatives.

theorem Semantics.Dynamic.IntensionalCDRT.MendesDerivations.derivation_future_ordering {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (maria : E) (atHomeRel answerRel : E → Situation W Time → Prop) (sfVar speechVar : Situations.SVar) (c : Situations.SitContext W Time E) (gs : Situations.SitAssignment W Time E × Situation W Time) (h : gs ∈ deriveFullSentence history maria atHomeRel answerRel sfVar speechVar c) : gs.1⟦sfVar⟧ₛ.time > gs.1⟦speechVar⟧ₛ.time

Derivation enforces future ordering.

The situation s₁ has time strictly after the speech situation.

theorem Semantics.Dynamic.IntensionalCDRT.MendesDerivations.derivation_conditional_holds {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [LT Time] (history : Tense.BranchingTime.WorldHistory W Time) (maria : E) (atHomeRel answerRel : E → Situation W Time → Prop) (sfVar speechVar : Situations.SVar) (c : Situations.SitContext W Time E) (gs : Situations.SitAssignment W Time E × Situation W Time) (h : gs ∈ deriveFullSentence history maria atHomeRel answerRel sfVar speechVar c) : atHomeRel maria (gs.1⟦sfVar⟧ₛ) → answerRel maria (gs.1⟦sfVar⟧ₛ)

Derivation enforces conditional semantics.

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

inductive Semantics.Dynamic.IntensionalCDRT.MendesDerivations.Construction : Type

Table 3 from @cite{mendes-2025}: temporal reference patterns.

Construction	Matrix Mood	Embedded Mood	Time Reference
Conditional	IND	SF	Future
Relative clause	IND	SF	Future
Complement	IND	SUBJ	Variable
Temporal clause	IND	SF	Future

• conditional : Construction
• relativeClause : Construction
• complement : Construction
• temporalClause : Construction

instance Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instDecidableEqConstruction : DecidableEq Construction

Equations

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

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instReprConstruction.repr : Construction → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instReprConstruction : Repr Construction

Equations

• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instReprConstruction = { reprPrec := Semantics.Dynamic.IntensionalCDRT.MendesDerivations.instReprConstruction.repr }

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.sfEnablesFutureReference (constr : Construction) : Prop

All SF constructions enable future reference via modal donkey anaphora.

Equations

• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.sfEnablesFutureReference Semantics.Dynamic.IntensionalCDRT.MendesDerivations.Construction.conditional = True
• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.sfEnablesFutureReference Semantics.Dynamic.IntensionalCDRT.MendesDerivations.Construction.relativeClause = True
• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.sfEnablesFutureReference Semantics.Dynamic.IntensionalCDRT.MendesDerivations.Construction.complement = True
• Semantics.Dynamic.IntensionalCDRT.MendesDerivations.sfEnablesFutureReference Semantics.Dynamic.IntensionalCDRT.MendesDerivations.Construction.temporalClause = True

def Semantics.Dynamic.IntensionalCDRT.MendesDerivations.deriveCounterfactual {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (maria : E) (atHomeRel answerRel : E → Situation W Time → Prop) (cfVar speechVar : Situations.SVar) (c : Situations.SitContext W Time E) : Situations.SitContext W Time E

Counterfactual conditional (for comparison).

"Se Maria estivesse em casa, ela atenderia." "If Maria were at home, she would answer."

Uses SUBJ but without FUT, and with imperfect morphology. The counterfactual uses past situations in the historical base.

Equations

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

theorem Semantics.Dynamic.IntensionalCDRT.MendesDerivations.sf_vs_counterfactual_temporal {W : Type u_4} {Time : Type u_5} {E : Type u_6} [Preorder Time] (history : Tense.BranchingTime.WorldHistory W Time) (maria : E) (atHomeRel answerRel : E → Situation W Time → Prop) (sitVar speechVar : Situations.SVar) (c : Situations.SitContext W Time E) : (∀ gs ∈ deriveFullSentence history maria atHomeRel answerRel sitVar speechVar c, gs.1⟦sitVar⟧ₛ.time > gs.1⟦speechVar⟧ₛ.time) ∧ True

SF vs counterfactual differ in temporal constraint.

SF constrains to future; counterfactual allows past/present.