Yalcin (2007): Epistemic Modals

This file formalizes Yalcin's domain semantics for epistemic modals and the puzzle of epistemic contradictions, sentences of the form it is raining and it might not be raining or it is not raining and it might be raining. Unlike Moore-paradoxical sentences, which are unassertable but embed happily under suppose and in conditional antecedents, epistemic contradictions are unsupposable, and a relational semantics cannot explain this, since it makes them true at some world (exists_relational_contra). Domain semantics evaluates a sentence at an index of an information parameter, a set of worlds, and a world, with the epistemic possibility modal quantifying existentially over the parameter (Sentence.might). Attitude verbs shift the parameter to the attitude state and quantify over it (supposes), so the universal quantifier of suppose is trumped by an embedded modal (supposes_might_iff), an attitude with an embedded possibility modal is the attitude's dual (supposes_might_iff_not_supposes_compl), and no state of supposition accepts an epistemic contradiction (not_supposes_contra). An indicative conditional shifts the parameter to the largest nonempty substate accepting its antecedent and quantifies over it (ifThen), so conditionals with an epistemic contradiction as antecedent are never true (ifThen_contra_false), and the conditional with an epistemic necessity in its consequent is equivalent to the plain one (ifThen_must_iff). Three notions of consequence are compared. Standard and diagonal consequence preserve truth at points, the latter at points whose world lies in the information state; informational consequence preserves acceptance, truth throughout a state evaluated at that state (InfoConsequence). Informational consequence validates Łukasiewicz's principle, epistemic contradiction, and the nonfactivity of epistemic possibility together (lukasiewicz, epistemic_contradiction, nonfactivity), which no classical consequence relation can, while diagonal consequence rejects epistemic contradiction (not_diagonal_epistemic_contradiction); on factual sentences informational consequence is classical (factual_classical). The dual necessity modal yields the same results (not_accepted_neg_must).

Implementation notes

The context coordinate is fixed throughout, so a sentence is a function of the index alone. Sentences form a Boolean algebra pointwise: negation is the complement φᶜ and conjunction the meet φ ⊓ ψ. The largest nonempty substate accepting the antecedent is characterized rather than constructed, and a conditional is true only if it exists. The probabilistic extension of the information parameter in the paper's seventh section is not modelled.

References

• [Yal07]
• [Kap89]
• [Vel96]
• [Ste07]

@[reducible, inline]

abbrev Yalcin2007.Sentence (W : Type u_2) : Type u_2

A sentence relative to a fixed context: truth at an index consisting of an information parameter, a set of worlds, and a world.

Equations

• Yalcin2007.Sentence W = (Set W → W → Prop)

def Yalcin2007.Sentence.ofProp {W : Type u_1} (p : Set W) : Sentence W

A nonepistemic sentence places a condition on the world alone.

Equations

• Yalcin2007.Sentence.ofProp p x✝ w = (w ∈ p)

def Yalcin2007.Sentence.might {W : Type u_1} (φ : Sentence W) : Sentence W

Epistemic possibility: existential quantification over the information parameter.

Equations

• φ.might s x✝ = ∃ w' ∈ s, φ s w'

def Yalcin2007.Sentence.must {W : Type u_1} (φ : Sentence W) : Sentence W

Epistemic necessity: universal quantification over the information parameter.

Equations

• φ.must s x✝ = ∀ w' ∈ s, φ s w'

def Yalcin2007.Sentence.AcceptedIn {W : Type u_1} (φ : Sentence W) (s : Set W) : Prop

A sentence is accepted in a state when it is true at every world of the state, relative to that state.

Equations

• φ.AcceptedIn s = ∀ w ∈ s, φ s w

theorem Yalcin2007.Sentence.might_might {W : Type u_1} (φ : Sentence W) : φ.might.might = φ.might

Iterating epistemic possibility adds nothing.

theorem Yalcin2007.Sentence.must_eq_compl_might_compl {W : Type u_1} (φ : Sentence W) : φ.must = φᶜ.mightᶜ

Necessity is the dual of possibility.

def Yalcin2007.contra {W : Type u_1} (p : Set W) : Sentence W

The epistemic contradiction not p and it might be that p.

Equations

