Anand & Hacquard 2013: epistemics and attitudes

Epistemic modals are acceptable in the complements of attitudes of acceptance (think, say, realize), unacceptable under desideratives and directives, and acceptable under emotive doxastics (hope, fear) and dubitatives (doubt) with possibility but not necessity force, in seven-point acceptability surveys of French, Italian, and Spanish. The account combines Yalcin's information-state semantics, on which an epistemic quantifies over a state S anaphoric to the embedding attitude and presupposes S ≠ ∅, with Bolinger's split of attitudes: representational attitudes pass their doxastic state as S; non-representational ones set S = ∅ and combine with their complement by Villalta's comparison against the Heimian alternative ¬φ, so an embedded epistemic is never defined. Emotive doxastics and dubitatives are hybrids — a doxastic possibility assertion, a comparison of the complement's verifiers with its falsifiers, and an uncertainty presupposition demanding both — and the doxastic assertion of an embedded necessity modal contradicts that presupposition, while an embedded possibility modal contributes nothing new. Italian pensare selects the subjunctive yet licenses epistemics, so subjunctive is an imperfect correlate.

Main definitions

• SProp: a complement relative to an information state S, with might, must, ofSet.
• Better: Villalta's lift of an ordering to propositions; verifiers the sub-states settled on a complement.
• Licensed: whether some context makes an embedded epistemic defined and true.

References

• [AH13]
• [Yal07] — the information-state parameter, and the suppose sentences that (23) adapts
• [Vel96], [Hac06], [Hac10] — anaphoric modal bases
• [Bol68] — representational attitudes
• [Vil08] — comparative semantics for subjunctive-selecting attitudes
• [Hei92] — the alternative set {φ, ¬φ}
• [Geu05] — the non-triviality presupposition of modals
• [Sch08b] — the doxastic component of hope
• [Fal10] — Romanian vreun under want and hope

Complements relative to an information state

@[reducible, inline]

abbrev AnandHacquard2013.SProp (W : Type u_2) : Type u_2

A complement evaluated against an information state S — Yalcin's parameter — as a trivalent proposition for each S.

Equations

• AnandHacquard2013.SProp W = (Set W → W → SignType)

noncomputable def AnandHacquard2013.ofSet {W : Type u_1} (p : Set W) : SProp W

An unmodalized complement ignores the information state.

Equations

• AnandHacquard2013.ofSet p x✝ w = SignType.ofProp (w ∈ p)

noncomputable def AnandHacquard2013.might {W : Type u_1} (p : Set W) : SProp W

Epistemic possibility (37a) presupposes S ≠ ∅ and is true iff S contains a p-world.

Equations

• AnandHacquard2013.might p S = {_w : W | S.Nonempty}.indicator fun (x : W) => SignType.ofProp (S ∩ p).Nonempty

noncomputable def AnandHacquard2013.must {W : Type u_1} (p : Set W) : SProp W

Epistemic necessity (37b) presupposes S ≠ ∅ and is true iff S ⊆ p.

Equations

• AnandHacquard2013.must p S = {_w : W | S.Nonempty}.indicator fun (x : W) => SignType.ofProp (S ⊆ p)

def AnandHacquard2013.neg {W : Type u_1} (φ : SProp W) : SProp W

Negation of a complement, keeping its presupposition.

Equations

• AnandHacquard2013.neg φ S = -φ S

def AnandHacquard2013.conj {W : Type u_1} (φ ψ : SProp W) : SProp W

Conjunction of complements, defined where both are (Weak Kleene).

Equations

• AnandHacquard2013.conj φ ψ S w = (φ S w).meetWeak (ψ S w)

@[simp]

theorem AnandHacquard2013.ofSet_eq_one_iff {W : Type u_1} {p S : Set W} {w : W} : ofSet p S w = 1 ↔ w ∈ p

@[simp]

theorem AnandHacquard2013.ofSet_eq_neg_one_iff {W : Type u_1} {p S : Set W} {w : W} : ofSet p S w = -1 ↔ w ∉ p

@[simp]

theorem AnandHacquard2013.ofSet_ne_zero {W : Type u_1} {p S : Set W} {w : W} : ofSet p S w ≠ 0

