@[reducible, inline]

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

Type of situation predicates: (situation, situation) → Prop

The two situations are:

• s: The "local" or "described" situation
• s': The "anchor" or "reference" situation

Equations

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

@[reducible, inline]

abbrev Semantics.Mood.sameWorld {W : Type u_1} {Time : Type u_2} (s₁ s₂ : Core.WorldTimeIndex W Time) : Prop

The sameWorld kernel: two situations share their world coordinate.

This is the modal counterpart of the temporal kernels (Semantics.Tense.precedes/coincides/follows). The static IND operator and its dynamic lift Semantics.Mood.dynIND both call this kernel; they share the same modal constraint, lifted from a static situation predicate to a context filter via Semantics.Dynamic.Core.dynRelationOn.

abbrev (= @[reducible] def) so decide/rw see through it.

Equations

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

def Semantics.Mood.SUBJ {W : Type u_1} {Time : Type u_2} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (P : SitPred W Time) (s₀ : Core.WorldTimeIndex W Time) : Prop

SUBJ operator (@cite{mendes-2025}, Definition on p.29).

⟦SUBJ^{s₁}_{s₀}⟧ = λP. [s₁ | s₁ ∈ hist(s₀)]; P(s₁)(s₀)

The subjunctive:

1. Introduces a new situation dref s₁
2. Constrains s₁ to be in the historical alternatives of s₀
3. Passes s₁ and s₀ to the embedded predicate P

Analogous to an indefinite for situations.

Equations

• Semantics.Mood.SUBJ history P s₀ = ∃ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, P s₁ s₀

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

IND operator (@cite{mendes-2025}, Definition on p.29).

⟦IND_{s₁,s₂}⟧ = λP. [| s₂ ≤ w_{s₁}]; P(s₂)(s₁)

The indicative:

1. Retrieves existing situations s₁ and s₂
2. Requires s₂'s world to be "part of" s₁'s world (same world)
3. Passes s₂ and s₁ to P

Analogous to a definite for situations.

Equations

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

Mood as Event Closure

@cite{grano-2024} proposes that mood morphemes operate on the eventuality argument of the complement clause:

• IND: existentially closes the eventuality argument (87), yielding a proposition
• SBJV₁: leaves the eventuality argument open (88a), yielding an event predicate (identity function)
• SBJV₂: leaves the eventuality argument open AND requires causal self-reference (134), for intention reports

This is independent of — and complementary to — the situation-level SUBJ/IND operators defined above.

def Semantics.Mood.INDev {Event : Type u_1} (P : Event → Prop) : Prop

IND existentially closes the eventuality argument (@cite{grano-2024}, (87)).

⟦INDIC⟧ = λP_(⟨vt⟩).∃e.P(e)

The eventuality variable is bound; the complement denotes a proposition.

Equations

• Semantics.Mood.INDev P = ∃ (e : Event), P e

def Semantics.Mood.SBJVev₁ {Event : Type u_1} (P : Event → Prop) : Event → Prop

SBJV₁ leaves the eventuality argument open (@cite{grano-2024}, (88a); §7 Subjunctive₃ (135)).

⟦SBJV₁⟧ = λP_(⟨vt⟩).P

The complement retains type ⟨vt⟩ — an event predicate, not a proposition. In the core proposal (§5, (88a)), this is the general non-closing mood operator. In the §7 unified theory, it becomes specifically Subjunctive₃ (135) — the identity variant for perception predicates ('see'), causative predicates ('make'), and aspectual predicates ('begin'). These predicates require or are compatible with eventuality abstraction but do not involve causal self-reference or ordering semantics. Distinct from the 'want' variant (§7, Subjunctive₁ (133)), which uses Portner & Rubinstein's ln (local necessity), and the 'intend' variant (Subjunctive₂ (134) = SBJVev₂), which incorporates CAUSE*.

Equations

• Semantics.Mood.SBJVev₁ P = P

def Semantics.Mood.SBJVev₂ {Event : Type u_1} {W : Type u_2} (causeStar : Event → Event → W → Prop) (content : Event → W → Prop) (P : W → Event → Prop) (e : Event) : Prop

SBJV₂ leaves the eventuality argument open AND requires causal self-reference (@cite{grano-2024}, (134); unified theory §7).

