Situation-Dependent Attitude Semantics

[HK98] [Kra98a] [Lew79a] [vS09] [Ogi89]

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. [vS09] synthesizes [Lew79a], [HK98], and [Ogi89]: 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 → Intensional.WorldTimeIndex W Time → Intensional.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 : Intensional.WorldTimeIndex W Time) (situations : List (Intensional.WorldTimeIndex W Time)) (p : Tense.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 : Intensional.WorldTimeIndex W Time) (situations : List (Intensional.WorldTimeIndex W Time)) (p : Tense.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' : Intensional.WorldTimeIndex W Time) → Decidable (R a s s')] (agent : E) (s : Intensional.WorldTimeIndex W Time) (situations : List (Intensional.WorldTimeIndex W Time)) (p : Tense.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' : Intensional.WorldTimeIndex W Time) → Decidable (R a s s')] (agent : E) (s : Intensional.WorldTimeIndex W Time) (situations : List (Intensional.WorldTimeIndex W Time)) (p : Tense.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) : Tense.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 : Intensional.WorldTimeIndex W Time) (sits : List (Intensional.WorldTimeIndex W Time)) (p : W → Prop) : sitBoxAt (liftAccess R) agent s sits (liftProp p) ↔ Doxastic.boxAt R agent s.world (List.map (fun (x : Intensional.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 : Tense.SitProp W Time) (s : Intensional.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 : Tense.SitProp W Time) [DecidablePred p] (s : Intensional.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 : Intensional.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 [vS09]'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 : Tense.SitProp W Time) (s : Intensional.WorldTimeIndex W Time) (situations : List (Intensional.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 : Intensional.WorldTimeIndex W Time) (sits : List (Intensional.WorldTimeIndex W Time)) : (liftDoxastic V Time).holdsAt agent (liftProp p) s sits ↔ V.holdsAt agent p s.world (List.map (fun (x : Intensional.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 : Tense.SitProp W Time) (s : Intensional.WorldTimeIndex W Time) (sits : List (Intensional.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 : Tense.SitProp W Time) (s : Intensional.WorldTimeIndex W Time) (sits : List (Intensional.WorldTimeIndex W Time)) (hp : sitBoxAt R agent s sits p) (hpq : sitBoxAt R agent s sits fun (s' : Intensional.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 Tense.Basic (embedded frames) and Tense.SOT.Decomposition 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₂ : Intensional.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₂ : Intensional.WorldTimeIndex W Time) : Decidable (futureOriented R a s₁ s₂)

Equations

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