@[simp]

theorem AnandHacquard2013.might_eq_one_iff {W : Type u_1} {p S : Set W} {w : W} : might p S w = 1 ↔ (S ∩ p).Nonempty

@[simp]

theorem AnandHacquard2013.might_eq_neg_one_iff {W : Type u_1} {p S : Set W} {w : W} : might p S w = -1 ↔ S.Nonempty ∧ ¬(S ∩ p).Nonempty

@[simp]

theorem AnandHacquard2013.might_eq_zero_iff {W : Type u_1} {p S : Set W} {w : W} : might p S w = 0 ↔ S = ∅

@[simp]

theorem AnandHacquard2013.must_eq_one_iff {W : Type u_1} {p S : Set W} {w : W} : must p S w = 1 ↔ S.Nonempty ∧ S ⊆ p

@[simp]

theorem AnandHacquard2013.must_eq_neg_one_iff {W : Type u_1} {p S : Set W} {w : W} : must p S w = -1 ↔ S.Nonempty ∧ ¬S ⊆ p

@[simp]

theorem AnandHacquard2013.must_eq_zero_iff {W : Type u_1} {p S : Set W} {w : W} : must p S w = 0 ↔ S = ∅

@[simp]

theorem AnandHacquard2013.neg_apply {W : Type u_1} {S : Set W} {w : W} (φ : SProp W) : neg φ S w = -φ S w

def AnandHacquard2013.accordingTo {W : Type u_1} (T : Set W) (φ : SProp W) : SProp W

An according to X phrase evaluates its complement at X's own information state (39).

Equations

• AnandHacquard2013.accordingTo T φ x✝ = φ T

inductive AnandHacquard2013.Force : Type

Epistemic modal force.

• possibility : Force
• necessity : Force

@[instance_reducible]

instance AnandHacquard2013.instDecidableEqForce : DecidableEq Force

Equations

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

@[instance_reducible]

instance AnandHacquard2013.instFintypeForce : Fintype Force

Equations

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

noncomputable def AnandHacquard2013.Force.modal {W : Type u_1} : Force → Set W → SProp W

The epistemic of a given force.

Equations

• AnandHacquard2013.Force.possibility.modal = AnandHacquard2013.might
• AnandHacquard2013.Force.necessity.modal = AnandHacquard2013.must

Representational and non-representational attitudes

noncomputable def AnandHacquard2013.representational {W : Type u_1} (dox : W → Set W) (φ : SProp W) : W → SignType

Under a representational attitude (29) the complement holds at every world of the attitude's domain, which also serves as its information state; it is the Weak Kleene universal over the domain.

Equations

• AnandHacquard2013.representational dox φ w = Trivalent.forallWeak fun (v : ↑(dox w)) => φ (dox w) ↑v

theorem AnandHacquard2013.representational_must_eq_one_iff {W : Type u_1} (dox : W → Set W) (p : Set W) (w : W) : representational dox (must p) w = 1 ↔ dox w ⊆ p

Vacuous quantification (35) — an embedded necessity epistemic claims that the domain is included in its prejacent.

theorem AnandHacquard2013.imagine_epistemic_eq_neg_one {W : Type u_1} (dox : W → Set W) (p : Set W) {w : W} (h : (dox w).Nonempty) : representational dox (conj (ofSet p) (might pᶜ)) w = -1

The paper's (23b), imagine that it is raining but it might not be, is contradictory whenever the imagination state is nonempty, since the modal quantifies over that very state.

def AnandHacquard2013.Better {α : Type u_2} (r : α → α → Prop) (p q : Set α) : Prop

Villalta's lift of a strict ordering to sets (32b) requires that every member of q is bettered by some member of p, and some member of p is bettered by no member of q. Applied to sets of sets it is the ordering of (52).

Equations

• AnandHacquard2013.Better r p q = ((∀ v ∈ q, ∃ u ∈ p, r u v) ∧ ∃ u ∈ p, ∀ v ∈ q, ¬r v u)

