Mendes (2025): Indefiniteness in future reference

Mendes analyses the Subordinate Future, a subjunctive combined with a forward-shifting temporal morpheme, in Muskens's compositional discourse representation theory over situations. The subjunctive is an indefinite that introduces a situation among the historical alternatives of its anchor, and the indicative is the definite that retrieves it. A main clause is therefore evaluated in the future situation its subordinate clause introduced (modal donkey anaphora), and a strong quantifier whose restrictor carries the form has its existence presupposition satisfied in a historical alternative rather than at the anchor (modal displacement).

Main results

• sfForm_true_at: the truth conditions of the paper's conditional and relative-clause derivations.
• temporal_shift, modal_donkey_anaphora: the orderings of the paper's table of main-clause tenses, and the retrieval of the introduced situation.
• subj_fut_true_at, ind_fut_true_at: a restrictor in the Subordinate Future is true in some later historical alternative of the anchor, one in the indicative only in the anchor's world.

Implementation notes

• States assign situations to registers only: individual drefs are saturated in the radicals (Ivan leaves the room is a situation predicate), so the quantifying-in of the relative clause reduces to the implication of its restrictor and nuclear scope.
• A situation is a world–time Index, and s₂ is part of the world of s₁ is world identity.

References

• [Men25]
• [Mus96]

Types

@[reducible, inline]

abbrev Mendes2025.State (W : Type u_3) (T : Type u_4) : Type (max u_4 u_3)

A state assigns situations to drefs.

Equations

• Mendes2025.State W T = Assignment (Reference.Index W T)

@[reducible, inline]

abbrev Mendes2025.Sit (W : Type u_3) (T : Type u_4) : Type (max u_4 u_3)

A situation dref, the type s.

Equations

• Mendes2025.Sit W T = (Mendes2025.State W T → Reference.Index W T)

@[reducible, inline]

abbrev Mendes2025.Radical (W : Type u_3) (T : Type u_4) : Type (max (max u_4 u_3) u_4 u_3)

A sentence radical, of type st, takes a situation dref to an update.

Equations

• Mendes2025.Radical W T = (Mendes2025.Sit W T → DynamicSemantics.Update (Mendes2025.State W T))

@[reducible, inline]

abbrev Mendes2025.Tensed (W : Type u_3) (T : Type u_4) : Type (max (max u_4 u_3) u_4 u_3)

A tensed radical, the type (s, st), the argument of a mood morpheme.

Equations

• Mendes2025.Tensed W T = (Mendes2025.Sit W T → Mendes2025.Sit W T → DynamicSemantics.Update (Mendes2025.State W T))

def Mendes2025.radical {W : Type u_1} {T : Type u_2} (P : Reference.Index W T → Prop) : Radical W T

The radical of a situation predicate, λs.[ | P(s)].

Equations

• Mendes2025.radical P s = DynamicSemantics.Update.test {i : Mendes2025.State W T | P (s i)}

Lexical entries

def Mendes2025.ind {W : Type u_1} {T : Type u_2} (s₂ s₁ : Sit W T) (ℙ : Tensed W T) : DynamicSemantics.Update (State W T)

The indicative ind^{s₂,s₁} ⇝ λℙ.[ | s₂ ≤ w_{s₁}]; ℙ(s₂)(s₁) is a definite over situations, testing that s₂ is part of the world of s₁.

Equations

• Mendes2025.ind s₂ s₁ ℙ = SetRel.comp (DynamicSemantics.Update.test {i : Mendes2025.State W T | (s₂ i).world = (s₁ i).world}) (ℙ s₂ s₁)

theorem Mendes2025.ind_apply {W : Type u_1} {T : Type u_2} {ℙ : Tensed W T} {s s' : Sit W T} {i o : State W T} : (i, o) ∈ ind s s' ℙ ↔ (s i).world = (s' i).world ∧ (i, o) ∈ ℙ s s'

def Mendes2025.temporal {W : Type u_1} {T : Type u_2} [LinearOrder T] (cell : Finset Ordering) (P : Radical W T) (s s' : Sit W T) : DynamicSemantics.Update (State W T)

A temporal morpheme λ𝒫.λs.λs'.[ | τ(s) ⋈ τ(s')]; 𝒫(s) tests that the running times of s and s' compare within the cell, then runs the radical at s.

Equations

• Mendes2025.temporal cell P s s' = SetRel.comp (DynamicSemantics.Update.test {i : Mendes2025.State W T | compare (s i).time (s' i).time ∈ cell}) (P s)

@[reducible, inline]

abbrev Mendes2025.fut {W : Type u_1} {T : Type u_2} [LinearOrder T] : Radical W T → Sit W T → Sit W T → DynamicSemantics.Update (State W T)

fut places the event situation after the evaluation situation.

Equations

