Documentation

Linglib.Studies.AnandHacquard2013

Anand & Hacquard 2013: epistemics and attitudes #

[AH13] (Semantics & Pragmatics 6:8) survey the distribution of epistemic modals in the complements of attitude verbs across French, Italian, and Spanish: epistemics are fully acceptable under attitudes of acceptance (doxastics, argumentatives, semifactives), degraded under desideratives and directives, and emotive doxastics (hope, fear) and dubitatives (doubt) show a mixed pattern — possibility but not necessity.

The account combines two proposals. Epistemics quantify over an information state parameter obtained by anaphora to the embedding attitude ([Yal07], [Hac06]); attitudes split by representationality ([Bol68]): representational attitudes convey a mental picture and so provide an information state S = DOX(x,w), non-representational ones combine with their complement by comparative preference semantics ([Vil08]) and provide none, and hybrids have both components — the representational component licenses possibility epistemics while the uncertainty condition blocks necessity. Representationality, AttitudeClass, and LicensesEpistemic render the classification, and theory_matches_data checks the prediction against the paper's pooled acceptability survey.

The final section maps the hybrid structure onto Bayesian theory-of-mind inference ([BJEST17]; [HKWH+23]): the doxastic, preference, and uncertainty components are the belief marginal, the desire marginal, and non-extreme credence of a prospective emotion.

The representationality classification #

inductive AnandHacquard2013.Representationality :

Classification of attitude semantics by representationality: an attitude is representational iff its semantics provides a non-trivial information state that embedded epistemics can be anaphoric to (§3).

representational : Representationality
Provides the information state S = DOX(x,w): doxastics, argumentatives, semifactives.
nonRepresentational : Representationality
No information state: desideratives and directives, whose comparative semantics ([Vil08]) supplies S = ∅.
hybrid : Representationality
Both components: a representational component providing DOX and a preference component ordering alternatives — emotive doxastics and dubitatives.

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidableEqRepresentationality :

DecidableEq Representationality

Equations

AnandHacquard2013.instDecidableEqRepresentationality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AnandHacquard2013.instReprRepresentationality :

Repr Representationality

Equations

AnandHacquard2013.instReprRepresentationality = { reprPrec := AnandHacquard2013.instReprRepresentationality.repr }

def AnandHacquard2013.instReprRepresentationality.repr :

Representationality → ℕ → Std.Format

Equations

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

Instances For

def AnandHacquard2013.Representationality.HasInformationState :

Representationality → Prop

An attitude with a representational component provides an information state that epistemics can quantify over.

Equations

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidablePredRepresentationalityHasInformationState :

DecidablePred Representationality.HasInformationState

Equations

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

def AnandHacquard2013.Representationality.HasPreferenceComponent :

Representationality → Prop

An attitude with a preference component uses comparative semantics.

Equations

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidablePredRepresentationalityHasPreferenceComponent :

DecidablePred Representationality.HasPreferenceComponent

Equations

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

inductive AnandHacquard2013.EpistemicForce :

Epistemic modal force.

possibility : EpistemicForce
might, may (∃ over the information state).
necessity : EpistemicForce
must, have to (∀ over the information state).

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidableEqEpistemicForce :

DecidableEq EpistemicForce

Equations

AnandHacquard2013.instDecidableEqEpistemicForce x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AnandHacquard2013.instReprEpistemicForce :

Repr EpistemicForce

Equations

AnandHacquard2013.instReprEpistemicForce = { reprPrec := AnandHacquard2013.instReprEpistemicForce.repr }

def AnandHacquard2013.instReprEpistemicForce.repr :

EpistemicForce → ℕ → Std.Format

Equations

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

Instances For

def AnandHacquard2013.Representationality.LicensesEpistemic :

Representationality → EpistemicForce → Prop

The central prediction: representational attitudes license both forces, non-representational ones neither (the trivial modal base yields tautology or contradiction), and hybrids license possibility only — the uncertainty condition contradicts universal quantification over DOX.

Equations

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidableLicensesEpistemic (r : Representationality) (f : EpistemicForce) :

Decidable (r.LicensesEpistemic f)

Equations

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

theorem AnandHacquard2013.licensing_requires_information_state (r : Representationality) (f : EpistemicForce) (h : r.LicensesEpistemic f) :

r.HasInformationState

Epistemic licensing requires an information state.

inductive AnandHacquard2013.AttitudeClass :

The seven attitude classes of the survey.

