Neo-Stalnakerian Formalization of Assertion

@cite{rudin-2025} @cite{stalnaker-1978} @cite{veltman-1996} @cite{kratzer-1981}

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. @cite{veltman-1996}'s consistency-test semantics for epistemic might (§4.2)
3. A novel ordering-source update for might on @cite{kratzer-1981} 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.

Part 1: Core Types

@[reducible, inline]

abbrev Semantics.Dynamic.NeoStalnakerian.InfoSensDen (W : Type u_2) : Type u_2

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

Equations

• Semantics.Dynamic.NeoStalnakerian.InfoSensDen W = (List W → BProp W)

def Semantics.Dynamic.NeoStalnakerian.liftProp {W : Type u_1} (p : BProp W) : 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

• Semantics.Dynamic.NeoStalnakerian.liftProp p x✝ = p

def Semantics.Dynamic.NeoStalnakerian.mightSimple {W : Type u_1} (p : BProp W) : 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 @cite{yalcin-2007}.

Equations

• Semantics.Dynamic.NeoStalnakerian.mightSimple p i x✝ = i.any p

def Semantics.Dynamic.NeoStalnakerian.mustSimple {W : Type u_1} (p : BProp W) : InfoSensDen W

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

Appendix A, eq. (57).

Equations

• Semantics.Dynamic.NeoStalnakerian.mustSimple p i x✝ = i.all p

Part 2: Meta-Intensionalization

def Semantics.Dynamic.NeoStalnakerian.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

• Semantics.Dynamic.NeoStalnakerian.MI sem i = ∀ w ∈ i, sem i w = true

def Semantics.Dynamic.NeoStalnakerian.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

• Semantics.Dynamic.NeoStalnakerian.refines i' i = ∀ w ∈ i', w ∈ i

def Semantics.Dynamic.NeoStalnakerian.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

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

def Semantics.Dynamic.NeoStalnakerian.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

• Semantics.Dynamic.NeoStalnakerian.rejectionLicensed sem i_rejector = ¬Semantics.Dynamic.NeoStalnakerian.sCompatible sem i_rejector

Part 3: MI Characterization Theorems

