Neo-Stalnakerian Formalization of Assertion

[Rud25a] [Sta78] [Vel96] [Kra81]

Rudin proposes that when a speaker asserts a sentence s, she predicates her epistemic state: she presents herself as though she knows s, and proposes the context be updated to reflect that knowledge. This is formalized via the meta-intensionalization function MI, which maps s to the set of epistemic states compatible with knowing s.

Applied uniformly to all declaratives, this single mechanism derives:

1. Standard Stalnakerian intersective update for non-epistemic sentences (§4.1)
2. [Vel96]'s consistency-test semantics for epistemic might (§4.2)
3. A novel ordering-source update for might on [Kra81] semantics (§5)

The key insight: epistemic modals get nonstandard updates not because they have special update semantics, but because they are speaker-orientedly epistemic in the same way that assertion is.

Following the Bool→Prop migration: predicates on worlds are W → Prop (mathlib-native), and list operations that depend on decidability of predicates carry [DecidablePred p] constraints.

@[reducible, inline]

abbrev Rudin2025.World : Type

Equations

• Rudin2025.World = Fin 4

def Rudin2025.allWorlds : List World

Equations

• Rudin2025.allWorlds = [0, 1, 2, 3]

Part 1: Core Types

@[reducible, inline]

abbrev Rudin2025.InfoSensDen (W : Type u_2) : Type u_2

Information-sensitive denotation: ⟦s⟧ⁱ(w). Truth value may depend on the epistemic state i.

Equations

• Rudin2025.InfoSensDen W = (List W → W → Prop)

def Rudin2025.liftProp {W : Type u_1} (p : W → Prop) : InfoSensDen W

Lift a plain proposition to an information-insensitive denotation. For sentences like "John is dead" whose truth doesn't vary with i.

Equations

• Rudin2025.liftProp p x✝ = p

def Rudin2025.mightSimple {W : Type u_1} (p : W → Prop) : InfoSensDen W

Simple quantificational semantics for epistemic might: ⟦might-p⟧ⁱ(w) = true iff ∃w' ∈ i, p(w') = true. Truth is insensitive to the evaluation world w.

eq. (25); adapted from [Yal07].

Equations

• Rudin2025.mightSimple p i x✝ = ∃ w ∈ i, p w

def Rudin2025.mustSimple {W : Type u_1} (p : W → Prop) : InfoSensDen W

Simple quantificational semantics for epistemic must: ⟦must-p⟧ⁱ(w) = true iff ∀w' ∈ i, p(w') = true.

Appendix A, eq. (57).

Equations

• Rudin2025.mustSimple p i x✝ = ∀ w ∈ i, p w

Part 2: Meta-Intensionalization

def Rudin2025.MI {W : Type u_1} (sem : InfoSensDen W) (i : List W) : Prop

Meta-intensionalization: the set of epistemic states the speaker could hold if she knows s to be true.

MI(s) = { i : ∀w ∈ i, ⟦s⟧ⁱ(w) = 1 }

When a speaker asserts s, she presents herself as though her epistemic state is a member of MI(s).

Definition (10).

Equations

• Rudin2025.MI sem i = ∀ w ∈ i, sem i w