doxastic : AttitudeClass
believe, think, suppose.
argumentative : AttitudeClass
say, argue, conclude.
semifactive : AttitudeClass
know, realize, discover.
desiderative : AttitudeClass
want, wish.
directive : AttitudeClass
demand, order, require.
emotiveDoxastic : AttitudeClass
hope, fear.
dubitative : AttitudeClass
doubt.

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidableEqAttitudeClass :

DecidableEq AttitudeClass

Equations

AnandHacquard2013.instDecidableEqAttitudeClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AnandHacquard2013.instReprAttitudeClass :

Repr AttitudeClass

Equations

AnandHacquard2013.instReprAttitudeClass = { reprPrec := AnandHacquard2013.instReprAttitudeClass.repr }

def AnandHacquard2013.instReprAttitudeClass.repr :

AttitudeClass → ℕ → Std.Format

Equations

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

Instances For

def AnandHacquard2013.AttitudeClass.representationality :

AttitudeClass → Representationality

The representationality of each attitude class.

Equations

Instances For

def AnandHacquard2013.AttitudeClass.LicensesEpistemic (c : AttitudeClass) (f : EpistemicForce) :

Epistemic licensing for an attitude class, via its representationality.

Equations

c.LicensesEpistemic f = c.representationality.LicensesEpistemic f

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidableLicensesEpistemic_1 (c : AttitudeClass) (f : EpistemicForce) :

Decidable (c.LicensesEpistemic f)

Equations

AnandHacquard2013.instDecidableLicensesEpistemic_1 c f = id inferInstance

def AnandHacquard2013.Representationality.fromSelector :

Mood.Selector → Representationality

The mood-selection correlate (§6): subjunctive tracks the preference component and indicative representationality, so the correlation with epistemic licensing is strong but imperfect — hybrids license possibility epistemics and select subjunctive.

Equations

Instances For

Empirical Data: Acceptability Ratings (Table 4) #

Cross-Romance Survey Data #

Seven-point acceptability ratings (1 = unacceptable, 7 = completely acceptable) for epistemic modals under attitude verbs, pooled across French (n=31), Italian (n=11), and Spanish (n=21).

Table 4: Pooled Descriptive Statistics (mean (sd) / median) #

	des/direct	emo dox	dubitative	semifactive	accept	Mean
might	3.5/3	5.1/6	6.1/7	6.1/7	6.4/7	5.4 (1.8)/6
must	1.9/1	2.7/2	3.1/2	5.6/6	6.0/7	3.9 (1.7)/4
probable	2.4/3	4.2/5	4.8/6	5.6/7	6.2/7	5.0 (1.9)/5

The critical contrasts:

Acceptance/semifactive: might ≈ must (both high)
Des/directive: might ≈ must (both low)
Emotive doxastic/dubitative: might >> must

The survey collapses some classes (doxastics ≈ argumentatives, desideratives ≈ directives), but the theory predicts the same licensing for collapsed classes — verified cell by cell in theory_matches_data.

inductive AnandHacquard2013.Acceptability :

Acceptability judgment: acceptable (median ≥ 5) or degraded.

acceptable : Acceptability
degraded : Acceptability

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidableEqAcceptability :

DecidableEq Acceptability

Equations

AnandHacquard2013.instDecidableEqAcceptability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AnandHacquard2013.instReprAcceptability.repr :

Acceptability → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance AnandHacquard2013.instReprAcceptability :

Repr Acceptability

Equations

AnandHacquard2013.instReprAcceptability = { reprPrec := AnandHacquard2013.instReprAcceptability.repr }

def AnandHacquard2013.observedAcceptability :

AttitudeClass → EpistemicForce → Acceptability

Observed acceptability from the survey data, indexed by the full AttitudeClass from Representationality.lean. Argumentatives pattern with doxastics; directives pattern with desideratives.

Equations

Instances For

def AnandHacquard2013.predictedAcceptability (att : AttitudeClass) (force : EpistemicForce) :

Predicted licensing: the prediction follows from the representationality classification, not per-cell stipulation.

Equations

AnandHacquard2013.predictedAcceptability att force = if att.LicensesEpistemic force then AnandHacquard2013.Acceptability.acceptable else AnandHacquard2013.Acceptability.degraded

Instances For

Theory Matches Data #

theorem AnandHacquard2013.theory_matches_data (att : AttitudeClass) (force : EpistemicForce) :

predictedAcceptability att force = observedAcceptability att force

The representationality theory correctly predicts all 14 cells (7 attitude classes × 2 epistemic forces).

