Situation-Dependent Attitude Semantics

@cite{heim-kratzer-1998} @cite{kratzer-1998} @cite{lewis-1979-attitudes} @cite{von-stechow-2009} @cite{ogihara-1989}

Attitude operators with temporal parameters: believe's complement type shifts from st (propositions = W → Bool) to s(it) (situation-dependent propositions = WorldTimeIndex W Time → Bool). The doxastic alternatives Dox_y(w,t) become world–time pairs, not just worlds.

Motivation

Standard attitude semantics evaluates embedded clauses relative to worlds only: ⟦x believes p⟧(w) = ∀w' ∈ Dox_x(w). p(w')

This blocks sequence-of-tense (SOT) analysis, where embedded tense receives a shifted interpretation relative to the matrix event time. @cite{von-stechow-2009} synthesizes @cite{lewis-1979-attitudes}, @cite{heim-kratzer-1998}, and @cite{ogihara-1989}: believe's complement type shifts to s(it), and doxastic alternatives become situation pairs.

Design

Phase 1 (this module): Additive — new operators alongside existing ones, with lifting theorems proving generalization. Zero breaking changes.

Phase 2 (future): Migrate Doxastic.lean and Preferential.lean to use situation-dependent types natively, with backward-compat wrappers.

@[reducible, inline]