def Rudin2025.refines {W : Type u_1} (i' i : List W) : Prop

Refinement: i' refines i iff i' ⊆ i. Removing worlds monotonically increases information.

Definition (13).

Equations

• Rudin2025.refines i' i = ∀ w ∈ i', w ∈ i

def Rudin2025.sCompatible {W : Type u_1} (sem : InfoSensDen W) (c : List W) : Prop

A context c is s-compatible iff some non-empty refinement is in MI(s).

Definition (18).

Equations

• Rudin2025.sCompatible sem c = ∃ (c' : List W), Rudin2025.refines c' c ∧ Rudin2025.MI sem c' ∧ c' ≠ []

def Rudin2025.rejectionLicensed {W : Type u_1} (sem : InfoSensDen W) (i_rejector : List W) : Prop

Rejection of s is licensed when the rejector's state is not s-compatible.

Definition (20).

Equations

• Rudin2025.rejectionLicensed sem i_rejector = ¬Rudin2025.sCompatible sem i_rejector

Part 3: MI Characterization Theorems

theorem Rudin2025.MI_liftProp {W : Type u_1} (p : W → Prop) (i : List W) : MI (liftProp p) i ↔ ∀ w ∈ i, p w

MI for non-epistemic sentences: i ∈ MI(p) iff every world in i satisfies p. Equivalently, i ⊆ ext(p) — the downward closure of the proposition's extension.

eqs. (22)–(23).

theorem Rudin2025.MI_mightSimple {W : Type u_1} (p : W → Prop) (i : List W) (hi : i ≠ []) : MI (mightSimple p) i ↔ ∃ w ∈ i, p w

MI for might-p (non-empty states): i ∈ MI(might-p) iff i has a p-world. The universal quantifier in MI collapses because might's truth conditions are insensitive to the evaluation world.

eq. (27b): MI(might-p) = { i : i ∩ p ≠ ∅ }.

theorem Rudin2025.MI_mustSimple {W : Type u_1} (p : W → Prop) (i : List W) (hi : i ≠ []) : MI (mustSimple p) i ↔ ∀ w ∈ i, p w

MI for must-p coincides with MI for the bare prejacent. Since must universally quantifies over the same set i that MI quantifies over, the two collapse: MI(must-p) = { i : i ⊆ p }.

Appendix A, eq. (58).

theorem Rudin2025.MI_must_eq_MI_lift {W : Type u_1} (p : W → Prop) (i : List W) (hi : i ≠ []) : MI (mustSimple p) i ↔ MI (liftProp p) i

MI(must-p) = MI(p): must has the same meta-intensionalized denotation as a non-epistemic assertion of its prejacent.

Part 4: Derived Update Potentials

def Rudin2025.nsfUpdateNonEpistemic {W : Type u_1} (p : W → Prop) [DecidablePred p] (c : List W) : List W

NSF update for non-epistemic sentences: intersect with proposition. The most conservative refinement of c that lands in MI(liftProp p).

eq. (24).

Equations

• Rudin2025.nsfUpdateNonEpistemic p c = List.filter (fun (b : W) => decide (p b)) c

def Rudin2025.nsfUpdateMight {W : Type u_1} (p : W → Prop) [DecidablePred p] (c : List W) : List W

NSF update for might-p (simple semantics): consistency test. Leave context unchanged if c has p-worlds; anomaly otherwise.

eq. (29).

Equations

• Rudin2025.nsfUpdateMight p c = if (c.any fun (w : W) => decide (p w)) = true then c else []

def Rudin2025.nsfUpdateMust {W : Type u_1} (p : W → Prop) [DecidablePred p] (c : List W) : List W

NSF update for must-p (simple semantics): same as non-epistemic.

Appendix A, eq. (59).

Equations

• Rudin2025.nsfUpdateMust p c = List.filter (fun (b : W) => decide (p b)) c

Part 5: Derivation Theorems

theorem Rudin2025.context_in_MI_might {W : Type u_1} (p : W → Prop) (c : List W) (h : ∃ w ∈ c, p w) : MI (mightSimple p) c

If c has p-worlds, it is already in MI(might-p). No refinement needed.

theorem Rudin2025.no_p_worlds_not_compatible {W : Type u_1} (p : W → Prop) (c : List W) (h : ¬∃ w ∈ c, p w) : ¬sCompatible (mightSimple p) c

Core lemma: subset refinement cannot introduce p-worlds. If c has no p-worlds, no refinement of c does either, making c not-might-p-compatible. This forces anomalous update.

This is the key step in deriving Veltman's test semantics from the NSF: the "consistency test" behavior of might falls out of the monotonicity of refinement.

theorem Rudin2025.nsfUpdateMight_spec {W : Type u_1} (p : W → Prop) [DecidablePred p] (c : List W) : nsfUpdateMight p c = if (c.any fun (w : W) => decide (p w)) = true then c else []

NSF derives Veltman's consistency test.

Given solipsistic contextualist truth conditions for might and the NSF's assertive machinery, the update potential for might-p is:

• c[might-p] = c if c ∩ p ≠ ∅ (test passes)
• c[might-p] = ∅ if c ∩ p = ∅ (anomaly)

This is exactly [Vel96], derived rather than stipulated. The derivation uses context_in_MI_might (compatible case) and no_p_worlds_not_compatible (incompatible case).

Bridges nsfUpdateMight to Update.might from UpdateSemantics.

§4.2; cf. [Vel96], [Yal07].

theorem Rudin2025.nsfUpdateMust_eq_nonEpistemic {W : Type u_1} (p : W → Prop) [DecidablePred p] (c : List W) : nsfUpdateMust p c = nsfUpdateNonEpistemic p c

NSF update for must-p equals update for its prejacent. Must-p updates identically to a non-epistemic assertion of p.

Appendix A, eq. (59).

theorem Rudin2025.nsf_recovers_stalnaker {W : Type u_1} (p : W → Prop) [DecidablePred p] (c : List W) (w : W) : w ∈ nsfUpdateNonEpistemic p c ↔ w ∈ c ∧ p w

NSF recovers Stalnaker for non-epistemic sentences.

For sentences whose denotation doesn't vary with the information parameter, the NSF update is intersection with the proposition — exactly [Sta78]'s original formalization.

Bridges nsfUpdateNonEpistemic to ContextSet.update from CommonGround: both compute c ∩ p (filter c to p-worlds).

Part 6: Rejection Licensing

theorem Rudin2025.rejection_nonEpistemic {W : Type u_1} (p : W → Prop) (i : List W) : i ≠ [] → (rejectionLicensed (liftProp p) i ↔ ∀ w ∈ i, ¬p w)

Rejection of a non-epistemic assertion of p is licensed iff the rejector has no p-worlds — i.e., the rejector knows ¬p.

theorem Rudin2025.rejection_mightSimple {W : Type u_1} (p : W → Prop) (i : List W) : rejectionLicensed (mightSimple p) i ↔ ¬sCompatible (mightSimple p) i

Rejection of might-p is licensed iff the rejector has no p-worlds. Crucially, this depends on the rejector's information, not the assertor's. The assertor's might-claim can be true (she has p-worlds) while the rejector is licensed to reject (he has none).

This predicts [Kho15]'s finding that might-claims can be simultaneously not-judged-false and rejected.

§4.2.1.

theorem Rudin2025.rejection_might_iff_no_p_worlds {W : Type u_1} (p : W → Prop) (i : List W) (hi : ¬∃ w ∈ i, p w) : rejectionLicensed (mightSimple p) i

Rejection of might-p reduces to having no p-worlds.

Part 7: Ordering Semantics (Kratzer bridge)

structure Rudin2025.OrdEpistemicState : Type

Epistemic state (ordering version): a modal base (set of worlds) paired with an ordering source (set of propositions ranking those worlds).

Definition (43): D_i = { ⟨b_i, o_i⟩ : b_i ∈ D_st ∧ o_i ∈ ℘D_st }

• base : List World

  Modal base: the set of epistemically accessible worlds

• ordering : List (World → Prop)

  Ordering source: propositions ranking accessible worlds

def Rudin2025.OrdEpistemicState.notDominated (s : OrdEpistemicState) (w : World) : Prop

Predicate: world w is not strictly dominated in s (i.e., there is no w' in the base that beats w strictly under the ordering).

Equations

• s.notDominated w = ¬∃ w' ∈ s.base, (w' ≤[s.ordering] w) ∧ ¬w ≤[s.ordering] w'

theorem Rudin2025.OrdEpistemicState.mem_bestWorlds_iff (s : OrdEpistemicState) (w : World) : w ∈ s.base ∧ s.notDominated w ↔ w ∈ s.base ∧ ¬∃ w' ∈ s.base, (w' ≤[s.ordering] w) ∧ ¬w ≤[s.ordering] w'

Membership in bestWorlds unfolds to base ∧ notDominated.

noncomputable def Rudin2025.OrdEpistemicState.bestWorlds (s : OrdEpistemicState) : List World

BEST worlds: worlds in the modal base not strictly dominated by any other. A world w is strictly dominated by w' iff w' satisfies a proper superset of the ordering propositions that w satisfies.

eq. (44); [Kra81].

Equations

• s.bestWorlds = List.filter (fun (b : Rudin2025.World) => decide (s.notDominated b)) s.base

theorem Rudin2025.OrdEpistemicState.mem_bestWorlds (s : OrdEpistemicState) (w : World) : w ∈ s.bestWorlds ↔ w ∈ s.base ∧ s.notDominated w

def Rudin2025.mightOrdering (p : World → Prop) (s : OrdEpistemicState) : World → Prop

Ordering semantics for might: ⟦might-p⟧ⁱ(w) = true iff ∃w' ∈ BEST_{b_i,o_i}, p(w') = true.

