Documentation

Linglib.Phenomena.Presupposition.Studies.Karttunen1973

Karttunen 1973: Presuppositions of Compound Sentences #

@cite{karttunen-1973} @cite{hintikka-1962} @cite{karttunen-1971}

Linguistic Inquiry 4(2): 169–193.

The projection problem: how presuppositions of constituent sentences are inherited (or not) by compound sentences. K1973's contribution is the plug/hole/filter taxonomy of complement-takers (§§3–5), the asymmetric filtering rules for the connectives (§§5–7), the §8 Harman derivation of the conditional/conjunction-filter coincidence, and the §9 admission that filtering must be relativized to a set of background assumptions — the genealogical ancestor of CCP local contexts (@cite{heim-1983}, @cite{schlenker-2009}).

This file makes load-bearing the contributions that survive: the classification (§§3–4), the rule (13)/(17)/(24) filters, the §8 Harman derivation, the §9 X-set machinery (with concrete Geraldine example), and the §10 three-valued comparison (Bochvar internal/external negation in particular). K1973's §11 verdict on propositional attitudes (tentative plug, hedged) is recorded explicitly and contrasted with the Heim-1992-era hole consensus.

K1973 §3 (p. 174) plug list: "say, mention, tell, ask, promise, warn, request, order, accuse, criticize, blame" — verbs of saying / performatives. K1973 §4 (p. 175) hole list: "know, regret, understand, surprise, be significant, begin, stop, continue, manage, avoid, be able, be possible, force, prevent, hesitate, seem, be probable" — Kiparsky's factives, Newmeyer's aspectuals, K's one- and two-way implicatives. Footnote 6 (p. 175) adds realize: "factive verbs, such as realize, … are holes irrespective of the type of the complement."

K1973's lists are **lexical, not structural**: there is no clean
`inferProjection : VerbCore → ProjectionBehavior`, because the
Fragment has e.g. `reveal` as `speechActVerb := true` *and* a factive
soft-trigger (which would be a hole). So the file consolidates K's
Fragment-attested classifications as list-quantified theorems
rather than re-stipulating per-verb rfl checks. 

K1973 §3 plug list, restricted to the Fragment's attested entries. K's other list members (mention, ask, warn, request, order, accuse, criticize) lack a projectionBehavior annotation in Verbal.lean.

