Situation-level mood operators

[mendes-2025]'s mood operators work like determiners for situations: SUBJ introduces a new situation dref constrained to the historical alternatives of the anchor (like indefinite a), IND retrieves an existing situation and tests same-worldhood (like definite the). The Subordinate Future of Portuguese/Spanish — present morphology with future reference in subordinate contexts — is his main application: SF is subjunctive, introducing a future situation dref that the main clause retrieves for temporal anchoring (conditionalSF).

Main declarations

• SitPred, sameWorld — situation predicates and the modal kernel.
• SUBJ, IND — the situation-level mood operators.
• conditionalSF — the SF conditional.
• nonVeridical, subj_nonveridical — subjunctive non-veridicality.
• subjShift — SUBJ as a tower context shift.

@[reducible, inline]

abbrev Mood.SitPred (W : Type u_1) (T : Type u_2) : Type (max u_2 u_1)

A situation predicate, relating a described situation to its anchor.

Equations

• Mood.SitPred W T = (Reference.Index W T → Reference.Index W T → Prop)

@[reducible, inline]

abbrev Mood.sameWorld {W : Type u_1} {T : Type u_2} (s₁ s₂ : Reference.Index W T) : Prop

The modal kernel: two situations share their world coordinate. abbrev so decide/rw see through it.

Equations

• Mood.sameWorld s₁ s₂ = (s₁.world = s₂.world)

def Mood.SUBJ {W : Type u_1} {T : Type u_2} (history : HistoricalAlternatives W T) (P : SitPred W T) (s₀ : Reference.Index W T) [LE T] : Prop

The subjunctive introduces a new situation dref from the historical alternatives of the anchor — an indefinite for situations ([mendes-2025], Definition on p.29).

Equations

• Mood.SUBJ history P s₀ = ∃ s₁ ∈ history.historicalBase s₀, P s₁ s₀

def Mood.IND {W : Type u_1} {T : Type u_2} (P : SitPred W T) (s₁ s₂ : Reference.Index W T) : Prop

The indicative retrieves existing situations and tests that they share a world — a definite for situations ([mendes-2025], Definition on p.29).

Equations

• Mood.IND P s₁ s₂ = (Mood.sameWorld s₂ s₁ ∧ P s₂ s₁)

def Mood.conditionalSF {W : Type u_1} {T : Type u_2} (history : HistoricalAlternatives W T) [LE T] (antecedent : Reference.Index W T → Prop) (consequent : Reference.Index W T → Reference.Index W T → Prop) (s₀ : Reference.Index W T) : Prop

A conditional with an SF antecedent: SUBJ introduces the if situation, and the consequent is temporally anchored to it — why SF enables future reference ([mendes-2025]).

Equations

• Mood.conditionalSF history antecedent consequent s₀ = Mood.SUBJ history (fun (s₁ s₀' : Reference.Index W T) => antecedent s₁ → consequent s₁ s₀') s₀

theorem Mood.ind_same_world {W : Type u_1} {T : Type u_2} (P : SitPred W T) (s₁ s₂ : Reference.Index W T) (h : IND P s₁ s₂) : s₂.world = s₁.world

Surviving IND means the two situations share a world.

theorem Mood.subj_current_option {W : Type u_1} {T : Type u_2} (history : HistoricalAlternatives W T) (P : SitPred W T) (s₀ : Reference.Index W T) [Preorder T] (h_refl : history.reflexive) (h_P : P s₀ s₀) : SUBJ history P s₀

With a reflexive history, the anchor itself is always an option.

theorem Mood.subj_temporal_anchor {W : Type u_1} {T : Type u_2} (history : HistoricalAlternatives W T) (P : SitPred W T) (s₀ : Reference.Index W T) [LE T] (h : SUBJ history P s₀) : ∃ s₁ ∈ history.historicalBase s₀, s₁.time ≥ s₀.time ∧ P s₁ s₀

The introduced situation is a temporal anchor at or after the base situation's time — the mechanism SF exploits for future reference, and the parallel to attitude verbs shifting embedded evaluation to matrix event time (Studies/VonStechow2009.lean).

Non-veridicality

def Mood.nonVeridical {W : Type u_1} {T : Type u_2} (F : (Reference.Index W T → Prop) → Reference.Index W T → Prop) : Prop

A propositional operator is non-veridical iff F p can hold without p ([giannakidou-1998]).

Equations

• Mood.nonVeridical F = ∃ (P : Reference.Index W T → Prop) (s : Reference.Index W T), F P s ∧ ¬P s

theorem Mood.subj_nonveridical {W : Type u_1} {T : Type u_2} (history : HistoricalAlternatives W T) [LE T] (h_branching : ∃ (s₀ : Reference.Index W T), ∃ s₁ ∈ history.historicalBase s₀, s₀ ≠ s₁) : nonVeridical fun (P : Reference.Index W T → Prop) (s₀ : Reference.Index W T) => SUBJ history (fun (s₁ x : Reference.Index W T) => P s₁) s₀

SUBJ is non-veridical whenever the history branches: the introduced situation may differ from the actual one.

SUBJ as tower push

Entering a subjunctive clause pushes a mood-labeled context shift to the coordinates of the introduced situation; the existential quantification over situations is a separate semantic step. The tower version tracks depth for depth-sensitive operations (presupposition, tense indexing).

def Mood.subjShift {W : Type u_1} {T : Type u_2} {E : Type u_3} {P : Type u_4} (newWorld : W) (newTime : T) : Function.End (Reference.Context W E P T)

The context shift to the introduced situation's world and time.

Equations

• Mood.subjShift newWorld newTime c = { agent := c.agent, addressee := c.addressee, world := newWorld, time := newTime, position := c.position }