• Mendes2025.fut = Mendes2025.temporal (Semantics.Denotes.denote Tense.future)

@[reducible, inline]

abbrev Mendes2025.pres {W : Type u_1} {T : Type u_2} [LinearOrder T] : Radical W T → Sit W T → Sit W T → DynamicSemantics.Update (State W T)

pres places the event situation at the evaluation situation.

Equations

• Mendes2025.pres = Mendes2025.temporal (Semantics.Denotes.denote Tense.present)

@[reducible, inline]

abbrev Mendes2025.past {W : Type u_1} {T : Type u_2} [LinearOrder T] : Radical W T → Sit W T → Sit W T → DynamicSemantics.Update (State W T)

past places the event situation before the evaluation situation.

Equations

• Mendes2025.past = Mendes2025.temporal (Semantics.Denotes.denote Tense.past)

def Mendes2025.subj {W : Type u_1} {T : Type u_2} [LinearOrder T] (history : HistoricalAlternatives W T) (s₁ : ℕ) (s₀ : Sit W T) (ℙ : Tensed W T) : DynamicSemantics.Update (State W T)

The subjunctive subj^{s₁}_{s₀} ⇝ λℙ.[s₁ | s₁ ∈ hist s₀]; ℙ(s₁)(s₀) is an indefinite over situations, introducing s₁ among the historical alternatives of the anchor s₀.

Equations

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

Unpacking the entries