Information State Semantics (Yalcin's S parameter) #

Epistemic Modals as Information-State Quantifiers #

Following [Yal07] and [Vel96], epistemic modals quantify over an information state parameter S:

⟦might φ⟧^{c,w,S,g} = 1 iff ∃w' ∈ S: ⟦φ⟧^{c,w',S,g} = 1
⟦must φ⟧^{c,w,S,g} = 1 iff ∀w' ∈ S: ⟦φ⟧^{c,w',S,g} = 1

Attitude verbs update S with their quantificational domain:

⟦att φ⟧^{c,w,S,g} = λx. ∀w' ∈ S': ⟦φ⟧^{c,w',S',g} = 1
where S' = quantificational domain provided by att

For representational attitudes: S' = DOX(x,w) (non-trivial) For non-representational attitudes: S' = ∅ (trivial → tautology/contradiction)

@[reducible, inline]

abbrev AnandHacquard2013.InfoState (W : Type u_2) :

Type u_2

Information state: a set of worlds (represented as a list).

Equations

AnandHacquard2013.InfoState W = List W

Instances For

def AnandHacquard2013.mightS {W : Type u_1} (S : InfoState W) (φ : W → Prop) :

Epistemic possibility over information state S: ⟦might φ⟧_S = ∃w' ∈ S: φ(w')

Equations

AnandHacquard2013.mightS S φ = ∃ w ∈ S, φ w

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidableMightSOfDecidablePred {W : Type u_1} {S : InfoState W} {φ : W → Prop} [DecidablePred φ] :

Decidable (mightS S φ)

Equations

AnandHacquard2013.instDecidableMightSOfDecidablePred = id inferInstance

def AnandHacquard2013.mustS {W : Type u_1} (S : InfoState W) (φ : W → Prop) :

Epistemic necessity over information state S: ⟦must φ⟧_S = ∀w' ∈ S: φ(w')

Equations

AnandHacquard2013.mustS S φ = ∀ w ∈ S, φ w

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidableMustSOfDecidablePred {W : Type u_1} {S : InfoState W} {φ : W → Prop} [DecidablePred φ] :

Decidable (mustS S φ)

Equations

AnandHacquard2013.instDecidableMustSOfDecidablePred = id inferInstance

def AnandHacquard2013.nonTrivial {W : Type u_1} (S : InfoState W) :

Non-triviality presupposition ([Geu05]): epistemics presuppose their modal base is non-trivial.

Equations

AnandHacquard2013.nonTrivial S = (S ≠ [])

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidableNonTrivialOfDecidableEq {W : Type u_1} [DecidableEq W] {S : InfoState W} :

Decidable (nonTrivial S)

Equations

AnandHacquard2013.instDecidableNonTrivialOfDecidableEq = id inferInstance

theorem AnandHacquard2013.might_defined_iff_nontrivial {W : Type u_1} (S : InfoState W) (φ : W → Prop) [DecidablePred φ] (_h : nonTrivial S) :

mightS S φ ∨ ¬mightS S φ

Epistemic possibility is defined (non-trivial) whenever S ≠ ∅.

theorem AnandHacquard2013.might_empty {W : Type u_1} (φ : W → Prop) :

¬mightS [] φ

With empty S, might is trivially false — yielding infelicity.

theorem AnandHacquard2013.must_empty {W : Type u_1} (φ : W → Prop) :

mustS [] φ

With empty S, must is trivially true — yielding infelicity.

Attitude Embedding: S-Update #

def AnandHacquard2013.representationalS {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) [(a : E) → (w w' : W) → Decidable (R a w w')] (agent : E) (w : W) (worlds : List W) :

Representational attitude embedding: S' = DOX(x,w). The doxastic alternatives form the information state that embedded epistemics quantify over.

Equations

AnandHacquard2013.representationalS R agent w worlds = List.filter (fun (w' : W) => decide (R agent w w')) worlds

Instances For

def AnandHacquard2013.nonRepresentationalS {W : Type u_1} :

Non-representational attitude embedding: S' = ∅. Comparative semantics provides no information state.

Equations

AnandHacquard2013.nonRepresentationalS = []

Instances For

theorem AnandHacquard2013.representational_nontrivial {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) [(a : E) → (w w' : W) → Decidable (R a w w')] (agent : E) (w : W) (worlds : List W) (h : ∃ w' ∈ worlds, R agent w w') :

nonTrivial (representationalS R agent w worlds)