Equations
Instances For

    K1973 §4 hole list, restricted to the Fragment's attested entries. realize is included on the strength of K1973 fn 6 paragraph 3.

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

      K's distinction: trigger-status (introduces a presupposition?) is orthogonal to projection-behavior (passes complement presuppositions through?). know exhibits both.

      K1973 fn 6 (p. 175 paragraph 4): tell is a plug for that-clauses but a hole for indirect questions ("Bill told John that Harry insulted the present king of France" vs "Bill told John who insulted the present king of France"). The Fragment's flat tell.projectionBehavior = some .plug is K's that-clause verdict; the indirect-question case is a separate analysis K credits to Permesly 1973 (Ch. 2).

      K1973 §1 (5)/(6) typological contrast: plugs and holes are distinct profiles. K's own minimal pair uses order vs force; order lacks a Fragment annotation, so we use the closest attested pair (promise, plug; force, hole).

      K1973 §11 (pp. 188–190) discusses propositional attitudes at length. §4 raised the question (hole or plug?) and postponed it. §11 considers the hole-with-equivalence-machinery analysis: the (37)/(38) move uses @cite{hintikka-1962}'s believe(A) ∧ believe(B) ↔ believe(A ∧ B) to let believe survive as a hole even when the complement-internal presupposition appears not to project. (38) keeps the hole verdict safe for cases like

          (37) Bill believes Fred has been beating Zelda, and furthermore,
               Bill believes that Fred has stopped beating Zelda.
      
      But K's (42) defeats the trick — two distinct attitude verbs (believe
      + hope) on a shared presupposed clause can't be re-collected into a
      single attitude:
      
          (42) Bill believed that Fred had been beating his wife and hoped
               that Fred would stop beating her.
      
      K's tentative §11 conclusion (p. 190): "we do not seem to have any
      other alternative except to classify all propositional attitude verbs
      as plugs, although I am still not convinced that this is the right
      approach." So K1973's published verdict on `believe` is **tentative
      plug, with explicit hedging**. The Fragment annotation
      `believe.projectionBehavior = some .hole` reflects the post-1974 /
      @cite{heim-1992} consensus, not K1973. 
      

      believe has no presupposition trigger (doxastic, not factive).

      Contentful disagreement on a concrete scenario #

      The flat enum-tag inequality `.plug ≠ .hole` is meta-fact. The real
      disagreement: on a scenario where the complement of *believe* carries
      a presupposition that is true in the attitude holder's belief state
      but false in reality, the two analyses make distinct predictions
      about what the speaker is committed to. 
      

      Two-world model: actual (where Mary never smoked) and believed (John's belief world, where Mary did smoke).

      Instances For
        @[implicit_reducible]
        Equations
        def Karttunen1973.instReprAttWorld.repr :
        AttWorldStd.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          "Mary used to smoke" — the presupposition of "stop smoking". True in believed, false in actual.

          Equations
          Instances For

            The speaker-projection of a plug-treatment of believe: nothing of the complement projects.

            Equations
            Instances For

              The speaker-projection of K1973's flat hole-treatment of believe (pre-Heim 1992): the complement's presupposition projects unchanged to the speaker.

              Equations
              Instances For

                The plug analysis predicts no speaker commitment to "Mary used to smoke" at the actual world; the hole analysis predicts the speaker IS committed there. The two analyses make different predictions on the same input.

                Heim 1992 / @cite{schlenker-2009} resolve the dispute by attributing the presupposition to the attitude holder, not the speaker. The holder-attribution analysis lives in Theories/Semantics/Presupposition/BeliefEmbedding.lean as presupAttributedToHolder. K1973's flat hole-treatment differs from both Heim 1992's holder-attribution and K1973 §11's tentative plug verdict — three coexisting positions on the same data.

                Karttunen's rules (13), (17), (24) are realized by Core.Presupposition operators impFilter, andFilter, disjFilterLeft/orFilter. Theorems below re-export Core facts under K's rule names for greppability.

                K1973 rule (13a), p. 178: the antecedent's presupposition always projects to "If A then B".

                K1973 rule (13b), p. 178: B's presupposition is filtered when A's assertion entails it.

                K1973 rule (17), p. 179: filtering for and matches that for if...then.

                theorem Karttunen1973.disjFilterLeft_eliminates_presup_when_neg_entails {W : Type u_1} (A : WProp) (q : Core.Presupposition.PrProp W) (h : ∀ (w : W), ¬A wq.presup w) :

                K1973 rule (24b), p. 181 — paper-anchored alias for the substrate PrProp.disjFilterLeft_eliminates_presup_when_neg_entails. Karttunen's asymmetric form: "A or B" carries no residual presupposition from B when ¬A entails it. The substrate carries the proof; Karttunen 1973 is the paper that motivated it.

                theorem Karttunen1973.cumulativity_principle {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) :
                (p.and q).presup w p.presup w q.presup w

                K's "cumulative principle" (Langendoen & Savin 1971; named by Morgan 1969 per K1973 §1): the presuppositions of a compound include those of its constituents. For PrProp.and this is just the conjunction of presuppositions.

                K1973 §8 (p. 181) credits Gilbert Harman (p.c.) with the observation that identical filtering for if...then and and is consistent with classical logic given: (i) internal negation preserves presupposition, (ii) logical equivalents share presupposition, (iii) classical De Morgan / contraposition.

                `if_and_share_presup_function` re-exports the underlying Core
                identity; `harman_derivation_principles_hold` records the principles
                K's §8 argument relies on. 
                

                The presupposition functions of if A then B and A and B coincide.

                Harman's principles, as facts about Core PrProp connectives: (i) internal negation preserves presupposition; (ii) impFilter and andFilter share presupposition (the structural witness of "logical equivalents share presupposition" specialized to the De Morgan equivalence ⌜A ⊃ B⌝ ≡ ⌜~(A ∧ ~B)⌝).

                K1973 §9 (pp. 182–185) relativizes the filtering rules to a "(possibly null) set X of assumed facts". K p. 185: "We can no longer talk about the presuppositions of a compound sentence in an absolute sense, only with regard to a given set of background assumptions." This is the genealogical ancestor of CCP local contexts.

                The bridge to local contexts is in `LocalContext.lean`; the theorem
                below consumes `local_context_matches_impFilter` explicitly so the
                K1973 → CCP relation is a Lean dependency rather than a docstring
                claim. 
                
                theorem Karttunen1973.k1973_section9_local_context_correspondence {W : Type u_1} (c : Core.CommonGround.ContextSet W) (p q : Core.Presupposition.PrProp W) :
                (∀ (w : W), c w(p.impFilter q).presup w) ∀ (w : W), c wp.presup w (p.assertion wq.presup w)

                K1973 §9 ↔ CCP local contexts: the presupposition of if A then B holds throughout context c iff at every world in c, A's presupposition holds and A's assertion entails B's presupposition. The forward direction is K's rule (13b) relativized; the backward direction is Schlenker's local-context derivation.

                theorem Karttunen1973.rule13b_is_empty_X_instance {W : Type u_1} (p q : Core.Presupposition.PrProp W) (h : ∀ (w : W), p.assertion wq.presup w) :

                K1973 §9's revised rule (13b'): the simple rule (13b) is the X = ∅ instance. K p. 185 frames (13b) as a degenerate case of the X-set machinery, which is what LocalContext.lean makes load-bearing for the general case.

                K1973 §10 (pp. 185–188) compares four three-valued conjunction tables:

                | System            | K's verdict (pp. 187–188)            |
                |-------------------|---------------------------------------|
                | Bochvar internal  | hole (no filtering, cumulative)       |
                | Łukasiewicz       | symmetric truth-value-based filter    |
                | Van Fraassen      | symmetric truth-value-based filter    |
                | Bochvar external  | plug (truth operator t : # → F)       |
                
                K rejects all four for natural language (p. 188): the truth-value-
                based filters give wrong predictions on examples like (35), and the
                Bochvar systems lack the asymmetric filtering K's (17)/(24) capture.
                This motivates the §9 X-set / context-relative formulation that
                becomes CCP. 
                
                theorem Karttunen1973.bochvar_internal_is_cumulative {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) :
                (p.and q).presup w p.presup w q.presup w

                Bochvar internal conjunction = PrProp.and = cumulative principle. K1973 p. 187: "the internal Bochvar connectives are holes."

                The filtering conjunction is strictly weaker than cumulative: andFilter can be defined when q's presupposition fails (provided p's assertion is false).

                K1973 §10 footnote 18 (p. 187): two senses of not.

                > "As internal negation (choice negation), *not* is a hole and lets
                > through all of the presuppositions of the sentence it negates.
                > The external (exclusion negation) *not* is a plug that blocks off
                > all of them." (p. 187)
                
                K defines `⌜¬A⌝ ≡ ⌜~t(A)⌝`. Both operators are now in
                `Core.Presupposition`: `PrProp.neg` (internal/choice) and
                `PrProp.negExt` (external/exclusion = `neg ∘ truthOp`). 
                

                Internal negation preserves presupposition (it's a hole).

                External negation is always defined (it's a plug).

                Internal and external negation agree on assertion at worlds where the presupposition holds; they diverge only at presupposition failure (where neg is undefined and negExt is asserted true).

                K1973 §9 ex (25)–(28), pp. 182–183:

                    (25) Either Geraldine is not a Mormon or she has given up
                         wearing her holy underwear.
                    (26) Geraldine is a Mormon.   (negation of first disjunct)
                    (27) Geraldine has worn holy underwear.   (presup of second)
                    (28) All Mormons have worn holy underwear.   (Fred's belief)
                
                The simple rule (24b) requires ⌜~(25-first)⌝ ⊨ (27), i.e.,
                (26) ⊨ (27). This fails directly. The revised (24b') admits an
                X-set such that X ∪ {(26)} ⊨ (27); K supplies X = {(28)}. The
                example demonstrates that filtering must consult background
                assumptions beyond the disjuncts themselves — exactly the move that
                becomes CCP. 
                

                Four-world model parameterized by Geraldine's Mormon-status and her holy-underwear history.

                Instances For
                  @[implicit_reducible]
                  Equations
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    "Geraldine is a Mormon" — no presupposition.

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

                      K1973 (28): "All Mormons have worn holy underwear" — modeled as a background assumption excluding mormon_notWorn.

                      Equations
                      Instances For

                        The simple K1973 rule (24b) fails: there exist worlds where ¬isMormon holds but hasWornHolyUnderwear does not (witness: notMormon_notWorn). So without an X-set, the second disjunct's presupposition is not filtered.

                        The revised K1973 rule (24b') with X = {(28)} succeeds: at every world consistent with the background assumption (28) where ¬isMormon also holds, hasWornHolyUnderwear does NOT need to hold — but the rule (24b') only requires X ∪ {¬A} ⊨ C, and at the surviving counterexample worlds the disjunction's first disjunct is in fact true (or the world is excluded by (28)). The lemma below formalizes the survivor: at every (28)-compatible world where ¬isMormon holds, hasWornHolyUnderwear need NOT hold (the rule is vacuously satisfied at the kept worlds because ¬isMormon and notMormon_notWorn is one of the worlds). The genuine content is that no (28)-compatible world is mormon_notWorn, where the presupposition would have classically failed.