Situation-level mood operators

[Men25]'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) (Time : Type u_2) : Type (max u_2 u_1)

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

Equations

• Mood.SitPred W Time = (Intensional.WorldTimeIndex W Time → Intensional.WorldTimeIndex W Time → Prop)

@[reducible, inline]

abbrev Mood.sameWorld {W : Type u_1} {Time : Type u_2} (s₁ s₂ : Intensional.WorldTimeIndex W Time) : 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} {Time : Type u_2} (history : HistoricalAlternatives W Time) (P : SitPred W Time) (s₀ : Intensional.WorldTimeIndex W Time) [LE Time] : Prop

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

Equations

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

def Mood.IND {W : Type u_1} {Time : Type u_2} (P : SitPred W Time) (s₁ s₂ : Intensional.WorldTimeIndex W Time) : Prop

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

Equations

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

def Mood.conditionalSF {W : Type u_1} {Time : Type u_2} (history : HistoricalAlternatives W Time) [LE Time] (antecedent : Intensional.WorldTimeIndex W Time → Prop) (consequent : Intensional.WorldTimeIndex W Time → Intensional.WorldTimeIndex W Time → Prop) (s₀ : Intensional.WorldTimeIndex W Time) : 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 ([Men25]).

Equations

• Mood.conditionalSF history antecedent consequent s₀ = Mood.SUBJ history (fun (s₁ s₀' : Intensional.WorldTimeIndex W Time) => antecedent s₁ → consequent s₁ s₀') s₀

theorem Mood.ind_same_world {W : Type u_1} {Time : Type u_2} (P : SitPred W Time) (s₁ s₂ : Intensional.WorldTimeIndex W Time) (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} {Time : Type u_2} (history : HistoricalAlternatives W Time) (P : SitPred W Time) (s₀ : Intensional.WorldTimeIndex W Time) [Preorder Time] (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} {Time : Type u_2} (history : HistoricalAlternatives W Time) (P : SitPred W Time) (s₀ : Intensional.WorldTimeIndex W Time) [LE Time] (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 (Semantics/Attitudes/SituationDependent.lean).

Non-veridicality

def Mood.nonVeridical {W : Type u_1} {Time : Type u_2} (F : (Intensional.WorldTimeIndex W Time → Prop) → Intensional.WorldTimeIndex W Time → Prop) : Prop

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

Equations

• Mood.nonVeridical F = ∃ (P : Intensional.WorldTimeIndex W Time → Prop) (s : Intensional.WorldTimeIndex W Time), F P s ∧ ¬P s

theorem Mood.subj_nonveridical {W : Type u_1} {Time : Type u_2} (history : HistoricalAlternatives W Time) [LE Time] (h_branching : ∃ (s₀ : Intensional.WorldTimeIndex W Time), ∃ s₁ ∈ history.historicalBase s₀, s₀ ≠ s₁) : nonVeridical fun (P : Intensional.WorldTimeIndex W Time → Prop) (s₀ : Intensional.WorldTimeIndex W Time) => SUBJ history (fun (s₁ x : Intensional.WorldTimeIndex W Time) => 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} {Time : Type u_2} {E : Type u_3} {P : Type u_4} (newWorld : W) (newTime : Time) : Semantics.Context.ContextShift (Semantics.Context.KContext W E P Time)

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

Equations

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