eq. (45).

Equations

• Rudin2025.mightOrdering p s x✝ = ∃ w ∈ s.bestWorlds, p w

def Rudin2025.MI_ord (p : World → Prop) (s : OrdEpistemicState) : Prop

MI for ordering-semantic might-p: the set of epistemic states whose BEST worlds include at least one p-world.

eq. (54b).

Equations

• Rudin2025.MI_ord p s = ∃ w ∈ s.bestWorlds, p w

def Rudin2025.OrdEpistemicState.refines (c' c : OrdEpistemicState) : Prop

Refinement (ordering version): only the modal base is refined.

Definition (46).

Equations

• c'.refines c = ∀ w ∈ c'.base, w ∈ c.base

def Rudin2025.nsfUpdateMightOrd (p : World → Prop) [DecidablePred p] (c : OrdEpistemicState) : OrdEpistemicState

NSF update for might-p (ordering semantics): add p to ordering source.

This is the paper's most novel result. Asserting might-p proposes that the prejacent be added as a "live possibility" — a proposition in the ordering source. This makes p-worlds more likely to be among the BEST worlds, yielding an informative (non-trivial) update.

eq. (56).

Equations

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

theorem Rudin2025.nonPWorld_cannot_dominate_pWorld (A : List (World → Prop)) (p : World → Prop) (w z : World) (hw : p w) (hz : ¬p z) : ¬z ≤[p :: A] w

Adding p to the ordering source cannot make a p-world dominated by a non-p-world, because the non-p-world fails to satisfy p while the p-world satisfies it.

This is the key step in proving the ordering update is commensurate.

theorem Rudin2025.ordering_update_commensurate (c : OrdEpistemicState) (p : World → Prop) [DecidablePred p] (hCompat : ∃ w ∈ c.base, p w) : MI_ord p (nsfUpdateMightOrd p c)

Commensurativity: if the modal base has a p-world, adding p to the ordering source yields a state whose BEST worlds include a p-world.

After adding p, no non-p-world can dominate any p-world (nonPWorld_cannot_dominate_pWorld). Among p-worlds, the element with maximum satisfaction count is maximal. Since the base has p-worlds, BEST_{b, A+p} ∩ p ≠ ∅.

§5.3, pp. 77–78.

theorem Rudin2025.ordering_update_conservative (c : OrdEpistemicState) (p : World → Prop) [DecidablePred p] (hCompat : ∃ w ∈ c.base, p w) : (nsfUpdateMightOrd p c).base = c.base

The ordering update is conservative: adding p to the ordering source does not guarantee that the resulting context will entail anything not already entailed by might-p.

§5.3.

theorem Rudin2025.ordering_nonEpistemic_preserves_ordering (c : OrdEpistemicState) (p : World → Prop) [DecidablePred p] : have c' := { base := List.filter (fun (b : World) => decide (p b)) c.base, ordering := c.ordering }; c'.ordering = c.ordering

Non-epistemic sentences still get standard intersective update in the ordering version: the ordering source is unchanged.

eq. (52).

Appendix A2: Must on ordering semantics

def Rudin2025.mustOrdering (p : World → Prop) (s : OrdEpistemicState) : World → Prop

Ordering semantics for must: ⟦must-p⟧ⁱ(w) = true iff ∀w' ∈ BEST_{b_i,o_i}, p(w') = true.

