Farkas & Bruce 2010

[FB10]

The F&B table-model dynamics — assert / polarQuestion / acceptTop and the plain dcS / dcL commitment views — live in the substrate Discourse/Commitment/Table.lean, which is itself the [FB10] table model. This study file records the paper's load-bearing claim about the assertion/acceptance split.

theorem FarkasBruce2010.assert_preserves_cg {W : Type u_1} (ds : Discourse.Commitment.Table.State W) (p : W → Prop) : (Discourse.Commitment.Table.assert ds p).cg = ds.cg

F&B's assertion does not narrow the common ground, in contrast to [Sta78] where assertion is a direct common-ground update. The pre-assertion cg is preserved exactly; acceptance is a separate move (acceptTop).

theorem FarkasBruce2010.assert_not_narrowing : ∃ (ds : Discourse.Commitment.Table.State Bool) (p : Bool → Prop), ∃ w ∈ Discourse.Commitment.Table.DiscourseState.contextSet (Discourse.Commitment.Table.assert ds p), ¬p w

F&B's assert violates the Stalnakerian narrowing law: a world can survive the assertion of p without satisfying p, because assertion only proposes (dcS + table) and the context set moves at acceptance. This is the formal witness for the non-instance advertised at CommonGround.HasAssertion — State W does not instantiate it via F&B's own assert.