theorem Mendes2025.temporal_radical_apply {W : Type u_1} {T : Type u_2} {s s' : Sit W T} {i o : State W T} [LinearOrder T] {cell : Finset Ordering} {P : Reference.Index W T → Prop} : (i, o) ∈ temporal cell (radical P) s s' ↔ i = o ∧ compare (s o).time (s' o).time ∈ cell ∧ P (s o)

theorem Mendes2025.isTest_temporal_radical {W : Type u_1} {T : Type u_2} {s s' : Sit W T} [LinearOrder T] {cell : Finset Ordering} {P : Reference.Index W T → Prop} : (temporal cell (radical P) s s').IsTest

A temporal morpheme over a radical is a test, which neither introduces nor retrieves drefs.

theorem Mendes2025.subj_apply {W : Type u_1} {T : Type u_2} {ℙ : Tensed W T} {s : Sit W T} {i o : State W T} [LinearOrder T] (history : HistoricalAlternatives W T) {s₁ : ℕ} : (i, o) ∈ subj history s₁ s ℙ ↔ ∃ e ∈ history.historicalBase (s (Function.update i s₁ e)), (Function.update i s₁ e, o) ∈ ℙ (DynamicSemantics.RegisterStructure.val s₁) s

The Subordinate Future

The forms SF(A); tense(C) of the paper's table of main-clause tenses: a conditional antecedent or a relative clause carrying the Subordinate Future, subj^{s₁}_{s₀}(fut(A)), and a main clause ind^{s₂,s₁}(tense(C)) whose evaluation situation is the introduced s₁. The anchor s₀ is the dref 0, the introduced situation the dref 1, the main-clause situation the dref 2.

def Mendes2025.sfForm {W : Type u_1} {T : Type u_2} [LinearOrder T] (history : HistoricalAlternatives W T) (A C : Reference.Index W T → Prop) (cell : Finset Ordering) : DynamicSemantics.Update (State W T)

A subordinate clause carrying the Subordinate Future and a main clause with the tense cell form a dynamic implication, as in the conditional and the relative-clause quantification of the paper's derivations.

Equations

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

@[reducible, inline]

abbrev Mendes2025.conditional {W : Type u_1} {T : Type u_2} [LinearOrder T] (history : HistoricalAlternatives W T) (leaves wentWell : Reference.Index W T → Prop) : DynamicSemantics.Update (State W T)

If Ivan leaves the room smiling, the interview went well has the Subordinate Future in the antecedent and the past in the consequent.

Equations

• Mendes2025.conditional history leaves wentWell = Mendes2025.sfForm history leaves wentWell (Semantics.Denotes.denote Tense.past)

@[reducible, inline]

abbrev Mendes2025.relativeClause {W : Type u_1} {T : Type u_2} [LinearOrder T] (history : HistoricalAlternatives W T) (delivers chance : Reference.Index W T → Prop) : DynamicSemantics.Update (State W T)

Every candidate who delivers a good job talk has an equal chance of being hired has the Subordinate Future in the restrictor and the present in the nuclear scope.

Equations

• Mendes2025.relativeClause history delivers chance = Mendes2025.sfForm history delivers chance (Semantics.Denotes.denote Tense.present)

theorem Mendes2025.sfForm_true_at {W : Type u_1} {T : Type u_2} {i : State W T} [LinearOrder T] (history : HistoricalAlternatives W T) {cell : Finset Ordering} (A C : Reference.Index W T → Prop) : i ∈ SetRel.dom (sfForm history A C cell) ↔ ∀ e ∈ history.historicalBase (i 0), (i 0).time < e.time → A e → (i 2).world = e.world ∧ compare (i 2).time e.time ∈ cell ∧ C (i 2)

The form of the paper's derivations is a test, true at a state iff every historical alternative e of the anchor after it where A holds has the main-clause situation in its world, timed by the cell relative to e, satisfying C.

theorem Mendes2025.conditional_true_at {W : Type u_1} {T : Type u_2} {i : State W T} [LinearOrder T] (history : HistoricalAlternatives W T) (leaves wentWell : Reference.Index W T → Prop) : i ∈ SetRel.dom (conditional history leaves wentWell) ↔ ∀ e ∈ history.historicalBase (i 0), (i 0).time < e.time → leaves e → (i 2).world = e.world ∧ (i 2).time < e.time ∧ wentWell (i 2)

If Ivan leaves the room smiling, the interview went well is true iff in every later historical alternative of the anchor where Ivan leaves, the interview situation lies in its world, earlier, and went well.

theorem Mendes2025.relativeClause_true_at {W : Type u_1} {T : Type u_2} {i : State W T} [LinearOrder T] (history : HistoricalAlternatives W T) (delivers chance : Reference.Index W T → Prop) : i ∈ SetRel.dom (relativeClause history delivers chance) ↔ ∀ e ∈ history.historicalBase (i 0), (i 0).time < e.time → delivers e → (i 2).world = e.world ∧ (i 2).time = e.time ∧ chance (i 2)

Every candidate who delivers a good job talk has an equal chance of being hired is true iff in every later historical alternative of the anchor where the talk is delivered, the hiring situation lies in its world, at its time, and gives an equal chance.

theorem Mendes2025.temporal_shift {W : Type u_1} {T : Type u_2} {i : State W T} [LinearOrder T] (history : HistoricalAlternatives W T) {cell : Finset Ordering} (A C : Reference.Index W T → Prop) {k l : State W T} (hk : (i, k) ∈ subj history 1 (DynamicSemantics.RegisterStructure.val 0) (fut (radical A))) (hl : (k, l) ∈ ind (DynamicSemantics.RegisterStructure.val 2) (DynamicSemantics.RegisterStructure.val 1) (temporal cell (radical C))) : (l 0).time < (l 1).time ∧ compare (l 2).time (l 1).time ∈ cell

The Subordinate Future places the situation it introduces after the anchor, and the main clause is timed by its tense relative to that situation, not the anchor. The rows of the paper's table of main-clause tenses are the cells future, present and past.

theorem Mendes2025.modal_donkey_anaphora {W : Type u_1} {T : Type u_2} {i : State W T} [LinearOrder T] (history : HistoricalAlternatives W T) {cell : Finset Ordering} (A C : Reference.Index W T → Prop) {k l : State W T} (hk : (i, k) ∈ subj history 1 (DynamicSemantics.RegisterStructure.val 0) (fut (radical A))) (hl : (k, l) ∈ ind (DynamicSemantics.RegisterStructure.val 2) (DynamicSemantics.RegisterStructure.val 1) (temporal cell (radical C))) : (l 2).world ∈ history (l 0)

In modal donkey anaphora the indicative retrieves the situation the subjunctive introduced, so the main clause is evaluated in a historical alternative of the anchor.

Modal displacement

A restrictor carrying the Subordinate Future is true at a state iff some historical alternative of the anchor, after it, satisfies it: the existence presupposition of a strong quantifier is satisfied in a historical alternative, not at the anchor, which is why the continuation I doubt anyone will come at all is felicitous. Under the indicative it must be satisfied in the anchor's world.

theorem Mendes2025.subj_fut_true_at {W : Type u_1} {T : Type u_2} {i : State W T} [LinearOrder T] (history : HistoricalAlternatives W T) (A : Reference.Index W T → Prop) : i ∈ SetRel.dom (subj history 1 (DynamicSemantics.RegisterStructure.val 0) (fut (radical A))) ↔ ∃ e ∈ history.historicalBase (i 0), (i 0).time < e.time ∧ A e

The Subordinate Future restrictor is true iff the anchor has a later historical alternative satisfying A.

theorem Mendes2025.ind_fut_true_at {W : Type u_1} {T : Type u_2} {i : State W T} [LinearOrder T] (A : Reference.Index W T → Prop) : i ∈ SetRel.dom (ind (DynamicSemantics.RegisterStructure.val 2) (DynamicSemantics.RegisterStructure.val 0) (fut (radical A))) ↔ (i 2).world = (i 0).world ∧ (i 0).time < (i 2).time ∧ A (i 2)

The indicative restrictor is true iff its situation lies in the anchor's world, after the anchor, and satisfies A.