eq. (60).

Equations

• Rudin2025.mustOrdering p s x✝ = ∀ w ∈ s.bestWorlds, p w

def Rudin2025.MI_ord_must (p : World → Prop) (s : OrdEpistemicState) : Prop

MI for ordering-semantic must-p: the set of epistemic states whose BEST worlds are all p-worlds.

eq. (61).

Equations

• Rudin2025.MI_ord_must p s = ∀ w ∈ s.bestWorlds, p w

theorem Rudin2025.MI_ord_must_iff (p : World → Prop) (s : OrdEpistemicState) : MI_ord_must p s ↔ ∀ w ∈ s.bestWorlds, p w

MI(must-p) on ordering semantics ↔ BEST ⊆ p.

def Rudin2025.pDisjoint (p q : World → Prop) (base : List World) : Prop

A proposition is p-disjoint iff no world in the base satisfies both it and p.

Equations

• Rudin2025.pDisjoint p q base = ∀ w ∈ base, ¬(p w ∧ q w)

noncomputable def Rudin2025.nsfUpdateMustOrd (p : World → Prop) [DecidablePred p] (c : OrdEpistemicState) : OrdEpistemicState

NSF update for must-p (ordering semantics).

Add p to the ordering source AND remove all p-disjoint propositions. Simply adding p is insufficient: p-disjoint ordering propositions can keep non-p-worlds in BEST. Removing them ensures all BEST worlds satisfy p.