theorem AnandHacquard2013.Better.mono_left {α : Type u_2} {r : α → α → Prop} {p p' q : Set α} (h : Better r p q) (hp : p ⊆ p') : Better r p' q

theorem AnandHacquard2013.Better.anti_right {α : Type u_2} {r : α → α → Prop} {p q q' : Set α} (h : Better r p q) (hq : q' ⊆ q) : Better r p q'

noncomputable def AnandHacquard2013.preferential {W : Type u_1} (des : W → W → W → Prop) (φ : SProp W) : W → SignType

Under a non-representational attitude (36) the information state is reset to ∅, and the complement evaluated there is compared with its negation — Villalta's comparison over the Heimian alternative set {φ, ¬φ}, with des w the desirability ordering at w, setting the worlds where the complement is true against those where its negation is.

Equations

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

theorem AnandHacquard2013.preferential_modal_eq_zero {W : Type u_1} (des : W → W → W → Prop) (f : Force) (p : Set W) (w : W) : preferential des (f.modal p) w = 0

In (38) an epistemic embedded under a non-representational attitude inherits the empty information state and fails its non-triviality presupposition.

theorem AnandHacquard2013.preferential_accordingTo_ne_zero_iff {W : Type u_1} (des : W → W → W → Prop) (T : Set W) (f : Force) (p : Set W) (w : W) : preferential des (accordingTo T (f.modal p)) w ≠ 0 ↔ T.Nonempty

The escape hatch (39) is an according to X phrase making the embedded epistemic defined exactly when X's information state is nonempty.

Verifiers and falsifiers

def AnandHacquard2013.subStates {α : Type u_2} (A : Set α) : Set (Set α)

The nonempty sub-states of A.

Equations

• AnandHacquard2013.subStates A = {X : Set α | X ⊆ A ∧ X.Nonempty}

def AnandHacquard2013.verifiers {W : Type u_1} (φ : SProp W) (S : Set W) : Set (Set W)

The φ-verifiers in S (50) are the nonempty sub-states of S on all of whose sub-states φ holds throughout.

Equations

• AnandHacquard2013.verifiers φ S = {X : Set W | X ⊆ S ∧ X.Nonempty ∧ ∀ Y ⊆ X, ∀ w ∈ Y, φ Y w = 1}

def AnandHacquard2013.falsifiers {W : Type u_1} (φ : SProp W) (S : Set W) : Set (Set W)

The φ-falsifiers in S are the ¬φ-verifiers.

Equations

• AnandHacquard2013.falsifiers φ S = AnandHacquard2013.verifiers (AnandHacquard2013.neg φ) S

theorem AnandHacquard2013.verifiers_eq {W : Type u_1} {φ : SProp W} {q : Set W} (h : ∀ (X : Set W), (∀ Y ⊆ X, ∀ w ∈ Y, φ Y w = 1) ↔ X ⊆ q) (S : Set W) : verifiers φ S = subStates (S ∩ q)

theorem AnandHacquard2013.verifiers_ofSet {W : Type u_1} (p S : Set W) : verifiers (ofSet p) S = subStates (S ∩ p)

By Figure 3 the verifiers of p, might p, and must p in S are all the nonempty sub-states of S ∩ p.

theorem AnandHacquard2013.verifiers_might {W : Type u_1} (p S : Set W) : verifiers (might p) S = subStates (S ∩ p)

theorem AnandHacquard2013.verifiers_must {W : Type u_1} (p S : Set W) : verifiers (must p) S = subStates (S ∩ p)

theorem AnandHacquard2013.falsifiers_ofSet {W : Type u_1} (p S : Set W) : falsifiers (ofSet p) S = subStates (S ∩ pᶜ)

By Figure 3 the falsifiers of p, might p, and must p in S are all the nonempty sub-states of S ∩ pᶜ.

theorem AnandHacquard2013.falsifiers_might {W : Type u_1} (p S : Set W) : falsifiers (might p) S = subStates (S ∩ pᶜ)

theorem AnandHacquard2013.falsifiers_must {W : Type u_1} (p S : Set W) : falsifiers (must p) S = subStates (S ∩ pᶜ)