Representational attitudes yield non-trivial information states (when there is at least one accessible world).

theorem AnandHacquard2013.nonRepresentational_trivial {W : Type u_1} :

¬nonTrivial nonRepresentationalS

Non-representational attitudes yield trivial information states.

Deriving the Distribution #

theorem AnandHacquard2013.believe_must {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) [(a : E) → (w w' : W) → Decidable (R a w w')] (agent : E) (w : W) (worlds : List W) (p : W → Prop) [DecidablePred p] :

mustS (representationalS R agent w worlds) p ↔ Doxastic.BoxAt R agent w worlds p

Under a representational attitude, embedded must p holds iff all doxastic alternatives satisfy p — a non-trivial claim.

theorem AnandHacquard2013.want_must_trivial {W : Type u_1} (p : W → Prop) :

mustS nonRepresentationalS p

Under a non-representational attitude, must p is trivially true.

theorem AnandHacquard2013.want_might_trivial {W : Type u_1} (p : W → Prop) :

¬mightS nonRepresentationalS p

Under a non-representational attitude, might p is trivially false.

The emotive doxastic lexical entry (56) #

⟦a hopes_C that p⟧: defined iff both p-verifiers and p-falsifiers exist among the doxastic alternatives (the uncertainty condition); where defined, true iff some doxastic alternative verifies p (the doxastic assertion) and the p-verifiers are preferred to the p-falsifiers above the contextual threshold (the preference assertion). φ-verifiers in S are the subsets of S certain about φ — for unmodalized p, pow(S ∩ p) — so verifier/falsifier non-emptiness is mightS S p ∧ mightS S ¬p. The doxastic component is what lets hope answer a question ([Sch08b]'s dialogue, attributed to Truckenbrodt: "Kommt Peter heute?" — "Ich hoffe/*will, dass er heute kommt") and distinguishes hope from pure-preferential want.

def AnandHacquard2013.hopeAt {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) [(a : E) → (w w' : W) → Decidable (R a w w')] (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) (agent : E) (p : Finset W) (w : W) (worlds : List W) (C : List (Finset W)) :

Semantics.Presupposition.PartialProp W

The (56) entry over the study's information-state semantics: presupposition = uncertainty, assertion = doxastic possibility plus preference. The doxastic conjunct is entailed by the first presupposition conjunct; the paper states it separately as the component embedded epistemics are anaphoric to.

Equations

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

Instances For

theorem AnandHacquard2013.must_contradicts_uncertainty {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) [(a : E) → (w w' : W) → Decidable (R a w w')] (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) (agent : E) (p : Finset W) (w : W) (worlds : List W) (C : List (Finset W)) (h_must : mustS (representationalS R agent w worlds) fun (x : W) => x ∈ p) :

¬(hopeAt R μ θ agent p w worlds C).presup w

Embedded must p contradicts the uncertainty presupposition ((48) against (47c)): if p holds throughout the doxastic state, there are no falsifiers — epistemic necessity is blocked under hope and fear.

theorem AnandHacquard2013.might_concord {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) [(a : E) → (w w' : W) → Decidable (R a w w')] (agent : E) (p : W → Prop) (w : W) (worlds : List W) (h : mightS (representationalS R agent w worlds) p) :

mightS (representationalS R agent w worlds) fun (x : W) => mightS (representationalS R agent w worlds) p

Embedded might p contributes the same doxastic content as bare p ((58), modal concord): a modalized complement is settled by the shared information state, so its verifiers are the p-verifiers — epistemic possibility is licensed.

Emotive Doxastic Finite Model #

Concrete Demonstration #

We instantiate the abstract theory with a finite model demonstrating the must/might asymmetry under emotive doxastics.

World model: 3 worlds {w₁, w₂, w₃}

w₁: it is raining
w₂: it is not raining
w₃: it is raining (backup)

John's beliefs (DOX): {w₁, w₂} — uncertain whether it's raining. John's preference: raining worlds preferred to non-raining.

Predictions:

"John hopes it is raining": ✓ (uncertainty + doxastic + preference)
"John hopes it might be raining": ✓ (same doxastic assertion)
"John hopes it must be raining": ✗ (contradicts uncertainty)

inductive AnandHacquard2013.RainWorld :

raining₁ : RainWorld
notRaining : RainWorld
raining₂ : RainWorld

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidableEqRainWorld :

DecidableEq RainWorld

Equations

AnandHacquard2013.instDecidableEqRainWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AnandHacquard2013.instReprRainWorld :

Equations

AnandHacquard2013.instReprRainWorld = { reprPrec := AnandHacquard2013.instReprRainWorld.repr }

def AnandHacquard2013.instReprRainWorld.repr :

RainWorld → ℕ → Std.Format

Equations

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

Instances For

def AnandHacquard2013.isRaining :

RainWorld → Prop

Equations

Instances For

@[instance_reducible]

instance AnandHacquard2013.instDecidablePredRainWorldIsRaining :

DecidablePred isRaining

Equations

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

def AnandHacquard2013.johnDox :

RainWorld → Bool

John's doxastic accessibility: worlds w₁ and w₂ are doxastically accessible (he's uncertain), w₃ is not.