eq. (64).

Equations

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

theorem Rudin2025.nsfUpdateMustOrd_preserves_base (c : OrdEpistemicState) (p : World → Prop) [DecidablePred p] (hCompat : ∃ w ∈ c.base, p w) : (nsfUpdateMustOrd p c).base = c.base

The must ordering update preserves the modal base (when compatible).

Part 8: Relational Semantics Equivalence (Appendix B)

def Rudin2025.mightRelational (f : World → List World) (p : World → Prop) (w : World) : Prop

Relational semantics for might: ⟦might-p⟧ⁱ(w) = true iff ∃w' ∈ f_i(w), p(w') = true, where f_i is the epistemic accessibility function determined by i.

eq. (65).

Equations

• Rudin2025.mightRelational f p w = ∃ w' ∈ f w, p w'

def Rudin2025.EpistemicClosure (f : World → List World) (i : List World) : Prop

Epistemic closure: f maps every world in i to i itself. Under solipsistic contextualism, the accessibility function for the speaker's epistemic state maps each accessible world to the full epistemic state.

eq. (67).

Equations

• Rudin2025.EpistemicClosure f i = ∀ w ∈ i, f w = i

theorem Rudin2025.MI_relational_might_eq_domain (f : World → List World) (i : List World) (p : World → Prop) (hClosed : EpistemicClosure f i) (hi : i ≠ []) : (∀ w ∈ i, mightRelational f p w) ↔ ∃ w ∈ i, p w

Under epistemic closure, MI(might-p) on relational semantics is { i : i ∩ p ≠ ∅ } — identical to the domain semantics result.

Proof follows eq. (69a–c):

• If i ∩ p ≠ ∅, then for any w ∈ i, f(w) = i has p-worlds ✓
• If i ∩ p = ∅, then for any w ∈ i, f(w) = i has no p-worlds ✗

