[Sau04] — Scalar Implicatures in Complex Sentences

[Sau04]

Sauerland, U. (2004). Scalar implicatures in complex sentences. Linguistics and Philosophy 27(3): 367–391.

The paper's derivation for disjunction, run through the consistency-gated algorithm in Pragmatics/NeoGricean/Basic.lean (IsSecondaryImplicature, implementing the paper's (42)/(43), verified p. 383): asserting A or B against the alternatives {A, B, A∧B} yields the primary implicatures ¬KA, ¬KB, ¬K(A∧B). Of the candidate secondary implicatures, K¬(A∧B) is consistent with the commitments and arises (conj_secondary), while K¬A is blocked (disjunct_blocked): K¬A together with K(A∨B) forces KB, contradicting the primary ¬KB. (The paper frames the same block dually: K¬A contradicts the possibility implicature PA entailed by the assertion plus ¬KB.) This asymmetry — "not both" arises but "not A" does not — is the paper's signature prediction for disjunction, unavailable to accounts that negate all stronger alternatives indiscriminately.

The four-world model DisjWorld distinguishes worlds by which disjuncts hold; the assertion A or B excludes only neither.

inductive Sauerland2004.DisjWorld : Type

Worlds distinguished by which of the two disjuncts hold.

• neither : DisjWorld
• onlyA : DisjWorld
• onlyB : DisjWorld
• both : DisjWorld

@[instance_reducible]

instance Sauerland2004.instDecidableEqDisjWorld : DecidableEq DisjWorld

Equations

• Sauerland2004.instDecidableEqDisjWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sauerland2004.instReprDisjWorld.repr : DisjWorld → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Sauerland2004.instReprDisjWorld : Repr DisjWorld

Equations

• Sauerland2004.instReprDisjWorld = { reprPrec := Sauerland2004.instReprDisjWorld.repr }

@[instance_reducible]

instance Sauerland2004.instFintypeDisjWorld : Fintype DisjWorld

Equations

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

def Sauerland2004.DisjWorld.propA : Set DisjWorld

The first disjunct A.

Equations

• Sauerland2004.DisjWorld.propA = {Sauerland2004.DisjWorld.onlyA, Sauerland2004.DisjWorld.both}

def Sauerland2004.DisjWorld.propB : Set DisjWorld

The second disjunct B.

Equations

• Sauerland2004.DisjWorld.propB = {Sauerland2004.DisjWorld.onlyB, Sauerland2004.DisjWorld.both}

def Sauerland2004.DisjWorld.disj : Set DisjWorld

The assertion A or B.

Equations

• Sauerland2004.DisjWorld.disj = {Sauerland2004.DisjWorld.onlyA, Sauerland2004.DisjWorld.onlyB, Sauerland2004.DisjWorld.both}

def Sauerland2004.DisjWorld.conj : Set DisjWorld

The conjunctive alternative A and B.

Equations

• Sauerland2004.DisjWorld.conj = {Sauerland2004.DisjWorld.both}

def Sauerland2004.orAlts : Set (Set DisjWorld)

The scalar alternatives to A or B: each disjunct and the conjunction.

Equations

• Sauerland2004.orAlts = {Sauerland2004.DisjWorld.propA, Sauerland2004.DisjWorld.propB, Sauerland2004.DisjWorld.conj}

theorem Sauerland2004.conj_secondary : NeoGricean.IsSecondaryImplicature DisjWorld.disj orAlts DisjWorld.conj

The secondary implicature that arises: K¬(A∧B) is consistent with the assertion and all primary implicatures — witnessed by the strengthened meaning disj \ conj, the state considering exactly onlyA and onlyB possible. This is the "not both" inference of A or B.

theorem Sauerland2004.disjunct_blocked : ¬NeoGricean.IsSecondaryImplicature DisjWorld.disj orAlts DisjWorld.propA

The blocked secondary implicature: K¬A is inconsistent with the commitments. The strengthened meaning disj \ propA entails B, so K¬A together with K(A∨B) forces KB — contradicting the primary implicature ¬KB (isSecondaryImplicature_iff: the single primary ¬KB blocks K¬A). The disjuncts therefore yield only ignorance inferences, never "not A".

theorem Sauerland2004.disjunct_blocked' : ¬NeoGricean.IsSecondaryImplicature DisjWorld.disj orAlts DisjWorld.propB

By the A↔B symmetry of the model, K¬B is blocked identically, by ¬KA.

theorem Sauerland2004.strengthened_or_realizable : (DisjWorld.disj \ DisjWorld.conj).Nonempty

The strengthened reading of A or B the algorithm predicts: assertion plus the licensed "not both", realizable at exactly the one-disjunct worlds.