⟦Subjunctive₂⟧ = λPλe[sn({λw.∃e'.CAUSE*(e,e',w) & P(w)(e')}, content(e), e)]

This is the variant operative with 'intend' in the §7 unified theory, which integrates CAUSE* from the core proposal (§4, (79)) with Portner & Rubinstein's (@cite{portner-rubinstein-2020}) modal quantification framework. The attitude state e must causally bring about the described event e' "in the right way" (@cite{searle-1983}; @cite{harman-1976}).

Equations

• Semantics.Mood.SBJVev₂ causeStar content P e = ∀ (w : W), content e w → ∃ (e' : Event), causeStar e e' w ∧ P w e'

theorem Semantics.Mood.INDev_is_propositional {Event : Type u_1} (P : Event → Prop) : INDev P = ∃ (e : Event), P e

IND closure yields a proposition (no free eventuality variable).

theorem Semantics.Mood.SBJVev₁_is_identity {Event : Type u_1} (P : Event → Prop) : SBJVev₁ P = P

SBJV₁ is the identity on event predicates.

inductive Semantics.Mood.MoodSelector : Type

Mood selection by embedding predicates.

Certain predicates select for specific moods in their complement:

• "know", "see" → typically indicative
• "want", "wish" → robustly subjunctive cross-linguistically
• "hope" → cross-linguistically variable (@cite{grano-2024}, Table 1)
• "say", "think" → mood-neutral (pragmatically flexible)

• indicativeSelecting : MoodSelector
• subjunctiveSelecting : MoodSelector
• crossLinguisticallyVariable : MoodSelector
• moodNeutral : MoodSelector

@[implicit_reducible]

instance Semantics.Mood.instDecidableEqMoodSelector : DecidableEq MoodSelector

Equations

• Semantics.Mood.instDecidableEqMoodSelector x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Mood.instReprMoodSelector : Repr MoodSelector

Equations

• Semantics.Mood.instReprMoodSelector = { reprPrec := Semantics.Mood.instReprMoodSelector.repr }

def Semantics.Mood.instReprMoodSelector.repr : MoodSelector → ℕ → Std.Format

Equations

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

def Semantics.Mood.prefersSubjunctive : MoodSelector → Bool

Does the selector prefer subjunctive?

Equations

• Semantics.Mood.prefersSubjunctive Semantics.Mood.MoodSelector.indicativeSelecting = false
• Semantics.Mood.prefersSubjunctive Semantics.Mood.MoodSelector.subjunctiveSelecting = true
• Semantics.Mood.prefersSubjunctive Semantics.Mood.MoodSelector.crossLinguisticallyVariable = false
• Semantics.Mood.prefersSubjunctive Semantics.Mood.MoodSelector.moodNeutral = false

def Semantics.Mood.conditionalSF {W : Type u_1} {Time : Type u_2} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (antecedent : Core.WorldTimeIndex W Time → Prop) (consequent : Core.WorldTimeIndex W Time → Core.WorldTimeIndex W Time → Prop) (s₀ : Core.WorldTimeIndex W Time) : Prop

Conditional with SF antecedent (@cite{mendes-2025}, main application).

"If Maria be.SF home, she will answer"

Structure:

1. SUBJ introduces s₁ ∈ hist(s₀) (the "if" situation)
2. Antecedent is evaluated at s₁
3. Consequent is temporally anchored to s₁

This explains why SF enables future reference: the subjunctive introduces a future situation that the main clause can refer back to.

Equations

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

def Semantics.Mood.conditionalIND {W : Type u_1} {Time : Type u_2} (antecedent consequent : Core.WorldTimeIndex W Time → Prop) (s : Core.WorldTimeIndex W Time) : Prop

Standard indicative conditional (for comparison).

"If Maria is home, she answers"

Here the antecedent is evaluated at the same situation as the main clause. No new situation is introduced.

Equations

• Semantics.Mood.conditionalIND antecedent consequent s = (antecedent s → consequent s)

theorem Semantics.Mood.subj_is_existential {W : Type u_1} {Time : Type u_2} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (P : SitPred W Time) (s₀ : Core.WorldTimeIndex W Time) : SUBJ history P s₀ → ∃ (s₁ : Core.WorldTimeIndex W Time), P s₁ s₀

SUBJ is existential: it introduces a situation.

theorem Semantics.Mood.subj_in_hist {W : Type u_1} {Time : Type u_2} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (P : SitPred W Time) (s₀ : Core.WorldTimeIndex W Time) : SUBJ history P s₀ → ∃ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, P s₁ s₀

SUBJ constrains to historical base: the introduced situation is in the historical alternatives.

theorem Semantics.Mood.ind_same_world {W : Type u_1} {Time : Type u_2} (P : SitPred W Time) (s₁ s₂ : Core.WorldTimeIndex W Time) : IND P s₁ s₂ → s₂.world = s₁.world

IND requires same world: the two situations must share a world.

theorem Semantics.Mood.subj_current_option {W : Type u_1} {Time : Type u_2} [Preorder Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (h_refl : history.reflexive) (P : SitPred W Time) (s₀ : Core.WorldTimeIndex W Time) (h_P : P s₀ s₀) : SUBJ history P s₀

SUBJ with reflexive history: if the history is reflexive, the current situation is always an option.

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

Non-veridicality:

A propositional operator F is non-veridical iff: F(p) does NOT entail p

The subjunctive is associated with non-veridical contexts because SUBJ introduces a situation that may differ from the actual one.

Equations

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

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

SUBJ is non-veridical: the introduced situation may differ from actual.

This follows from the existential nature of SUBJ: it quantifies over situations in the historical base, which includes non-actual futures.

SUBJ as Temporal Anchor

@cite{giannakidou-1998} @cite{mendes-2025} @cite{muskens-1996}

Both SUBJ's situation introduction and attitude embedding create new temporal reference points for embedded clauses:

• SUBJ: introduces s₁ ∈ hist(s₀) with τ(s₁) ≥ τ(s₀). The embedded clause evaluates at τ(s₁), not τ(s₀). This is why the Subordinate Future (SF) enables future reference.

• Attitude verbs: set embedded P = matrix E. The embedded clause's tense is relative to the matrix event time, not speech time.

The structural parallel: both mechanisms shift the temporal evaluation point of the embedded clause from the default (speech time or matrix time) to a newly introduced temporal anchor.

See Semantics.Attitudes.SituationDependent for the attitude side and Semantics.Tense.SequenceOfTense for the formal connection.

theorem Semantics.Mood.subj_temporal_anchor {W : Type u_1} {Time : Type u_2} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (P : SitPred W Time) (s₀ : Core.WorldTimeIndex W Time) (h : SUBJ history P s₀) : ∃ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, s₁.time ≥ s₀.time ∧ P s₁ s₀

SUBJ introduces a temporal anchor: the introduced situation's time is at or after the base situation's time.

This parallels attitude embedding, where the embedded clause's perspective time shifts to the matrix event time. Both mechanisms create a new temporal reference point for embedded evaluation.

SUBJ as Tower Push

SUBJ introduces a new situation from the historical base. In the tower framework, this corresponds to pushing a mood-labeled context shift that changes the world and time coordinates to those of the introduced situation.

The tower-based subjShift is not a replacement for the existential SUBJ operator — rather, it is the shift that the tower records when a subjunctive clause is entered. The existential quantification over situations is a separate semantic step. Both descriptions are independently useful: the tower version tracks depth and enables interaction with other depth-sensitive operations (presupposition, tense indexing); the existential version directly models the semantics.

def Semantics.Mood.subjShift {W : Type u_1} {Time : Type u_2} {E : Type u_3} {P : Type u_4} (newWorld : W) (newTime : Time) : Core.Context.ContextShift (Core.Context.KContext W E P Time)

SUBJ as a context shift: a mood-labeled shift that changes the world and time to those of the introduced situation.

This is the shift that the tower records when a subjunctive clause is entered. The newWorld and newTime are the coordinates of the existentially introduced situation s₁.

Equations

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

theorem Semantics.Mood.subjShift_changes_world {W : Type u_1} {Time : Type u_2} {E : Type u_3} {P : Type u_4} (w : W) (t : Time) (c : Core.Context.KContext W E P Time) : ((subjShift w t).apply c).world = w

Pushing a subjShift changes the world to the introduced situation's world.

theorem Semantics.Mood.subjShift_changes_time {W : Type u_1} {Time : Type u_2} {E : Type u_3} {P : Type u_4} (w : W) (t : Time) (c : Core.Context.KContext W E P Time) : ((subjShift w t).apply c).time = t

Pushing a subjShift changes the time to the introduced situation's time.

theorem Semantics.Mood.subjShift_preserves_agent {W : Type u_1} {Time : Type u_2} {E : Type u_3} {P : Type u_4} (w : W) (t : Time) (c : Core.Context.KContext W E P Time) : ((subjShift w t).apply c).agent = c.agent

Pushing a subjShift preserves the agent.

theorem Semantics.Mood.subj_as_tower_push {W : Type u_1} {Time : Type u_2} [LE Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (Q : SitPred W Time) (s₀ : Core.WorldTimeIndex W Time) : SUBJ history Q s₀ ↔ ∃ s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀, Q s₁ s₀

The tower-based subjunctive: SUBJ holds iff there exists a situation in the historical base such that pushing subjShift for that situation and evaluating the predicate yields truth.

This is the bridge between the existential SUBJ and the tower push.