Documentation

Linglib.Studies.Sauerland2004

[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 (SecondaryLicensed, 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 licensed (conj_secondary_licensed), while K¬A is blocked (disjunct_secondary_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.

source
inductive Sauerland2004.DisjWorld :
Type

Worlds distinguished by which of the two disjuncts hold.

Instances For
    source
    @[implicit_reducible]
    instance Sauerland2004.instDecidableEqDisjWorld :
    DecidableEq DisjWorld
    Equations
    source
    def Sauerland2004.instReprDisjWorld.repr :
    DisjWorld → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Sauerland2004.instReprDisjWorld :
      Repr DisjWorld
      Equations
      source
      @[implicit_reducible]
      instance Sauerland2004.instFintypeDisjWorld :
      Fintype DisjWorld
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Sauerland2004.DisjWorld.propA :
      DisjWorld → Prop

      The first disjunct A.

      Equations
      Instances For
        source
        def Sauerland2004.DisjWorld.propB :
        DisjWorld → Prop

        The second disjunct B.

        Equations
        Instances For
          source
          def Sauerland2004.DisjWorld.disj :
          DisjWorld → Prop

          The assertion A or B.

          Equations
          Instances For
            source
            def Sauerland2004.DisjWorld.conj :
            DisjWorld → Prop

            The conjunctive alternative A and B.

            Equations
            Instances For
              source
              @[implicit_reducible]
              instance Sauerland2004.DisjWorld.instDecidablePredPropA :
              DecidablePred propA
              Equations
              source
              @[implicit_reducible]
              instance Sauerland2004.DisjWorld.instDecidablePredPropB :
              DecidablePred propB
              Equations
              source
              @[implicit_reducible]
              instance Sauerland2004.DisjWorld.instDecidablePredDisj :
              DecidablePred disj
              Equations
              source
              @[implicit_reducible]
              instance Sauerland2004.DisjWorld.instDecidablePredConj :
              DecidablePred conj
              Equations
              source
              def Sauerland2004.orAlts :
              List (DisjWorld → Prop)

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

              Equations
              Instances For
                source
                theorem Sauerland2004.conj_secondary_licensed :
                NeoGricean.SecondaryLicensed DisjWorld.disj orAlts DisjWorld.conj

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

                source
                theorem Sauerland2004.disjunct_secondary_blocked :
                ¬NeoGricean.SecondaryLicensed DisjWorld.disj orAlts DisjWorld.propA

                The blocked secondary implicature: K¬A is inconsistent with the commitments. From K(A∨B) and K¬A every possible world satisfies B, so KB holds — contradicting the primary implicature ¬KB. The disjuncts therefore yield only ignorance inferences, never "not A".

                source
                theorem Sauerland2004.disjunct_secondary_blocked' :
                ¬NeoGricean.SecondaryLicensed DisjWorld.disj orAlts DisjWorld.propB

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

                source
                theorem Sauerland2004.strengthened_or_realizable :
                ∃ (w : DisjWorld), w.disj ∧ ¬w.conj

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