Occurrences of triggers

The theories of presupposition projection read three things off an occurrence of a trigger: its presupposition and its assertion, as denotations of the gap the trigger fills, and at each parsing point after it the continuations they consult, the functions from the gap's denotation to the sentence's truth set (Presupposition.Occurrence). The parsing points run from the first, which consults every good final of the string up to the trigger, to the last, ⊤, which consults the sentence itself, and a later parsing point consults fewer continuations.

A theory checks the presupposition at a parsing point: transparency (Occurrence.Transparent), satisfaction in the local context (Occurrence.Satisfied), or stable transparency (Occurrence.StablyTransparent). Since the continuations shrink along the parsing points, transparency at a parsing point holds at every later one (Occurrence.Transparent.mono) and implies stable transparency there (Occurrence.Transparent.stablyTransparent), and at the last parsing point, where only the sentence itself is consulted, stable transparency is transparency (Occurrence.stablyTransparent_top_iff).

Each sentence type lists the occurrences of its triggers: Formula.occurrences for the propositional fragment and QuantifiedClause.occurrences for quantified clauses.

References

• [Sch09a]
• [Kal23]

structure Presupposition.Occurrence (W : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

An occurrence of a trigger: its presupposition and its assertion as denotations of its gap, and the continuations consulted at each parsing point after it, which shrink from parsing point to parsing point down to the sentence's own continuation at the last.

• presupposition : α

  The presupposition.

• assertion : α

  The assertion.

• continuations : ℕ∞ → Set (α → Set W)

  The continuations consulted at each parsing point.

• truth : α → Set W

  The sentence's truth set as a function of the gap's denotation.

• antitone_continuations : Antitone self.continuations
• continuations_top : self.continuations ⊤ = {self.truth}

theorem Presupposition.Occurrence.truth_mem_continuations {W : Type u_1} {α : Type u_2} (o : Occurrence W α) (n : ℕ∞) : o.truth ∈ o.continuations n

Every parsing point consults the sentence's own continuation.

def Presupposition.Occurrence.Transparent {W : Type u_1} {α : Type u_2} (o : Occurrence W α) [SemilatticeInf α] (n : ℕ∞) (C : Set W) : Prop

The presupposition is a transparent restriction at parsing point n.

Equations

• o.Transparent n C = Presupposition.Transparent C (o.continuations n) o.presupposition

def Presupposition.Occurrence.Satisfied {W : Type u_1} {α : Type u_2} (o : Occurrence W α) [SemilatticeInf α] (n : ℕ∞) (C : Set W) : Prop

The local context at parsing point n entails the presupposition.

Equations

• o.Satisfied n C = Presupposition.Satisfied C (o.continuations n) o.presupposition

def Presupposition.Occurrence.StablyTransparent {W : Type u_1} {α : Type u_2} (o : Occurrence W α) [SemilatticeInf α] (n : ℕ∞) (C : Set W) : Prop

The presupposition is stably transparent at parsing point n.

Equations

• o.StablyTransparent n C = Presupposition.StablyTransparent C (o.continuations n) o.presupposition

theorem Presupposition.Occurrence.Transparent.mono {W : Type u_1} {α : Type u_2} {o : Occurrence W α} [SemilatticeInf α] {n : ℕ∞} {C : Set W} {m : ℕ∞} (h : o.Transparent n C) (hnm : n ≤ m) : o.Transparent m C

Transparency at a parsing point holds at every later one.

theorem Presupposition.Occurrence.Satisfied.transparent {W : Type u_1} {α : Type u_2} {o : Occurrence W α} [SemilatticeInf α] {n : ℕ∞} {C : Set W} (h : o.Satisfied n C) : o.Transparent n C

theorem Presupposition.Occurrence.Transparent.stablyTransparent {W : Type u_1} {α : Type u_2} {o : Occurrence W α} [SemilatticeInf α] {n : ℕ∞} {C : Set W} (h : o.Transparent n C) : o.StablyTransparent n C

theorem Presupposition.Occurrence.stablyTransparent_top_iff {W : Type u_1} {α : Type u_2} {o : Occurrence W α} [SemilatticeInf α] {C : Set W} : o.StablyTransparent ⊤ C ↔ o.Transparent ⊤ C

At the last parsing point, where only the sentence itself is consulted, stable transparency is transparency.