• Yalcin2007.contra p = (Yalcin2007.Sentence.ofProp p)ᶜ ⊓ (Yalcin2007.Sentence.ofProp p).might

def Yalcin2007.contra' {W : Type u_1} (p : Set W) : Sentence W

The epistemic contradiction p and it might be that not p.

Equations

• Yalcin2007.contra' p = Yalcin2007.Sentence.ofProp p ⊓ (Yalcin2007.Sentence.ofProp p)ᶜ.might

theorem Yalcin2007.not_accepted_contra {W : Type u_1} {p s : Set W} (hs : s.Nonempty) : ¬(contra p).AcceptedIn s

No nonempty state accepts an epistemic contradiction.

theorem Yalcin2007.not_accepted_contra' {W : Type u_1} {p s : Set W} (hs : s.Nonempty) : ¬(contra' p).AcceptedIn s

Relational semantics

def Yalcin2007.relMight {W : Type u_1} (R : W → W → Prop) (p : Set W) : Set W

Epistemic possibility under an accessibility relation.

Equations

• Yalcin2007.relMight R p = {w : W | ∃ (w' : W), R w w' ∧ w' ∈ p}

theorem Yalcin2007.exists_relational_contra : ∃ (R : Bool → Bool → Prop) (p : Set Bool), ∃ w ∉ p, w ∈ relMight R p

A relational semantics makes an epistemic contradiction true at a world, so it cannot explain why the contradiction cannot be supposed.

Attitudes

def Yalcin2007.supposes {W : Type u_1} (S : W → Set W) (φ : Sentence W) : Sentence W

x supposes φ: φ holds at every world compatible with the supposition, relative to the state of supposition, which the verb makes the information parameter.

Equations

• Yalcin2007.supposes S φ x✝ w = ∀ w' ∈ S w, φ (S w) w'

theorem Yalcin2007.supposes_iff_accepted {W : Type u_1} {φ : Sentence W} {s : Set W} {w : W} {S : W → Set W} : supposes S φ s w ↔ φ.AcceptedIn (S w)

theorem Yalcin2007.supposes_might_iff {W : Type u_1} {φ : Sentence W} {s : Set W} {w : W} {S : W → Set W} (hne : (S w).Nonempty) : supposes S φ.might s w ↔ ∃ w' ∈ S w, φ (S w) w'

The universal quantifier of the attitude is trumped by an embedded possibility modal.

theorem Yalcin2007.supposes_might_iff_not_supposes_compl {W : Type u_1} {φ : Sentence W} {s : Set W} {w : W} {S : W → Set W} (hne : (S w).Nonempty) : supposes S φ.might s w ↔ ¬supposes S φᶜ s w

Attitude plus epistemic possibility is the attitude's dual.

theorem Yalcin2007.not_supposes_contra {W : Type u_1} {s : Set W} {w : W} {S : W → Set W} {p : Set W} (hne : (S w).Nonempty) : ¬supposes S (contra p) s w

No state of supposition satisfies an epistemic contradiction.

Indicative conditionals

def Yalcin2007.IsMaxAccepting {W : Type u_1} (s : Set W) (α : Sentence W) (s' : Set W) : Prop

s' is the largest nonempty substate of s accepting α.

Equations

• Yalcin2007.IsMaxAccepting s α s' = (s' ⊆ s ∧ s'.Nonempty ∧ α.AcceptedIn s' ∧ ∀ t ⊆ s, t.Nonempty → α.AcceptedIn t → t ⊆ s')

def Yalcin2007.ifThen {W : Type u_1} (α ψ : Sentence W) : Sentence W

The indicative conditional: the consequent holds throughout the largest nonempty substate accepting the antecedent, relative to that substate.

Equations

• Yalcin2007.ifThen α ψ s x✝ = ∃ (s' : Set W), Yalcin2007.IsMaxAccepting s α s' ∧ ψ.AcceptedIn s'

theorem Yalcin2007.isMaxAccepting_ofProp {W : Type u_1} {s : Set W} (p : Set W) (hne : (s ∩ p).Nonempty) : IsMaxAccepting s (Sentence.ofProp p) (s ∩ p)

For a factual antecedent the shifted state is the intersection, when nonempty.

theorem Yalcin2007.ifThen_contra_false {W : Type u_1} {ψ : Sentence W} {s : Set W} {w : W} {p : Set W} : ¬ifThen (contra p) ψ s w

A conditional whose antecedent is an epistemic contradiction is never true.

theorem Yalcin2007.ifThen_must_iff {W : Type u_1} {ψ : Sentence W} {s : Set W} {w : W} {α : Sentence W} : ifThen α ψ.must s w ↔ ifThen α ψ s w

The conditional with an epistemic necessity in its consequent is equivalent to the plain conditional: the necessity's quantification is trumped by the conditional's.

Consequence

def Yalcin2007.StandardConsequence {W : Type u_1} (Γ : List (Sentence W)) (φ : Sentence W) : Prop

Standard consequence preserves truth at every point.

Equations

• Yalcin2007.StandardConsequence Γ φ = ∀ (s : Set W) (w : W), (∀ γ ∈ Γ, γ s w) → φ s w

def Yalcin2007.DiagonalConsequence {W : Type u_1} (Γ : List (Sentence W)) (φ : Sentence W) : Prop

Diagonal consequence preserves truth at the diagonal points, those whose world lies in the information state.

Equations

• Yalcin2007.DiagonalConsequence Γ φ = ∀ (s : Set W), ∀ w ∈ s, (∀ γ ∈ Γ, γ s w) → φ s w

def Yalcin2007.InfoConsequence {W : Type u_1} (Γ : List (Sentence W)) (φ : Sentence W) : Prop

Informational consequence preserves acceptance.

Equations

• Yalcin2007.InfoConsequence Γ φ = ∀ (s : Set W), (∀ γ ∈ Γ, γ.AcceptedIn s) → φ.AcceptedIn s

def Yalcin2007.bot {W : Type u_1} : Sentence W

The absurd sentence.

Equations

• Yalcin2007.bot = Yalcin2007.Sentence.ofProp ∅

theorem Yalcin2007.DiagonalConsequence.of_standard {W : Type u_1} {φ : Sentence W} {Γ : List (Sentence W)} (h : StandardConsequence Γ φ) : DiagonalConsequence Γ φ

theorem Yalcin2007.lukasiewicz {W : Type u_1} (p : Set W) : InfoConsequence [(Sentence.ofProp p)ᶜ] (Sentence.ofProp p).mightᶜ

Łukasiewicz's principle: from not p, it is not possible that p.

theorem Yalcin2007.epistemic_contradiction {W : Type u_1} (p : Set W) : InfoConsequence [contra p] bot

Epistemic contradiction: not p and it might be that p is absurd.

theorem Yalcin2007.nonfactivity : ¬InfoConsequence [(Sentence.ofProp {true}).might] (Sentence.ofProp {true})

Nonfactivity: it might be that p does not yield p.

theorem Yalcin2007.not_diagonal_epistemic_contradiction : ¬DiagonalConsequence [contra {true}] bot

Diagonal consequence rejects epistemic contradiction: with more than one world epistemically possible at a context, a contradiction is true at its diagonal point.

theorem Yalcin2007.not_diagonal_factivity : ¬DiagonalConsequence [(Sentence.ofProp {true}).might] (Sentence.ofProp {true})

Diagonal consequence is nonfactive as well.

theorem Yalcin2007.factual_classical {W : Type u_1} (p q : Set W) : InfoConsequence [(Sentence.ofProp p)ᶜ ⊓ Sentence.ofProp q] bot ↔ InfoConsequence [Sentence.ofProp q] (Sentence.ofProp p)

On factual sentences informational consequence is classical: a conjunction with a negated sentence is absurd exactly when the other conjunct entails that sentence.

theorem Yalcin2007.not_classical : InfoConsequence [contra {true}] bot ∧ ¬InfoConsequence [(Sentence.ofProp {true}).might] (Sentence.ofProp {true})

Informational consequence is nonclassical: epistemic contradiction and nonfactivity, which no classical consequence relation admits together.

Epistemic necessity

theorem Yalcin2007.not_accepted_neg_must {W : Type u_1} {s p : Set W} (hs : s.Nonempty) : ¬((Sentence.ofProp p)ᶜ ⊓ (Sentence.ofProp p).must).AcceptedIn s

Not p and it must be that p is accepted by no nonempty state.