abbrev Semantics.Attitudes.SituationDependent.BAgentAccessRel (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Local alias for the agent-indexed accessibility relation used by the situation-dependent operators. Aliased to Semantics.Attitudes.Doxastic.AccessRel (Prop-valued, mathlib convention).

Equations

• Semantics.Attitudes.SituationDependent.BAgentAccessRel W E = Semantics.Attitudes.Doxastic.AccessRel W E

@[reducible, inline]

abbrev Semantics.Attitudes.SituationDependent.SitAccessRel (W : Type u_1) (Time : Type u_2) (E : Type u_3) : Type (max (max (max (max u_3 u_2) u_1) u_2) u_1)

Situation-dependent accessibility relation: Dox_y(w,t) = {(w',t') |...}.

Generalizes BAgentAccessRel W E = E → W → W → Prop to include temporal coordinates in both the evaluation and accessible situations.

Equations

• Semantics.Attitudes.SituationDependent.SitAccessRel W Time E = (E → Core.WorldTimeIndex W Time → Core.WorldTimeIndex W Time → Prop)

def Semantics.Attitudes.SituationDependent.sitBoxAt {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : SitAccessRel W Time E) (agent : E) (s : Core.WorldTimeIndex W Time) (situations : List (Core.WorldTimeIndex W Time)) (p : SitProp W Time) : Prop

Situation-dependent universal modal.

⟦□p⟧(s) = ∀s' ∈ situations. R(agent, s, s') → p(s')

Generalizes Doxastic.boxAt from worlds to situations.

Equations

• Semantics.Attitudes.SituationDependent.sitBoxAt R agent s situations p = ∀ s' ∈ situations, R agent s s' → p s'

def Semantics.Attitudes.SituationDependent.sitDiaAt {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : SitAccessRel W Time E) (agent : E) (s : Core.WorldTimeIndex W Time) (situations : List (Core.WorldTimeIndex W Time)) (p : SitProp W Time) : Prop

Situation-dependent existential modal.

⟦◇p⟧(s) = ∃s' ∈ situations. R(agent, s, s') ∧ p(s')

Generalizes Doxastic.diaAt from worlds to situations.

Equations

• Semantics.Attitudes.SituationDependent.sitDiaAt R agent s situations p = ∃ s' ∈ situations, R agent s s' ∧ p s'

@[implicit_reducible]

instance Semantics.Attitudes.SituationDependent.sitBoxAt_decidable {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : SitAccessRel W Time E) [(a : E) → (s s' : Core.WorldTimeIndex W Time) → Decidable (R a s s')] (agent : E) (s : Core.WorldTimeIndex W Time) (situations : List (Core.WorldTimeIndex W Time)) (p : SitProp W Time) [DecidablePred p] : Decidable (sitBoxAt R agent s situations p)

Equations

• Semantics.Attitudes.SituationDependent.sitBoxAt_decidable R agent s situations p = Semantics.Attitudes.SituationDependent.sitBoxAt_decidable._aux_1 R agent s situations p

@[implicit_reducible]

instance Semantics.Attitudes.SituationDependent.sitDiaAt_decidable {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : SitAccessRel W Time E) [(a : E) → (s s' : Core.WorldTimeIndex W Time) → Decidable (R a s s')] (agent : E) (s : Core.WorldTimeIndex W Time) (situations : List (Core.WorldTimeIndex W Time)) (p : SitProp W Time) [DecidablePred p] : Decidable (sitDiaAt R agent s situations p)

Equations

• Semantics.Attitudes.SituationDependent.sitDiaAt_decidable R agent s situations p = Semantics.Attitudes.SituationDependent.sitDiaAt_decidable._aux_1 R agent s situations p

def Semantics.Attitudes.SituationDependent.liftProp {W : Type u_1} {Time : Type u_2} (p : W → Prop) : SitProp W Time

Lift a world-proposition to a situation-proposition.

The lifted proposition ignores the temporal coordinate: liftProp p s = p s.world. This is the backward-compatibility embedding for code that hasn't moved to situation types yet.

Equations

• Semantics.Attitudes.SituationDependent.liftProp p s = p s.world

def Semantics.Attitudes.SituationDependent.liftAccess {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : BAgentAccessRel W E) : SitAccessRel W Time E

Lift a world-accessibility relation to a situation-accessibility relation.

The lifted relation ignores temporal coordinates in accessibility: liftAccess R agent s₁ s₂ = R agent s₁.world s₂.world. This gives classic Hintikka behavior where doxastic alternatives differ only in world, not time.

Equations

• Semantics.Attitudes.SituationDependent.liftAccess R agent s₁ s₂ = R agent s₁.world s₂.world

theorem Semantics.Attitudes.SituationDependent.sitBoxAt_lift_eq_boxAt {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : BAgentAccessRel W E) (agent : E) (s : Core.WorldTimeIndex W Time) (sits : List (Core.WorldTimeIndex W Time)) (p : W → Prop) : sitBoxAt (liftAccess R) agent s sits (liftProp p) ↔ Doxastic.boxAt R agent s.world (List.map (fun (x : Core.WorldTimeIndex W Time) => x.world) sits) p

KEY THEOREM: Lifted operators recover classic Hintikka semantics.

sitBoxAt (liftAccess R) agent s sits (liftProp p) is equivalent to boxAt R agent s.world (sits.map (·.world)) p.

This means code using the old world-only operators produces identical results when embedded in the situation framework.

def Semantics.Attitudes.SituationDependent.sitVeridicalityHolds {W : Type u_1} {Time : Type u_2} (v : Features.Veridicality) (p : SitProp W Time) (s : Core.WorldTimeIndex W Time) : Prop

Veridicality check for situation-dependent propositions.

For veridical predicates (know), requires p(s) at the evaluation situation. Mirrors Doxastic.veridicalityHolds.

Equations

• Semantics.Attitudes.SituationDependent.sitVeridicalityHolds Features.Veridicality.veridical p s = p s
• Semantics.Attitudes.SituationDependent.sitVeridicalityHolds Features.Veridicality.nonVeridical p s = True

@[implicit_reducible]

instance Semantics.Attitudes.SituationDependent.sitVeridicalityHolds_decidable {W : Type u_1} {Time : Type u_2} (v : Features.Veridicality) (p : SitProp W Time) [DecidablePred p] (s : Core.WorldTimeIndex W Time) : Decidable (sitVeridicalityHolds v p s)

Equations

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

theorem Semantics.Attitudes.SituationDependent.sitVeridicalityHolds_lift {W : Type u_1} {Time : Type u_2} (v : Features.Veridicality) (p : W → Prop) (s : Core.WorldTimeIndex W Time) : sitVeridicalityHolds v (liftProp p) s ↔ Doxastic.veridicalityHolds v p s.world

Lifted veridicality matches world-level veridicality.

structure Semantics.Attitudes.SituationDependent.SitDoxasticPredicate (W : Type u_1) (Time : Type u_2) (E : Type u_3) : Type (max (max u_1 u_2) u_3)

A situation-dependent doxastic attitude predicate.

Generalizes DoxasticPredicate to use situation-dependent accessibility: Dox_y(w,t) = {(w',t') |...} instead of Dox_y(w) = {w' |...}.

This is @cite{von-stechow-2009}'s enriched attitude semantics: ⟦x believes p⟧(w,t) = ∀(w',t') ∈ Dox_x(w,t). p(w')(t')

• name : String

  Name of the predicate

• access : SitAccessRel W Time E

  Situation-dependent accessibility relation

• veridicality : Features.Veridicality

  Veridicality (veridical or not)

def Semantics.Attitudes.SituationDependent.SitDoxasticPredicate.holdsAt {W : Type u_1} {Time : Type u_2} {E : Type u_3} (V : SitDoxasticPredicate W Time E) (agent : E) (p : SitProp W Time) (s : Core.WorldTimeIndex W Time) (situations : List (Core.WorldTimeIndex W Time)) : Prop

Semantics for a situation-dependent doxastic predicate.

⟦x V that p⟧(s) = veridicalityHolds(V, p, s) ∧ ∀s'. R(x,s,s') → p(s')

Generalizes DoxasticPredicate.holdsAt to situations.

Equations

• V.holdsAt agent p s situations = (Semantics.Attitudes.SituationDependent.sitVeridicalityHolds V.veridicality p s ∧ Semantics.Attitudes.SituationDependent.sitBoxAt V.access agent s situations p)

def Semantics.Attitudes.SituationDependent.liftDoxastic {W : Type u_1} {E : Type u_2} (V : Doxastic.DoxasticPredicate W E) (Time : Type u_3) : SitDoxasticPredicate W Time E

Lift a world-level DoxasticPredicate to a situation-dependent one.

The accessibility relation ignores temporal coordinates (classic Hintikka behavior), and veridicality is preserved. Use this to embed existing attitude predicates into the situation-dependent framework without changing their behavior.

Equations

• Semantics.Attitudes.SituationDependent.liftDoxastic V Time = { name := V.name, access := Semantics.Attitudes.SituationDependent.liftAccess V.access, veridicality := V.veridicality }

theorem Semantics.Attitudes.SituationDependent.liftDoxastic_holdsAt_eq {W : Type u_1} {Time : Type u_2} {E : Type u_3} (V : Doxastic.DoxasticPredicate W E) (agent : E) (p : W → Prop) (s : Core.WorldTimeIndex W Time) (sits : List (Core.WorldTimeIndex W Time)) : (liftDoxastic V Time).holdsAt agent (liftProp p) s sits ↔ V.holdsAt agent p s.world (List.map (fun (x : Core.WorldTimeIndex W Time) => x.world) sits)

The lifted predicate matches the original semantics.

(liftDoxastic V Time).holdsAt agent (liftProp p) s sits iff V.holdsAt agent p s.world (sits.map.world).

This is the key backward-compatibility theorem: any existing analysis using DoxasticPredicate can be replayed exactly in the situation-dependent framework by lifting.

theorem Semantics.Attitudes.SituationDependent.sit_veridical_entails_complement {W : Type u_1} {Time : Type u_2} {E : Type u_3} (V : SitDoxasticPredicate W Time E) (hV : V.veridicality = Features.Veridicality.veridical) (agent : E) (p : SitProp W Time) (s : Core.WorldTimeIndex W Time) (sits : List (Core.WorldTimeIndex W Time)) (holds : V.holdsAt agent p s sits) : p s

Veridical situation-dependent predicates entail their complement.

If x knows p at situation s, then p is true at s.

theorem Semantics.Attitudes.SituationDependent.sit_k_axiom {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : SitAccessRel W Time E) (agent : E) (p q : SitProp W Time) (s : Core.WorldTimeIndex W Time) (sits : List (Core.WorldTimeIndex W Time)) (hp : sitBoxAt R agent s sits p) (hpq : sitBoxAt R agent s sits fun (s' : Core.WorldTimeIndex W Time) => p s' → q s') : sitBoxAt R agent s sits q

Situation-dependent K axiom: closed under known implication.

If x believes p and x believes (p → q) at situation s, then x believes q at s.

Beyond Lifting: Temporal Accessibility Constraints

The lifting operators (liftAccess, liftProp) recover classic Hintikka semantics exactly. But the real power of situation-dependent attitudes comes from accessibility relations that genuinely constrain the temporal coordinate.

For example, an attitude verb might impose:

• Temporal binding: the doxastic alternative's time must match the matrix event time: R agent s s' → s'.time = s.time
• Temporal ordering: doxastic alternatives can only concern times at or after the attitude event: R agent s s' → s'.time ≥ s.time

These constraints are what make sequence-of-tense work: they tie the embedded clause's temporal interpretation to the matrix event time.

See Semantics.Tense.SequenceOfTense for the formal connection between these temporal constraints and SOT readings.

def Semantics.Attitudes.SituationDependent.temporallyBound {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : BAgentAccessRel W E) : SitAccessRel W Time E

Temporal binding constraint: accessible situations share the evaluation situation's time. This gives the "simultaneous" reading in sequence of tense.

Equations

• Semantics.Attitudes.SituationDependent.temporallyBound R agent s₁ s₂ = (R agent s₁.world s₂.world ∧ s₂.time = s₁.time)

@[implicit_reducible]

instance Semantics.Attitudes.SituationDependent.temporallyBound_decidable {W : Type u_1} {Time : Type u_2} {E : Type u_3} [DecidableEq Time] (R : BAgentAccessRel W E) [(a : E) → (w w' : W) → Decidable (R a w w')] (a : E) (s₁ s₂ : Core.WorldTimeIndex W Time) : Decidable (temporallyBound R a s₁ s₂)

Equations

• Semantics.Attitudes.SituationDependent.temporallyBound_decidable R a s₁ s₂ = id inferInstance

def Semantics.Attitudes.SituationDependent.futureOriented {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (R : BAgentAccessRel W E) : SitAccessRel W Time E

Future-oriented constraint: accessible situations have times at or after the evaluation time. This models forward-looking attitudes like "expect" or "intend".

Equations

• Semantics.Attitudes.SituationDependent.futureOriented R agent s₁ s₂ = (R agent s₁.world s₂.world ∧ s₁.time ≤ s₂.time)

@[implicit_reducible]

instance Semantics.Attitudes.SituationDependent.futureOriented_decidable {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [DecidableRel fun (x1 x2 : Time) => x1 ≤ x2] (R : BAgentAccessRel W E) [(a : E) → (w w' : W) → Decidable (R a w w')] (a : E) (s₁ s₂ : Core.WorldTimeIndex W Time) : Decidable (futureOriented R a s₁ s₂)

Equations

• Semantics.Attitudes.SituationDependent.futureOriented_decidable R a s₁ s₂ = id inferInstance