Equations

Instances For

def AnandHacquard2013.allRainWorlds :

Equations

AnandHacquard2013.allRainWorlds = [AnandHacquard2013.RainWorld.raining₁, AnandHacquard2013.RainWorld.notRaining, AnandHacquard2013.RainWorld.raining₂]

Instances For

def AnandHacquard2013.johnS :

InfoState RainWorld

John's doxastic information state

Equations

AnandHacquard2013.johnS = List.filter AnandHacquard2013.johnDox AnandHacquard2013.allRainWorlds

Instances For

theorem AnandHacquard2013.johnS_eq :

johnS = [RainWorld.raining₁, RainWorld.notRaining]

theorem AnandHacquard2013.john_nontrivial :

nonTrivial johnS

John's DOX is non-trivial (he has beliefs).

theorem AnandHacquard2013.john_might_rain :

mightS johnS isRaining

"might be raining" is true in John's DOX — there's a raining world.

theorem AnandHacquard2013.john_must_rain :

¬mustS johnS isRaining

"must be raining" is false in John's DOX — there's a non-raining world.

theorem AnandHacquard2013.john_uncertain :

mightS johnS isRaining ∧ mightS johnS fun (w : RainWorld) => ¬isRaining w

Uncertainty: both raining and non-raining worlds in DOX.

BToM Connection: Prospective Emotions = Emotive Doxastics #

The BToM–Emotive Doxastic Bridge #

[HKWH+23]'s emotion model computes retrospective appraisals from BToM marginals. We show that [AH13]'s emotive doxastic semantics gives the formal content of prospective emotions computed from the same marginals.

The mapping:

A&H component	BToM computation
Doxastic assertion	beliefMarginal: Pr(b \| a) > 0 for b ⊨ φ
Uncertainty condition	0 < Σ_b Pr(b\|a)·⟦φ⟧_b < 1
Preference assertion	desireMarginal: Σ_d Pr(d\|a)·U(φ,d) > Σ_d Pr(d\|a)·U(¬φ,d)

This unification means:

hope is a prospective emotion with positive AU (prefers φ-resolution)
fear is a prospective emotion with negative AU (prefers ¬φ-resolution)
Both require the same BToM inference (belief + desire marginals)
The emotive doxastic lexical semantics IS the readout function for prospective emotions, just as the 8-dimensional β vector is the readout for retrospective emotions

theorem AnandHacquard2013.hope_from_uncertainty_and_preference (cred u_true u_false : ℚ) (h_pos : 0 < cred) (h_lt_one : cred < 1) (h_pref : u_false < u_true) :

{ beliefCredence := cred, utilityIfTrue := u_true, utilityIfFalse := u_false }.isHope = true

Hope holds from uncertainty + positive preference over resolutions.

theorem AnandHacquard2013.fear_from_uncertainty_and_dispreference (cred u_true u_false : ℚ) (h_pos : 0 < cred) (h_lt_one : cred < 1) (h_pref : u_true < u_false) :

{ beliefCredence := cred, utilityIfTrue := u_true, utilityIfFalse := u_false }.isFear = true

Fear holds from uncertainty + negative preference over resolutions.

theorem AnandHacquard2013.necessity_contradicts_uncertainty (cred : ℚ) (h_high : cred ≥ 1) (h_lt : cred < 1) :

False

The uncertainty condition in the emotive doxastic semantics is the same as requiring non-extreme credence in the BToM framework: Pr(φ) > 0 ∧ Pr(φ) < 1 ↔ ∃w' ∈ DOX: φ(w') ∧ ∃w' ∈ DOX: ¬φ(w').

This is the formal content of why necessity epistemics are blocked: Pr(φ) ≥ θ_must (≈ 1) contradicts Pr(φ) < 1.