Situation-Dependent Attitude Semantics

@cite{heim-kratzer-1998} @cite{kratzer-1998} @cite{lewis-1979} @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 = Situation 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}, @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.SitProp (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

Situation-dependent proposition type (von Stechow's s(it), Bool-valued for computational RSA evaluation).

Where standard propositions are W → Bool (sets of worlds), situation-dependent propositions are Situation W Time → Bool (sets of world–time pairs). This is the complement type for attitude verbs that support temporal interpretation.

Note: a Prop-valued counterpart exists at Semantics.Tense.SitProp for proof-level temporal reasoning. The split follows the Prop'/BProp pattern in Core/Proposition.lean.

Equations

• Semantics.Attitudes.SituationDependent.SitProp W Time = (Situation W Time → Bool)

@[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 AgentAccessRel W E = E → W → W → Bool to include temporal coordinates in both the evaluation and accessible situations.

Equations

• Semantics.Attitudes.SituationDependent.SitAccessRel W Time E = (E → Situation W Time → Situation W Time → Bool)

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 : Situation W Time) (situations : List (Situation W Time)) (p : SitProp W Time) : Bool

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 = situations.all fun (s' : Situation W Time) => !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 : Situation W Time) (situations : List (Situation W Time)) (p : SitProp W Time) : Bool

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 = situations.any fun (s' : Situation W Time) => R agent s s' && p s'

def Semantics.Attitudes.SituationDependent.liftProp {W : Type u_1} {Time : Type u_2} (p : W → Bool) : 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 : Core.ModalLogic.AgentAccessRel 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 : Core.ModalLogic.AgentAccessRel W E) (agent : E) (s : Situation W Time) (sits : List (Situation W Time)) (p : W → Bool) : sitBoxAt (liftAccess R) agent s sits (liftProp p) = Doxastic.boxAt R agent s.world (List.map (fun (x : Situation 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 : Doxastic.Veridicality) (p : SitProp W Time) (s : Situation W Time) : Bool

Veridicality check for situation-dependent propositions.

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

Equations

• Semantics.Attitudes.SituationDependent.sitVeridicalityHolds Semantics.Attitudes.Doxastic.Veridicality.veridical p s = p s
• Semantics.Attitudes.SituationDependent.sitVeridicalityHolds Semantics.Attitudes.Doxastic.Veridicality.nonVeridical p s = true

theorem Semantics.Attitudes.SituationDependent.sitVeridicalityHolds_lift {W : Type u_1} {Time : Type u_2} (v : Doxastic.Veridicality) (p : W → Bool) (s : Situation 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 : Doxastic.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 : Situation W Time) (situations : List (Situation W Time)) : Bool

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

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

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 → Bool) (s : Situation W Time) (sits : List (Situation W Time)) : (liftDoxastic V Time).holdsAt agent (liftProp p) s sits = V.holdsAt agent p s.world (List.map (fun (x : Situation W Time) => x.world) sits)

The lifted predicate matches the original semantics.

(liftDoxastic V Time).holdsAt agent (liftProp p) s sits equals 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 = Doxastic.Veridicality.veridical) (agent : E) (p : SitProp W Time) (s : Situation W Time) (sits : List (Situation W Time)) (holds : V.holdsAt agent p s sits = true) : p s = true

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 : Situation W Time) (sits : List (Situation W Time)) (hp : sitBoxAt R agent s sits p = true) (hpq : (sitBoxAt R agent s sits fun (s' : Situation W Time) => !p s' || q s') = true) : sitBoxAt R agent s sits q = true

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} [DecidableEq Time] (R : Core.ModalLogic.AgentAccessRel 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)

def Semantics.Attitudes.SituationDependent.futureOriented {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [DecidableRel fun (x1 x2 : Time) => x1 ≤ x2] (R : Core.ModalLogic.AgentAccessRel 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 && decide (s₁.time ≤ s₂.time))