theorem Semantics.Dynamic.NeoStalnakerian.MI_liftProp {W : Type u_1} (p : BProp W) (i : List W) : MI (liftProp p) i ↔ ∀ w ∈ i, p w = true

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 Semantics.Dynamic.NeoStalnakerian.MI_mightSimple {W : Type u_1} (p : BProp W) (i : List W) (hi : i ≠ []) : MI (mightSimple p) i ↔ i.any p = true

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 Semantics.Dynamic.NeoStalnakerian.MI_mustSimple {W : Type u_1} (p : BProp W) (i : List W) (hi : i ≠ []) : MI (mustSimple p) i ↔ ∀ w ∈ i, p w = true

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 Semantics.Dynamic.NeoStalnakerian.MI_must_eq_MI_lift {W : Type u_1} (p : BProp W) (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 Semantics.Dynamic.NeoStalnakerian.nsfUpdateNonEpistemic {W : Type u_1} (p : BProp W) (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

• Semantics.Dynamic.NeoStalnakerian.nsfUpdateNonEpistemic p c = List.filter p c

def Semantics.Dynamic.NeoStalnakerian.nsfUpdateMight {W : Type u_1} (p : BProp W) (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

• Semantics.Dynamic.NeoStalnakerian.nsfUpdateMight p c = if c.any p = true then c else []

def Semantics.Dynamic.NeoStalnakerian.nsfUpdateMust {W : Type u_1} (p : BProp W) (c : List W) : List W

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

Appendix A, eq. (59).

Equations

• Semantics.Dynamic.NeoStalnakerian.nsfUpdateMust p c = List.filter p c

Part 5: Derivation Theorems

theorem Semantics.Dynamic.NeoStalnakerian.context_in_MI_might {W : Type u_1} (p : BProp W) (c : List W) (h : c.any p = true) : MI (mightSimple p) c

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

theorem Semantics.Dynamic.NeoStalnakerian.no_p_worlds_not_compatible {W : Type u_1} (p : BProp W) (c : List W) (h : c.any p = false) : ¬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 Semantics.Dynamic.NeoStalnakerian.nsfUpdateMight_spec {W : Type u_1} (p : BProp W) (c : List W) : nsfUpdateMight p c = if c.any p = 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 @cite{veltman-1996}, 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. @cite{veltman-1996}, @cite{yalcin-2007}.

theorem Semantics.Dynamic.NeoStalnakerian.nsfUpdateMust_eq_nonEpistemic {W : Type u_1} (p : BProp W) (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 Semantics.Dynamic.NeoStalnakerian.nsf_recovers_stalnaker {W : Type u_1} (p : BProp W) (c : List W) (w : W) : w ∈ nsfUpdateNonEpistemic p c ↔ w ∈ c ∧ p w = true

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 @cite{stalnaker-1978}'s original formalization.

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

Part 6: Rejection Licensing

theorem Semantics.Dynamic.NeoStalnakerian.rejection_nonEpistemic {W : Type u_1} (p : BProp W) (i : List W) : i ≠ [] → (rejectionLicensed (liftProp p) i ↔ ∀ w ∈ i, p w = false)

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

theorem Semantics.Dynamic.NeoStalnakerian.rejection_mightSimple {W : Type u_1} (p : BProp W) (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 @cite{khoo-2015}'s finding that might-claims can be simultaneously not-judged-false and rejected.

§4.2.1.

theorem Semantics.Dynamic.NeoStalnakerian.rejection_might_iff_no_p_worlds {W : Type u_1} (p : BProp W) (i : List W) (hi : i.any p = false) : rejectionLicensed (mightSimple p) i

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

Part 7: Ordering Semantics (Kratzer bridge)

structure Semantics.Dynamic.NeoStalnakerian.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 Attitudes.Intensional.World

  Modal base: the set of epistemically accessible worlds

• ordering : List (BProp Attitudes.Intensional.World)

  Ordering source: propositions ranking accessible worlds

def Semantics.Dynamic.NeoStalnakerian.OrdEpistemicState.bestWorlds (s : OrdEpistemicState) : List Attitudes.Intensional.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); @cite{kratzer-1981}.

Equations

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

def Semantics.Dynamic.NeoStalnakerian.mightOrdering (p : BProp Attitudes.Intensional.World) (s : OrdEpistemicState) : Attitudes.Intensional.World → Bool

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

eq. (45).

Equations

• Semantics.Dynamic.NeoStalnakerian.mightOrdering p s x✝ = s.bestWorlds.any p

def Semantics.Dynamic.NeoStalnakerian.MI_ord (p : BProp Attitudes.Intensional.World) (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

• Semantics.Dynamic.NeoStalnakerian.MI_ord p s = (s.bestWorlds.any p = true)

def Semantics.Dynamic.NeoStalnakerian.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 Semantics.Dynamic.NeoStalnakerian.nsfUpdateMightOrd (p : BProp Attitudes.Intensional.World) (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

• Semantics.Dynamic.NeoStalnakerian.nsfUpdateMightOrd p c = if (List.filter p c.base).isEmpty = true then { base := [], ordering := c.ordering } else { base := c.base, ordering := p :: c.ordering }

theorem Semantics.Dynamic.NeoStalnakerian.nonPWorld_cannot_dominate_pWorld (A : List (BProp Attitudes.Intensional.World)) (p : BProp Attitudes.Intensional.World) (w z : Attitudes.Intensional.World) (hw : p w = true) (hz : p z = false) : (z ≤[p :: A] w) = false

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 Semantics.Dynamic.NeoStalnakerian.ordering_update_commensurate (c : OrdEpistemicState) (p : BProp Attitudes.Intensional.World) (hCompat : c.base.any p = true) : 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 Semantics.Dynamic.NeoStalnakerian.ordering_update_conservative (c : OrdEpistemicState) (p : BProp Attitudes.Intensional.World) (hCompat : c.base.any p = true) : (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 Semantics.Dynamic.NeoStalnakerian.ordering_nonEpistemic_preserves_ordering (c : OrdEpistemicState) (p : BProp Attitudes.Intensional.World) : have c' := { base := List.filter p 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 Semantics.Dynamic.NeoStalnakerian.mustOrdering (p : BProp Attitudes.Intensional.World) (s : OrdEpistemicState) : Attitudes.Intensional.World → Bool

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

eq. (60).

Equations

• Semantics.Dynamic.NeoStalnakerian.mustOrdering p s x✝ = s.bestWorlds.all p

def Semantics.Dynamic.NeoStalnakerian.MI_ord_must (p : BProp Attitudes.Intensional.World) (s : OrdEpistemicState) : Prop

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

eq. (61).

Equations

• Semantics.Dynamic.NeoStalnakerian.MI_ord_must p s = ∀ w ∈ s.bestWorlds, p w = true

theorem Semantics.Dynamic.NeoStalnakerian.MI_ord_must_iff (p : BProp Attitudes.Intensional.World) (s : OrdEpistemicState) : MI_ord_must p s ↔ s.bestWorlds.all p = true

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

def Semantics.Dynamic.NeoStalnakerian.pDisjoint (p q : BProp Attitudes.Intensional.World) (base : List Attitudes.Intensional.World) : Bool

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

Equations

• Semantics.Dynamic.NeoStalnakerian.pDisjoint p q base = base.all fun (w : Semantics.Attitudes.Intensional.World) => !(p w && q w)

def Semantics.Dynamic.NeoStalnakerian.nsfUpdateMustOrd (p : BProp Attitudes.Intensional.World) (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 Semantics.Dynamic.NeoStalnakerian.nsfUpdateMustOrd_preserves_base (c : OrdEpistemicState) (p : BProp Attitudes.Intensional.World) (hCompat : c.base.any p = true) : (nsfUpdateMustOrd p c).base = c.base

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

Part 8: Relational Semantics Equivalence (Appendix B)

def Semantics.Dynamic.NeoStalnakerian.mightRelational (f : Attitudes.Intensional.World → List Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

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

• Semantics.Dynamic.NeoStalnakerian.mightRelational f p w = (f w).any p

def Semantics.Dynamic.NeoStalnakerian.EpistemicClosure (f : Attitudes.Intensional.World → List Attitudes.Intensional.World) (i : List Attitudes.Intensional.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

• Semantics.Dynamic.NeoStalnakerian.EpistemicClosure f i = ∀ w ∈ i, f w = i

theorem Semantics.Dynamic.NeoStalnakerian.MI_relational_might_eq_domain (f : Attitudes.Intensional.World → List Attitudes.Intensional.World) (i : List Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) (hClosed : EpistemicClosure f i) (hi : i ≠ []) : (∀ w ∈ i, mightRelational f p w = true) ↔ i.any p = true

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 Semantics.Dynamic.NeoStalnakerian.mustRelational (f : Attitudes.Intensional.World → List Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

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

Equations

• Semantics.Dynamic.NeoStalnakerian.mustRelational f p w = (f w).all p

theorem Semantics.Dynamic.NeoStalnakerian.MI_relational_must_eq_domain (f : Attitudes.Intensional.World → List Attitudes.Intensional.World) (i : List Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) (hClosed : EpistemicClosure f i) (_hi : i ≠ []) : (∀ w ∈ i, mustRelational f p w = true) ↔ ∀ w ∈ i, p w = true

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 Semantics.Dynamic.NeoStalnakerian.mightRelOrd (f : Attitudes.Intensional.World → List Attitudes.Intensional.World) (g : Attitudes.Intensional.World → List (BProp Attitudes.Intensional.World)) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

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

• Semantics.Dynamic.NeoStalnakerian.mightRelOrd f g p w = { base := f w, ordering := g w }.bestWorlds.any p

def Semantics.Dynamic.NeoStalnakerian.OrderingClosure (g : Attitudes.Intensional.World → List (BProp Attitudes.Intensional.World)) (base : List Attitudes.Intensional.World) (ordering : List (BProp Attitudes.Intensional.World)) : Prop

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

eq. (71).

Equations

• Semantics.Dynamic.NeoStalnakerian.OrderingClosure g base ordering = ∀ w ∈ base, g w = ordering

theorem Semantics.Dynamic.NeoStalnakerian.MI_relOrd_might_eq_domain (f : Attitudes.Intensional.World → List Attitudes.Intensional.World) (g : Attitudes.Intensional.World → List (BProp Attitudes.Intensional.World)) (i : OrdEpistemicState) (p : BProp Attitudes.Intensional.World) (hfClosed : EpistemicClosure f i.base) (hgClosed : OrderingClosure g i.base i.ordering) (hi : i.base ≠ []) : (∀ w ∈ i.base, mightRelOrd f g p w = true) ↔ 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 Semantics.Dynamic.NeoStalnakerian.nonEpistemic_truth_acceptance_biconditional {W : Type u_1} (p : BProp W) (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 = false) : 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 Semantics.Dynamic.NeoStalnakerian.might_truth_acceptance_dissociate {W : Type u_1} (p : BProp W) (c_assertor c_rejector : List W) (h_assertor_has_p : c_assertor.any p = true) (h_rejector_no_p : c_rejector.any p = false) : 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 @cite{khoo-2015}: participants reject might-claims (mean Likert rejection ~5.03) without judging them false (mean Likert falsity ~2.42).

§4.3, bridging §4.2.1.