Documentation

Linglib.Semantics.Presupposition.Context

Presuppositions in context #

A context set admits a sentence with a presupposition when it entails the presupposition, in the tradition of Stalnaker, Karttunen and Heim: for a trivalent proposition p, when C ⊆ Function.support p. An embedded clause is checked in its local context. Karttunen's table gives the local contexts of the connectives (Connective.localContext): a first argument and the argument of negation are evaluated in the context itself, the second argument of a conjunction or a conditional in the context updated with the first argument, and a second disjunct in the context updated with the first disjunct's negation. The complement of an attitude verb is evaluated in the image of the context under the subject's doxastic accessibility, which admits a sentence iff the context entails the core of its presupposition along the relation (SetRel.image_subset_iff), so the report presupposes that the subject believes what the complement presupposes.

Theories of projection agree on the table and differ in why it holds. Karttunen's filtering connectives, Peters' Middle Kleene connectives, are admittance in it (subset_support_meetMiddle_iff), Heim's context change potentials evaluate their second argument in it (Semantics/Dynamic/Partial.lean), and Schlenker derives it from transparency. They part at disjunction, where the table is asymmetric and symmetric filtering is TwoDim.orKPSymmetric.

Main declarations #

References #

source
inductive Presupposition.Connective :
Type

The binary connectives of [Kar74a]'s table of local contexts.

Instances For
    source
    @[instance_reducible]
    instance Presupposition.instDecidableEqConnective :
    DecidableEq Connective
    Equations
    source
    @[instance_reducible]
    instance Presupposition.instFintypeConnective :
    Fintype Connective
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Presupposition.Connective.localContext {W : Type u_1} (C A : Set W) :
    Connective → Set W

    The local context of a connective's second argument in the context C, where A is the first argument's content. It is C updated with A for a conjunction or a conditional, and with the negation of A for a disjunction.

    Equations
    Instances For
      source
      theorem Presupposition.subset_support_meetMiddle_iff {W : Type u_1} {C : Set W} {p q : W → SignType} :
      (C ⊆ Function.support fun (w : W) => (p w).meetMiddle (q w)) ↔ C ⊆ Function.support p ∧ Connective.localContext C (Trivalent.posExt p) Connective.conj ⊆ Function.support q

      A context admits Karttunen's filtering conjunction when it admits the first conjunct and the second conjunct's local context admits the second.

      source
      theorem Presupposition.subset_support_neg_joinMiddle_iff {W : Type u_1} {C : Set W} {p q : W → SignType} :
      (C ⊆ Function.support fun (w : W) => (-p w).joinMiddle (q w)) ↔ C ⊆ Function.support p ∧ Connective.localContext C (Trivalent.posExt p) Connective.cond ⊆ Function.support q

      A context admits Karttunen's filtering conditional when it admits the antecedent and the consequent's local context admits the consequent.

      source
      theorem Presupposition.subset_support_joinMiddle_iff {W : Type u_1} {C : Set W} {p q : W → SignType} :
      (C ⊆ Function.support fun (w : W) => (p w).joinMiddle (q w)) ↔ C ⊆ Function.support p ∧ Connective.localContext C (Trivalent.posExt p) Connective.disj ⊆ Function.support q

      A context admits Karttunen's filtering disjunction when it admits the first disjunct and the second disjunct's local context admits the second.