theorem AnandHacquard2013.better_subStates_iff {α : Type u_2} (r : α → α → Prop) (A B : Set α) : Better (Better r) (subStates A) (subStates B) ↔ Better r A B

By footnote 19, comparing two families of nonempty sub-states under the lifted ordering is comparing the states themselves, by upward monotonicity of Better in its first argument and downward monotonicity in its second.

theorem AnandHacquard2013.prefers_iff {W : Type u_1} {φ : SProp W} {p S : Set W} (r : W → W → Prop) (hv : verifiers φ S = subStates (S ∩ p)) (hf : falsifiers φ S = subStates (S ∩ pᶜ)) : Better (Better r) (verifiers φ S) (falsifiers φ S) ↔ Better r (S ∩ p) (S ∩ pᶜ)

In (51) the preference component of an emotive doxastic compares S ∩ p with S ∩ pᶜ.

theorem AnandHacquard2013.prefers_modal_iff {W : Type u_1} (r : W → W → Prop) (p S : Set W) (f : Force) : Better (Better r) (verifiers (f.modal p) S) (falsifiers (f.modal p) S) ↔ Better (Better r) (verifiers (ofSet p) S) (falsifiers (ofSet p) S)

The preference component does not see the modal, so hopes p, hopes might p, and hopes must p all prefer the p-verifying doxastic alternatives.

Emotive doxastics and dubitatives

def AnandHacquard2013.Uncertain {W : Type u_1} (φ : SProp W) (S : Set W) : Prop

The uncertainty condition (54) demands that the complement has both verifiers and falsifiers in the doxastic state.

Equations

• AnandHacquard2013.Uncertain φ S = ((AnandHacquard2013.verifiers φ S).Nonempty ∧ (AnandHacquard2013.falsifiers φ S).Nonempty)

def AnandHacquard2013.Possible {W : Type u_1} (φ : SProp W) (S : Set W) : Prop

The doxastic assertion (53) says the complement holds at some world of the doxastic state.

Equations

• AnandHacquard2013.Possible φ S = ∃ w ∈ S, φ S w = 1

noncomputable def AnandHacquard2013.hope {W : Type u_1} (des : W → W → W → Prop) (dox : W → Set W) (φ : SProp W) : W → SignType

a hopes that φ (55) presupposes uncertainty and asserts doxastic possibility and that the verifiers are more desirable than the falsifiers. fear has the shape of doubt over the desirability ordering.

Equations

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

noncomputable def AnandHacquard2013.doubt {W : Type u_1} (prob : W → W → W → Prop) (dox : W → Set W) (φ : SProp W) : W → SignType

a doubts that φ (63) is as hope, with the falsifiers likelier than the verifiers.

Equations

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

theorem AnandHacquard2013.hope_eq_one_iff {W : Type u_1} {r : W → W → W → Prop} {dox : W → Set W} {φ : SProp W} {w : W} : hope r dox φ w = 1 ↔ Uncertain φ (dox w) ∧ Possible φ (dox w) ∧ Better (Better (r w)) (verifiers φ (dox w)) (falsifiers φ (dox w))

theorem AnandHacquard2013.doubt_eq_one_iff {W : Type u_1} {r : W → W → W → Prop} {dox : W → Set W} {φ : SProp W} {w : W} : doubt r dox φ w = 1 ↔ Uncertain φ (dox w) ∧ Possible φ (dox w) ∧ Better (Better (r w)) (falsifiers φ (dox w)) (verifiers φ (dox w))

theorem AnandHacquard2013.uncertain_must_not_possible {W : Type u_1} {p S : Set W} (hu : Uncertain (must p) S) : ¬Possible (must p) S

In (58) with must, the doxastic assertion of an embedded necessity epistemic puts the whole state inside p, leaving no falsifier — it contradicts the uncertainty presupposition.

theorem AnandHacquard2013.hope_must_ne_one {W : Type u_1} (des : W → W → W → Prop) (dox : W → Set W) (p : Set W) (w : W) : hope des dox (must p) w ≠ 1

theorem AnandHacquard2013.doubt_must_ne_one {W : Type u_1} (prob : W → W → W → Prop) (dox : W → Set W) (p : Set W) (w : W) : doubt prob dox (must p) w ≠ 1

