Rudin (2025): Asserting epistemic modals

This file formalizes the paper's Neo-Stalnakerian formalization of assertion. A speaker who asserts a sentence presents her epistemic state as one in which the sentence is known: the meta-intensionalization of a sentence is the set of states at all of whose worlds it is true relative to that very state (MI), an assertion proposes that the context be refined into that set in the most conservative way, and a hearer may reject it when no nonempty refinement of her own state lies in it (Compatible). For a sentence whose truth does not depend on the state the set is the downward closure of its proposition, so the update is the intersection of Stalnaker, the largest refinement in the set. For might under the simple quantificational semantics the set is the states that contain a prejacent world, so the update is the consistency test of Veltman, and rejection turns on the rejector's information while truth turns on the assertor's: the dissociation of truth from acceptance that Khoo observed (dissociation). Under the ordering semantics of Kratzer a state carries an ordering source, and asserting might adds the prejacent to it, a commensurate update whenever the base has a prejacent world (mightOrdUpdate_commensurate). The appendices' must and relational semantics are also formalized.

Implementation notes

Epistemic states are sets of worlds, and the ordering version pairs a base with a Kratzer ordering source, its best worlds being the minimal worlds of the base. Commensurativity is stated as the paper states it, membership of the update in the meta-intensionalized set on every compatible context; conservativity, quantified over sentences, is rendered for the simple version by the update being the largest refinement in the set. The commensurativity of the ordering update for might uses a finite frame, the paper's limit assumption. The ordering update for must adds the prejacent and drops the propositions disjoint from it; the paper argues on two three-world scenarios that both steps are needed, and both are formalized.

TODO

• The paper claims that after the must update every best world is a prejacent world, since an ordering proposition overlapping the prejacent favors its prejacent worlds. Two overlapping propositions can jointly leave a non-prejacent world best (overlapping_not_sufficient), so the must update is not commensurate in general.

References

• D. Rudin, Asserting epistemic modals (2025)
• R. C. Stalnaker, Assertion (1978)
• F. Veltman, Defaults in Update Semantics (1996)
• A. Kratzer, The Notional Category of Modality (1981)
• J. Khoo, Modal Disagreements (2015)
• S. Yalcin, Epistemic Modals (2007)

Meta-intensionalization

@[reducible, inline]

abbrev Rudin2025a.Denotation (W : Type u_2) : Type u_2

An information-sensitive denotation gives truth at a world relative to an epistemic state.

Equations

• Rudin2025a.Denotation W = (Set W → W → Prop)

def Rudin2025a.plain {W : Type u_1} (p : Set W) : Denotation W

A proposition is a sentence whose truth does not depend on the state.

Equations

• Rudin2025a.plain p x✝ w = (w ∈ p)

def Rudin2025a.might {W : Type u_1} (p : Set W) : Denotation W

Under the simple quantificational semantics might is true when some world of the state is a prejacent world.

Equations

• Rudin2025a.might p i x✝ = (i ∩ p).Nonempty

def Rudin2025a.must {W : Type u_1} (p : Set W) : Denotation W

Under the simple quantificational semantics must is true when every world of the state is a prejacent world.

Equations

• Rudin2025a.must p i x✝ = (i ⊆ p)

def Rudin2025a.MI {W : Type u_1} (s : Denotation W) : Set (Set W)

The meta-intensionalization of a sentence consists of the states in which the speaker knows it, those at all of whose worlds it is true relative to the state itself.

Equations

• Rudin2025a.MI s = {i : Set W | ∀ w ∈ i, s i w}

def Rudin2025a.Compatible {W : Type u_1} (s : Denotation W) (c : Set W) : Prop

A context is compatible with a sentence when some nonempty refinement, a subset, lies in the sentence's meta-intensionalization.

Equations

• Rudin2025a.Compatible s c = ∃ c' ⊆ c, c'.Nonempty ∧ c' ∈ Rudin2025a.MI s

def Rudin2025a.RejectionLicensed {W : Type u_1} (s : Denotation W) (i : Set W) : Prop

Rejection of an assertion is licensed when the rejector's state is not compatible with the sentence.

Equations

• Rudin2025a.RejectionLicensed s i = ¬Rudin2025a.Compatible s i

def Rudin2025a.Commensurate {W : Type u_1} (s : Denotation W) (f : Set W → Set W) : Prop

An update is commensurate with a sentence when it takes every compatible context into the sentence's meta-intensionalization.

Equations

• Rudin2025a.Commensurate s f = ∀ (c : Set W), Rudin2025a.Compatible s c → f c ∈ Rudin2025a.MI s