Appendix B1, eq. (69c).

def Rudin2025.mustRelational (f : World → List World) (p : World → Prop) (w : World) : Prop

Must on relational semantics: ⟦must-p⟧ⁱ(w) = ∀w' ∈ f_i(w), p(w').

Equations

• Rudin2025.mustRelational f p w = ∀ w' ∈ f w, p w'

theorem Rudin2025.MI_relational_must_eq_domain (f : World → List World) (i : List World) (p : World → Prop) (hClosed : EpistemicClosure f i) (_hi : i ≠ []) : (∀ w ∈ i, mustRelational f p w) ↔ ∀ w ∈ i, p w

Under epistemic closure, MI(must-p) on relational semantics is { i : i ⊆ p } — identical to the domain semantics result.

Appendix B1 (analogous to eq. 69).

B2: Relational ordering semantics

def Rudin2025.mightRelOrd (f : World → List World) (g : World → List (World → Prop)) (p : World → Prop) (w : World) : Prop

Relational ordering semantics for might: ⟦might-p⟧ⁱ(w) = true iff ∃w' ∈ BEST_{f_i(w), g_i(w)}, p(w') = true, where g_i maps worlds to ordering sources.

eq. (70).

Equations

• Rudin2025.mightRelOrd f g p w = ∃ w' ∈ { base := f w, ordering := g w }.bestWorlds, p w'

def Rudin2025.OrderingClosure (g : World → List (World → Prop)) (base : List World) (ordering : List (World → Prop)) : Prop

Ordering closure: g maps every world in b_i to the same ordering o_i.

eq. (71).

Equations

• Rudin2025.OrderingClosure g base ordering = ∀ w ∈ base, g w = ordering

theorem Rudin2025.MI_relOrd_might_eq_domain (f : World → List World) (g : World → List (World → Prop)) (i : OrdEpistemicState) (p : World → Prop) (hfClosed : EpistemicClosure f i.base) (hgClosed : OrderingClosure g i.base i.ordering) (hi : i.base ≠ []) : (∀ w ∈ i.base, mightRelOrd f g p w) ↔ MI_ord p i

Under both epistemic and ordering closure, MI(might-p) on the relational ordering semantics equals { i : BEST_{b_i,o_i} has p-world } — identical to the domain ordering result.

Appendix B2, eq. (73).

Part 9: Truth ≠ Acceptance

theorem Rudin2025.nonEpistemic_truth_acceptance_biconditional {W : Type u_1} (p : W → Prop) (c_assertor c_rejector : List W) (_h_rej_ne : c_rejector ≠ []) (_h_assertor_true : MI (liftProp p) c_assertor) (h_rejector_false : ∀ w ∈ c_rejector, ¬p w) : rejectionLicensed (liftProp p) c_rejector

For non-epistemic sentences, truth and rejectability align: if the sentence is false in the rejector's state, rejection is licensed; if true, rejection is not licensed.

This is the standard biconditional relationship.

theorem Rudin2025.might_truth_acceptance_dissociate {W : Type u_1} (p : W → Prop) (c_assertor c_rejector : List W) (h_assertor_has_p : ∃ w ∈ c_assertor, p w) (h_rejector_no_p : ¬∃ w ∈ c_rejector, p w) : MI (mightSimple p) c_assertor ∧ rejectionLicensed (mightSimple p) c_rejector

For might-claims, truth and rejectability dissociate.

The assertor's might-claim can be true (she has p-worlds in her epistemic state) while the rejector is simultaneously licensed to reject (he has no p-worlds in his). This is because:

• Truth depends on the assertor's information parameter
• Rejection depends on the rejector's information parameter
• These are different parameters that can diverge

This predicts the empirical pattern in [Kho15]: participants reject might-claims (mean Likert rejection ~5.03) without judging them false (mean Likert falsity ~2.42).

§4.3, bridging §4.2.1.