Docs / Studies / Studies.ChatainSchlenker2026

Local Pragmatics Redux: Presupposition Accommodation Without Covert Operators

Chatain, K. & Schlenker, P. (2026). Semantics of Natural Languages, 1(1)

This file formalizes the argument that local accommodation is not the work of a covert node A, Bochvar's assertion operator, but of Free Enrichment, which conjoins a contextual restriction R in Strong Kleene with an elementary predicate. An operator whose meaning ignores context accommodates at every argument of a λ-abstract or at none, so an elided clause would copy its antecedent's choice. One enrichment can project at one argument and accommodate at another, and can accommodate one of a trigger's two presuppositions while the other projects.

Implementation notes

A trivalent predicate P : E → W → SignType is 0 where its presupposition fails. Free Enrichment (62) is Modifier.intersective at fun x w ↦ ofProp (R x w), written out below as ofProp (R x w) ⊓ P x w. On the partial composition engine, whose predicate modification is Weak Kleene, Free Enrichment is instead a map on the lexicon, if R d w then P w d else false, which agrees with the Strong Kleene conjunction because R is two-valued (enrichment_eq_meetMiddle); the composition rules (63) are then the engine's own. Since every mode of that engine is strict (Montague.Mode.dom_right_of_dom_evalPartial), A is no word meaning there.

TODO

Intermediate accommodation (55), Homer's diagnostic (§4.2.1), and the constraint on Free Enrichment that (77) calls for (§5.2.2).

References

Chatain & Schlenker 2026, Local Pragmatics Redux: Presupposition Accommodation Without Covert Operators
Beaver & Krahmer 2001, A Partial Account of Presupposition Projection formalized
Bochvar 1938, On a Three-valued Logical Calculus and Its Application to the Analysis of the Paradoxes of the Classical Extended Functional Calculus
Romoli 2011, Presupposition Wipe-Out Can’t Be All or Nothing: A Note on Conflicting Presuppositions

Operators and parallelism

An operator applied pointwise that keeps defined values defined, such as A, negation or their composite, either keeps the gap of every argument or fills the gap of every argument, so an elided clause accommodates exactly when its antecedent does (Table 1).

theorem pointwise_projects_or_accommodates L58–70

{E : Type u_1} {W : Type u_2} (f : SignType → SignType) (hf : ∀ (a : SignType), a ≠ 0 → f a ≠ 0) (P : E → W → SignType) :

(∀ (x : E), Trivalent.gapExt (f ∘ P x) = Trivalent.gapExt (P x)) ∨ ∀ (x : E), Trivalent.gapExt (f ∘ P x) = ∅

Free Enrichment

An enrichment trivial at Y and entailing the presupposition at X lets the presupposition project at Y and accommodates it at X, so the antecedent and the elided clause of (26) can share one λ-abstract and differ ((66)–(70)) ((71)).

theorem enrichment_projects_and_accommodates L86–95

{E : Type u_1} {W : Type u_2} (P : E → W → SignType) (R : E → W → Prop) [(x : E) → DecidablePred (R x)] {X Y : E} (hY : ∀ (w : W), R Y w) (hX : ∀ (w : W), R X w → P X w ≠ 0) :

(Trivalent.gapExt fun (w : W) => min (SignType.ofProp (R Y w)) (P Y w)) = Trivalent.gapExt (P Y) ∧ (Trivalent.gapExt fun (w : W) => min (SignType.ofProp (R X w)) (P X w)) = ∅

Enrichment by definedness is local accommodation by A (§5.2).

theorem enrichment_by_definedness L106–109

{E : Type u_1} {W : Type u_2} (P : E → W → SignType) :

(fun (x : E) (w : W) => min (SignType.ofProp (P x w ≠ 0)) (P x w)) = fun (x : E) (w : W) => SignType.ofProp (P x w = 1)

L112–114

Partial accommodation

Enriching a trigger that presupposes S ∩ T by S accommodates S and leaves the conditional presupposition that S implies T (§5.2.1), while A above the trigger leaves no presupposition at all ((35), Trivalent.gapExt_ofProp_eq_one), as does the substrate's accommodation of every trigger at once (Presupposition.Formula.isBivalent_middleKleene_accommodate).

theorem partial_accommodation L118–126

{W : Type u_2} (S T : Set W) [DecidablePred fun (x : W) => x ∈ S] {f : W → SignType} (hf : Trivalent.IsBivalent f) :

(Trivalent.gapExt fun (w : W) => min (SignType.ofProp (w ∈ S)) ((S ∩ T).indicator f w)) = S \ T

Each example accommodates one presupposition of its trigger and projects the other, so enriching by the accommodated one leaves exactly the other's conditional gap ((34), (38), (39)).

theorem partial_accommodation_rows L149–163

{W : Type u_2} (S T : Set W) [DecidablePred fun (x : W) => x ∈ S] [DecidablePred fun (x : W) => x ∈ T] {f : W → SignType} (hf : Trivalent.IsBivalent f) (row : Datum) :

row ∈ Examples.all → ∀ q ∈ row.parse? "accommodated" slots, ∀ r ∈ row.parse? "projected" slots, q ≠ r ∧ (Trivalent.gapExt fun (w : W) => min (SignType.ofProp (w ∈ Slot.set S T q)) ((S ∩ T).indicator f w)) = Slot.set S T q \ Slot.set S T r

Built from ,

Projection and accommodation

In a knowledge-monotone context C, the reading on which the presupposition projects entails the reading on which it is accommodated locally (§4.1).

theorem projection_entails_accommodation L167–176

{C : SignType → SignType} (hC : ∀ (a b : SignType), a.toFlat ≤ b.toFlat → (C a).toFlat ≤ (C b).toFlat) {a : SignType} (h : C a = 1) :

C (SignType.ofProp (a = 1)) = 1

Composition

The derivation of Examples.ex_26 on the partial engine.

The three-valued readout of the engine's denotation is the Strong Kleene negation of the enriched predicate, so the engine and enrichment_projects_and_accommodates describe one object ((67)).

theorem ofPart_clause L231–237

{D W : Type} (P : W → D →. Prop) (R : D → W → Prop) (w : W) (d : D) :

SignType.ofPart (Part.map Not (if R d w then P w d else Part.some False)) = -min (SignType.ofProp (R d w)) (SignType.ofPart (P w d))

The clause fails exactly where the enrichment holds and the predicate is undefined ((68), (70)).

theorem presupFailure_clause L239–245

{D W : Type} (P : W → D →. Prop) (R : D → W → Prop) (w : W) (g : Assignment D) (d : D) :

PhraseStructure.Tree.PresupFailure (lexicon P R w) g (clause d) ↔ R d w ∧ ¬(P w d).Dom

Built from ,

With an enrichment trivial at Y and entailing the presupposition at X, the clause shared by the antecedent and the elided clause fails at Y exactly where the presupposition does and never fails at X ((66)–(70)).

theorem clause_projects_and_accommodates L247–255

{D W : Type} (P : W → D →. Prop) (R : D → W → Prop) (w : W) (g : Assignment D) {X Y : D} (hY : ∀ (w : W), R Y w) (hX : ∀ (w : W), R X w → (P w X).Dom) :

(PhraseStructure.Tree.PresupFailure (lexicon P R w) g (clause Y) ↔ ¬(P w Y).Dom) ∧ ¬PhraseStructure.Tree.PresupFailure (lexicon P R w) g (clause X)

Built from ,

L257–261