theorem Rudin2025a.MI_plain {W : Type u_1} (p : Set W) : MI (plain p) = {i : Set W | i ⊆ p}

The meta-intensionalization of a proposition is its downward closure.

theorem Rudin2025a.mem_MI_might {W : Type u_1} {p i : Set W} (hi : i.Nonempty) : i ∈ MI (might p) ↔ (i ∩ p).Nonempty

A nonempty state is in the meta-intensionalization of might exactly when it contains a prejacent world, since the outer quantifier is vacuous.

theorem Rudin2025a.MI_must {W : Type u_1} (p : Set W) : MI (must p) = MI (plain p)

The meta-intensionalization of must is that of its prejacent.

theorem Rudin2025a.compatible_plain {W : Type u_1} {p c : Set W} : Compatible (plain p) c ↔ (c ∩ p).Nonempty

A context is compatible with a proposition exactly when it has a world of it.

theorem Rudin2025a.compatible_might {W : Type u_1} {p c : Set W} : Compatible (might p) c ↔ (c ∩ p).Nonempty

A context is compatible with might exactly when it has a prejacent world.

theorem Rudin2025a.rejectionLicensed_plain {W : Type u_1} {p i : Set W} : RejectionLicensed (plain p) i ↔ i ∩ p = ∅

Rejecting a proposition presents the rejector as knowing it false.

theorem Rudin2025a.rejectionLicensed_plain_iff {W : Type u_1} {p i : Set W} : RejectionLicensed (plain p) i ↔ i ∈ MI (plain pᶜ)

The Stalnakerian biconditional between truth and acceptance holds for propositions, so a proposition may be rejected exactly when its negation is known.

theorem Rudin2025a.rejectionLicensed_might {W : Type u_1} {p i : Set W} : RejectionLicensed (might p) i ↔ i ∩ p = ∅

Rejecting might presents the rejector as having no prejacent world, whatever the assertor's state.

Update potentials

def Rudin2025a.plainUpdate {W : Type u_1} (p c : Set W) : Set W

The Stalnakerian update is intersection with the proposition.

Equations

• Rudin2025a.plainUpdate p c = c ∩ p

theorem Rudin2025a.plainUpdate_commensurate {W : Type u_1} (p : Set W) : Commensurate (plain p) (plainUpdate p)

theorem Rudin2025a.plainUpdate_greatest {W : Type u_1} {p c c' : Set W} (hc' : c' ⊆ c) (h : c' ∈ MI (plain p)) : c' ⊆ plainUpdate p c

Intersection is the most conservative commensurate update, since every refinement of the context in the meta-intensionalization lies inside it.

def Rudin2025a.mightUpdate {W : Type u_1} (p c : Set W) : Set W

The update of might returns the context itself when it has a prejacent world, and the absurd context otherwise.

Equations

• Rudin2025a.mightUpdate p c = {w : W | w ∈ c ∧ (c ∩ p).Nonempty}

theorem Rudin2025a.mightUpdate_of_nonempty {W : Type u_1} {p c : Set W} (h : (c ∩ p).Nonempty) : mightUpdate p c = c

The consistency test leaves a context with a prejacent world as it is.

theorem Rudin2025a.mightUpdate_of_empty {W : Type u_1} {p c : Set W} (h : c ∩ p = ∅) : mightUpdate p c = ∅

The consistency test makes a context without a prejacent world anomalous.

theorem Rudin2025a.mightUpdate_commensurate {W : Type u_1} (p : Set W) : Commensurate (might p) (mightUpdate p)