theorem AnandHacquard2013.hope_neg_might_ne_one {W : Type u_1} (des : W → W → W → Prop) (dox : W → Set W) (p : Set W) (w : W) : hope des dox (neg (might p)) w ≠ 1

In (74) a possibility epistemic scoping under negation is a universal claim and fails like must.

theorem AnandHacquard2013.possible_might_iff {W : Type u_1} (p S : Set W) : Possible (might p) S ↔ Possible (ofSet p) S

theorem AnandHacquard2013.hope_might {W : Type u_1} (des : W → W → W → Prop) (dox : W → Set W) (p : Set W) : hope des dox (might p) = hope des dox (ofSet p)

Under an emotive doxastic, might p and bare p have the same uncertainty presupposition, doxastic assertion, and preference, so (59) is (57) — modal concord.

theorem AnandHacquard2013.doubt_might {W : Type u_1} (prob : W → W → W → Prop) (dox : W → Set W) (p : Set W) : doubt prob dox (might p) = doubt prob dox (ofSet p)

The distribution

inductive AnandHacquard2013.AttitudeClass : Type

The attitude classes of Table 3.

• doxastic : AttitudeClass
• argumentative : AttitudeClass
• semifactive : AttitudeClass
• desiderative : AttitudeClass
• directive : AttitudeClass
• emotiveDoxastic : AttitudeClass
• dubitative : AttitudeClass