theorem Rudin2025a.mightUpdate_greatest {W : Type u_1} {p c c' : Set W} (hc' : c' ⊆ c) (hne : c'.Nonempty) (h : c' ∈ MI (might p)) : c' ⊆ mightUpdate p c

The test is the most conservative commensurate update, since every nonempty refinement of the context in the meta-intensionalization lies inside it.

theorem Rudin2025a.must_updates_as_plain {W : Type u_1} (p : Set W) : Commensurate (must p) (plainUpdate p)

must updates as its prejacent does.

theorem Rudin2025a.dissociation {W : Type u_1} {p a r : Set W} (ha : (a ∩ p).Nonempty) (hr : r ∩ p = ∅) : a ∈ MI (might p) ∧ RejectionLicensed (might p) r

Truth and acceptance come apart for might, since the assertor, with a prejacent world, knows the claim, while the rejector, with none, is licensed to reject it.

The ordering semantics

structure Rudin2025a.OrdState (W : Type u_2) : Type u_2

An epistemic state of the ordering version consists of a modal base and an ordering source.

• base : Set W
• ordering : Set (W → Prop)

def Rudin2025a.OrdState.best {W : Type u_1} (i : OrdState W) : Set W

The best worlds of a state are the worlds of the base that no other world of the base betters under the ordering source.

Equations

• i.best = (Modality.premisePreorder i.ordering).minimals i.base

@[reducible, inline]

abbrev Rudin2025a.OrdDenotation (W : Type u_2) : Type u_2

A denotation relative to a state with an ordering source.

Equations

• Rudin2025a.OrdDenotation W = (Rudin2025a.OrdState W → W → Prop)

def Rudin2025a.plainOrd {W : Type u_1} (p : Set W) : OrdDenotation W

A proposition.

Equations

• Rudin2025a.plainOrd p x✝ w = (w ∈ p)

def Rudin2025a.mightOrd {W : Type u_1} (p : Set W) : OrdDenotation W

Under the ordering semantics might is true when some best world is a prejacent world.

Equations

• Rudin2025a.mightOrd p i x✝ = (i.best ∩ p).Nonempty

def Rudin2025a.mustOrd {W : Type u_1} (p : Set W) : OrdDenotation W

Under the ordering semantics must is true when every best world is a prejacent world.

Equations

• Rudin2025a.mustOrd p i x✝ = (i.best ⊆ p)

def Rudin2025a.MIOrd {W : Type u_1} (s : OrdDenotation W) : Set (OrdState W)

Meta-intensionalization over the base of a state.

Equations

• Rudin2025a.MIOrd s = {i : Rudin2025a.OrdState W | ∀ w ∈ i.base, s i w}

def Rudin2025a.OrdState.Refines {W : Type u_1} (i' i : OrdState W) : Prop

A refinement shrinks the base; the ordering source may change freely.

Equations

• i'.Refines i = (i'.base ⊆ i.base)

def Rudin2025a.CompatibleOrd {W : Type u_1} (s : OrdDenotation W) (c : OrdState W) : Prop

Compatibility, with a nonempty base in place of a nonempty state.

Equations

• Rudin2025a.CompatibleOrd s c = ∃ (c' : Rudin2025a.OrdState W), c'.Refines c ∧ c'.base.Nonempty ∧ c' ∈ Rudin2025a.MIOrd s

def Rudin2025a.plainOrdUpdate {W : Type u_1} (p : Set W) (c : OrdState W) : OrdState W

A proposition still updates by intersection, the ordering source untouched.

Equations

• Rudin2025a.plainOrdUpdate p c = { base := c.base ∩ p, ordering := c.ordering }

theorem Rudin2025a.plainOrdUpdate_mem_MIOrd {W : Type u_1} (p : Set W) (c : OrdState W) : plainOrdUpdate p c ∈ MIOrd (plainOrd p)

noncomputable def Rudin2025a.mightOrdUpdate {W : Type u_1} (p : Set W) (c : OrdState W) : OrdState W

The update of might adds the prejacent to the ordering source when the base has a prejacent world, and otherwise empties the base.

Equations

• Rudin2025a.mightOrdUpdate p c = if (c.base ∩ p).Nonempty then { base := c.base, ordering := insert (fun (x : W) => x ∈ p) c.ordering } else { base := ∅, ordering := c.ordering }

theorem Rudin2025a.mightOrdUpdate_of_compatible {W : Type u_1} {p : Set W} {c : OrdState W} (h : (c.base ∩ p).Nonempty) : mightOrdUpdate p c = { base := c.base, ordering := insert (fun (x : W) => x ∈ p) c.ordering }

theorem Rudin2025a.mightOrdUpdate_commensurate {W : Type u_1} [Finite W] {p : Set W} {c : OrdState W} (h : (c.base ∩ p).Nonempty) : mightOrdUpdate p c ∈ MIOrd (mightOrd p)

Adding the prejacent to the ordering source is commensurate. With the prejacent among the ordering propositions only a prejacent world can better a prejacent world, so a prejacent world best among the prejacent worlds of the base is best in the base.

theorem Rudin2025a.compatibleOrd_might {W : Type u_1} {p : Set W} {c : OrdState W} : CompatibleOrd (mightOrd p) c ↔ (c.base ∩ p).Nonempty

Compatibility with might under the ordering semantics is again having a prejacent world in the base, since the refinement whose ordering source is the prejacent alone makes the prejacent worlds best.

theorem Rudin2025a.rejectionOrd_might {W : Type u_1} {p : Set W} {i : OrdState W} : ¬CompatibleOrd (mightOrd p) i ↔ i.base ∩ p = ∅

Rejection of might is licensed, as before, by the rejector's lack of a prejacent world.

must under the ordering semantics

noncomputable def Rudin2025a.mustOrdUpdate {W : Type u_1} (p : Set W) (c : OrdState W) : OrdState W

The update of must adds the prejacent to the ordering source and removes the propositions disjoint from it, when the base has a prejacent world.

Equations

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

theorem Rudin2025a.mustOrd_singleton {W : Type u_1} {p : Set W} {c : OrdState W} (h : (c.base ∩ p).Nonempty) : { base := c.base, ordering := {fun (x : W) => x ∈ p} } ∈ MIOrd (mustOrd p)

With the prejacent as the whole ordering source, the best worlds are the prejacent worlds of the base.

theorem Rudin2025a.compatibleOrd_must {W : Type u_1} [Finite W] {p : Set W} {c : OrdState W} : CompatibleOrd (mustOrd p) c ↔ (c.base ∩ p).Nonempty

Compatibility with must under the ordering semantics is having a prejacent world in the base, given a best world in every nonempty base.

def Rudin2025a.tacticDecide_states : Lean.ParserDescr

Decide a claim about a three-world state by unfolding the operators.

Equations

• Rudin2025a.tacticDecide_states = Lean.ParserDescr.node `Rudin2025a.tacticDecide_states 1024 (Lean.ParserDescr.nonReservedSymbol "decide_states" false)

theorem Rudin2025a.must_needs_prejacent : { base := Set.univ, ordering := ∅ } ∉ MIOrd (mustOrd {0, 1}) ∧ { base := Set.univ, ordering := {fun (x : Fin 3) => x ∈ {0, 1}} } ∈ MIOrd (mustOrd {0, 1})

In the paper's first scenario the ordering source is empty and every world of the base is best, so a context with a prejacent world is compatible with must yet not in its meta-intensionalization until the prejacent is added.

theorem Rudin2025a.must_needs_removal : { base := Set.univ, ordering := {fun (x : Fin 3) => x ∈ {0, 1}, fun (x : Fin 3) => x ∈ {2}} } ∉ MIOrd (mustOrd {0, 1})

In the paper's second scenario a proposition disjoint from the prejacent keeps a non-prejacent world best even after the prejacent is added, so it has to be removed.

theorem Rudin2025a.mustOrdUpdate_removal : mustOrdUpdate {0, 1} { base := Set.univ, ordering := {fun (x : Fin 3) => x ∈ {2}} } ∈ MIOrd (mustOrd {0, 1})

On the second scenario the must update removes the disjoint proposition and lands in the meta-intensionalization.

theorem Rudin2025a.overlapping_not_sufficient : ∃ (o : Set (Fin 3 → Prop)), (∀ q ∈ o, ∃ w ∈ {0, 1}, q w) ∧ { base := Set.univ, ordering := insert (fun (x : Fin 3) => x ∈ {0, 1}) o } ∉ MIOrd (mustOrd {0, 1})

Removing the disjoint propositions does not suffice, since two propositions that each overlap the prejacent can jointly keep a non-prejacent world best.

The relational semantics

def Rudin2025a.mightRel {W : Type u_1} (f : W → Set W) (p : Set W) (w : W) : Prop

might on an accessibility function.

Equations

• Rudin2025a.mightRel f p w = (f w ∩ p).Nonempty

def Rudin2025a.Closed {W : Type u_1} (f : W → Set W) (i : Set W) : Prop

Epistemic closure says that from every world of the state the whole state is accessible.

Equations

• Rudin2025a.Closed f i = ∀ w ∈ i, f w = i

theorem Rudin2025a.relational_might {W : Type u_1} {f : W → Set W} {p i : Set W} (hf : Closed f i) (hi : i.Nonempty) : (∀ w ∈ i, mightRel f p w) ↔ (i ∩ p).Nonempty

Under closure the relational might is known in a nonempty state exactly when the state has a prejacent world, as on the domain semantics.

theorem Rudin2025a.relational_must {W : Type u_1} {f : W → Set W} {p i : Set W} (hf : Closed f i) : (∀ w ∈ i, f w ⊆ p) ↔ i ⊆ p

Under closure the relational must is known exactly when the state lies in the prejacent.

theorem Rudin2025a.relational_ordering {W : Type u_1} {f : W → Set W} {g : W → Set (W → Prop)} {p : Set W} {i : OrdState W} (hf : Closed f i.base) (hg : ∀ w ∈ i.base, g w = i.ordering) (hi : i.base.Nonempty) : (∀ w ∈ i.base, ((Modality.premisePreorder (g w)).minimals (f w) ∩ p).Nonempty) ↔ i ∈ MIOrd (mightOrd p)

Under closure of the accessibility and ordering functions, the relational ordering might is known exactly when the domain version is.