@[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.instFintypeAttitudeClass : Fintype AttitudeClass

Equations

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

inductive AnandHacquard2013.Kind : Type

The four lexical semantics the paper assigns.

• acceptance : Kind
• preferenceOriented : Kind
• emotiveDoxastic : Kind
• dubitative : Kind

@[instance_reducible]

instance AnandHacquard2013.instDecidableEqKind : DecidableEq Kind

Equations

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

def AnandHacquard2013.AttitudeClass.kind : AttitudeClass → Kind

Attitudes of acceptance are representational (§3.3), desideratives and directives preference-oriented (36), and the two hybrid classes get (55) and (63).

Equations

• AnandHacquard2013.AttitudeClass.doxastic.kind = AnandHacquard2013.Kind.acceptance
• AnandHacquard2013.AttitudeClass.argumentative.kind = AnandHacquard2013.Kind.acceptance
• AnandHacquard2013.AttitudeClass.semifactive.kind = AnandHacquard2013.Kind.acceptance
• AnandHacquard2013.AttitudeClass.desiderative.kind = AnandHacquard2013.Kind.preferenceOriented
• AnandHacquard2013.AttitudeClass.directive.kind = AnandHacquard2013.Kind.preferenceOriented
• AnandHacquard2013.AttitudeClass.emotiveDoxastic.kind = AnandHacquard2013.Kind.emotiveDoxastic
• AnandHacquard2013.AttitudeClass.dubitative.kind = AnandHacquard2013.Kind.dubitative

noncomputable def AnandHacquard2013.Kind.entry {W : Type u_1} : Kind → (W → W → W → Prop) → (W → Set W) → SProp W → W → SignType

The lexical entry of each kind, over the attitude's scale, doxastic state, and complement.

Equations

• AnandHacquard2013.Kind.acceptance.entry = fun (x : W → W → W → Prop) (dox : W → Set W) => AnandHacquard2013.representational dox
• AnandHacquard2013.Kind.preferenceOriented.entry = fun (r : W → W → W → Prop) (x : W → Set W) => AnandHacquard2013.preferential r
• AnandHacquard2013.Kind.emotiveDoxastic.entry = AnandHacquard2013.hope
• AnandHacquard2013.Kind.dubitative.entry = AnandHacquard2013.doubt

def AnandHacquard2013.Licensed (W : Type u_2) (k : Kind) (f : Force) : Prop

An epistemic of force f is licensed under a kind of attitude when some scale, doxastic state, prejacent, and world make the embedding defined and true.

Equations

• AnandHacquard2013.Licensed W k f = ∃ (r : W → W → W → Prop) (dox : W → Set W) (p : Set W) (w : W), k.entry r dox (f.modal p) w = 1

theorem AnandHacquard2013.licensed_acceptance {W : Type u_1} [Nontrivial W] (f : Force) : Licensed W Kind.acceptance f

theorem AnandHacquard2013.not_licensed_preferenceOriented {W : Type u_1} (f : Force) : ¬Licensed W Kind.preferenceOriented f

theorem AnandHacquard2013.licensed_emotiveDoxastic_possibility {W : Type u_1} [Nontrivial W] : Licensed W Kind.emotiveDoxastic Force.possibility

theorem AnandHacquard2013.not_licensed_emotiveDoxastic_necessity {W : Type u_1} : ¬Licensed W Kind.emotiveDoxastic Force.necessity

theorem AnandHacquard2013.licensed_dubitative_possibility {W : Type u_1} [Nontrivial W] : Licensed W Kind.dubitative Force.possibility

theorem AnandHacquard2013.not_licensed_dubitative_necessity {W : Type u_1} : ¬Licensed W Kind.dubitative Force.necessity

theorem AnandHacquard2013.licensed_iff {W : Type u_1} [Nontrivial W] (k : Kind) (f : Force) : Licensed W k f ↔ k ≠ Kind.preferenceOriented ∧ (k = Kind.acceptance ∨ f = Force.possibility)

Table 3, derived — epistemics are licensed by representational attitudes, by no preferential attitude, and by the hybrids only with possibility force.

The paper's examples

def AnandHacquard2013.AttitudeClass.ofString? : String → Option AttitudeClass

The attitude_class feature of an example row.

Equations

• AnandHacquard2013.AttitudeClass.ofString? "doxastic" = some AnandHacquard2013.AttitudeClass.doxastic
• AnandHacquard2013.AttitudeClass.ofString? "argumentative" = some AnandHacquard2013.AttitudeClass.argumentative
• AnandHacquard2013.AttitudeClass.ofString? "semifactive" = some AnandHacquard2013.AttitudeClass.semifactive
• AnandHacquard2013.AttitudeClass.ofString? "desiderative" = some AnandHacquard2013.AttitudeClass.desiderative
• AnandHacquard2013.AttitudeClass.ofString? "directive" = some AnandHacquard2013.AttitudeClass.directive
• AnandHacquard2013.AttitudeClass.ofString? "emotive_doxastic" = some AnandHacquard2013.AttitudeClass.emotiveDoxastic
• AnandHacquard2013.AttitudeClass.ofString? "dubitative" = some AnandHacquard2013.AttitudeClass.dubitative
• AnandHacquard2013.AttitudeClass.ofString? x✝ = none

def AnandHacquard2013.Force.ofString? : String → Option Force

The modal_force feature of an example row.

Equations

• AnandHacquard2013.Force.ofString? "possibility" = some AnandHacquard2013.Force.possibility
• AnandHacquard2013.Force.ofString? "necessity" = some AnandHacquard2013.Force.necessity
• AnandHacquard2013.Force.ofString? x✝ = none

theorem AnandHacquard2013.rows_track_licensing {W : Type u_1} [Nontrivial W] (r : Datum) : r ∈ Examples.all → r.feature? "anchor" = some "attitude" → r.feature? "modal_flavor" = some "epistemic" → ∀ (c : AttitudeClass) (f : Force), (r.feature? "attitude_class").bind AttitudeClass.ofString? = some c → (r.feature? "modal_force").bind Force.ofString? = some f → (r.judgment = Judgment.acceptable ↔ Licensed W c.kind f)

Every epistemic anchored to its embedding attitude is judged acceptable exactly when Licensed holds for the attitude's kind and the modal's force.

theorem AnandHacquard2013.unacceptable_rows_subjunctive (r : Datum) : r ∈ Examples.all → r.feature? "anchor" = some "attitude" → r.judgment = Judgment.unacceptable → r.feature? "mood" = none ∨ r.feature? "mood" = some "subjunctive"

Every unacceptable attitude-anchored epistemic in the Romance data sits in a subjunctive complement (§5.1); the converse fails at (18), (20), and (65).