Syntactic environments

A syntactic environment a _ b is a formula with a gap, in Schlenker's sense. It is represented by the steps from the gap to the root, innermost first (SyntacticEnvironment): the argument of a negation, or the first or the second argument of a binary connective whose other argument is given. Filling the gap gives a formula (SyntacticEnvironment.fill), and the environment's meaning is the function from the gap's truth set to the formula's (SyntacticEnvironment.truth). The triggers of a formula are listed with their environments by Formula.triggers.

The incremental theories of projection consult every good final of the initial string up to a trigger: SameInitialString K K' holds when K' keeps the material of K before the gap and replaces what follows it. For the first argument of a conjunction or a disjunction the connective itself follows the gap in the string, so it may be replaced too, while if precedes its antecedent.

Kalomoiros checks the constraint at every parsing point after a trigger: AgreeUpTo n K K' holds when K' keeps the material before the gap and the first n items after it, counting the connective after a first argument and the second argument as one item each. At the first point it admits every good final (SyntacticEnvironment.agreeUpTo_zero_iff), and from the last point on only the environment itself (SyntacticEnvironment.agreeUpTo_iff_eq). The continuations at a parsing point n : ℕ∞ are the truth functions of these finals, the sentence's own at ⊤ (SyntacticEnvironment.continuations); a later parsing point consults fewer of them (SyntacticEnvironment.antitone_continuations). With them the triggers of a formula are occurrences in the sense of Presupposition.Occurrence (Formula.occurrences).

Karttunen's local context of a gap (SyntacticEnvironment.localContext) is recovered from the good finals: some good final makes the formula's truth value at a world depend on the gap iff the world is in the local context (SyntacticEnvironment.exists_dependsAt_iff), and the filtering evaluation is defined at a world iff every trigger's presupposition holds there whenever the world is in the trigger's local context (Formula.middleKleene_ne_zero_iff).

Main definitions

• Presupposition.SyntacticEnvironment: a formula with a gap.
• Presupposition.SyntacticEnvironment.fill, Presupposition.SyntacticEnvironment.truth: filling the gap, and the meaning as a function of the gap's.
• Presupposition.Formula.triggers: the triggers of a formula with their environments.
• Presupposition.SyntacticEnvironment.SameInitialString: the environments of the good finals.
• Presupposition.SyntacticEnvironment.AgreeUpTo: the environments of the good finals at a parsing point.
• Presupposition.SyntacticEnvironment.continuations: the continuations at a parsing point.
• Presupposition.Formula.occurrences: the triggers of a formula as occurrences.
• Presupposition.SyntacticEnvironment.localContext: Karttunen's local context of the gap.

References

• [Sch09a]
• [Kal23]
• [Kar74a]
• [Pet79]

inductive Presupposition.SyntacticEnvironment.Step (Atom : Type u_3) : Type u_3

One step from a gap to the root is the argument of a negation, or the first (left) or second (right) argument of a binary connective whose other argument is given.

• not {Atom : Type u_3} : Step Atom
• left {Atom : Type u_3} (c : Connective) (G : Formula Atom) : Step Atom
• right {Atom : Type u_3} (c : Connective) (F : Formula Atom) : Step Atom

@[instance_reducible]

instance Presupposition.SyntacticEnvironment.instDecidableEqStep {Atom✝ : Type u_3} [DecidableEq Atom✝] : DecidableEq (Step Atom✝)

Equations

• Presupposition.SyntacticEnvironment.instDecidableEqStep = Presupposition.SyntacticEnvironment.instDecidableEqStep.decEq

def Presupposition.SyntacticEnvironment.instDecidableEqStep.decEq {Atom✝ : Type u_3} [DecidableEq Atom✝] (x✝ x✝¹ : Step Atom✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Presupposition.SyntacticEnvironment.instDecidableEqStep.decEq Presupposition.SyntacticEnvironment.Step.not Presupposition.SyntacticEnvironment.Step.not = isTrue ⋯
• Presupposition.SyntacticEnvironment.instDecidableEqStep.decEq Presupposition.SyntacticEnvironment.Step.not (Presupposition.SyntacticEnvironment.Step.left c G) = isFalse ⋯
• Presupposition.SyntacticEnvironment.instDecidableEqStep.decEq Presupposition.SyntacticEnvironment.Step.not (Presupposition.SyntacticEnvironment.Step.right c F) = isFalse ⋯
• Presupposition.SyntacticEnvironment.instDecidableEqStep.decEq (Presupposition.SyntacticEnvironment.Step.left c G) Presupposition.SyntacticEnvironment.Step.not = isFalse ⋯
• Presupposition.SyntacticEnvironment.instDecidableEqStep.decEq (Presupposition.SyntacticEnvironment.Step.left c G) (Presupposition.SyntacticEnvironment.Step.right c_1 F) = isFalse ⋯
• Presupposition.SyntacticEnvironment.instDecidableEqStep.decEq (Presupposition.SyntacticEnvironment.Step.right c F) Presupposition.SyntacticEnvironment.Step.not = isFalse ⋯
• Presupposition.SyntacticEnvironment.instDecidableEqStep.decEq (Presupposition.SyntacticEnvironment.Step.right c F) (Presupposition.SyntacticEnvironment.Step.left c_1 G) = isFalse ⋯

@[reducible, inline]

abbrev Presupposition.SyntacticEnvironment (Atom : Type u_3) : Type u_3

A syntactic environment a _ b is a formula with a gap, given as the steps from the gap to the root, innermost first.

Equations

• Presupposition.SyntacticEnvironment Atom = List (Presupposition.SyntacticEnvironment.Step Atom)

def Presupposition.SyntacticEnvironment.Step.fill {Atom : Type u_1} : Step Atom → Formula Atom → Formula Atom

Fill the gap of a step.

Equations

• Presupposition.SyntacticEnvironment.Step.not.fill x✝ = x✝.not
• (Presupposition.SyntacticEnvironment.Step.left c G).fill x✝ = Presupposition.Formula.bin c x✝ G
• (Presupposition.SyntacticEnvironment.Step.right c F).fill x✝ = Presupposition.Formula.bin c F x✝

def Presupposition.SyntacticEnvironment.Step.truth {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) : Step Atom → Set W → Set W

The meaning of a step as a function of the gap's truth set.

Equations

• Presupposition.SyntacticEnvironment.Step.truth I Presupposition.SyntacticEnvironment.Step.not x✝ = x✝ᶜ
• Presupposition.SyntacticEnvironment.Step.truth I (Presupposition.SyntacticEnvironment.Step.left c G) x✝ = {w : W | c.eval (w ∈ x✝) (w ∈ Presupposition.Formula.truth I G)}
• Presupposition.SyntacticEnvironment.Step.truth I (Presupposition.SyntacticEnvironment.Step.right c F) x✝ = {w : W | c.eval (w ∈ Presupposition.Formula.truth I F) (w ∈ x✝)}

def Presupposition.SyntacticEnvironment.Step.localContext {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) : Step Atom → Set W → Set W

In [Kar74a]'s local context of the gap of a step in the context C, the second argument of a binary connective is evaluated in C updated as Connective.localContext prescribes, and any other gap in C itself.

Equations

• Presupposition.SyntacticEnvironment.Step.localContext I (Presupposition.SyntacticEnvironment.Step.right c F) x✝ = Presupposition.Connective.localContext x✝ (Presupposition.Formula.truth I F) c
• Presupposition.SyntacticEnvironment.Step.localContext I x✝¹ x✝ = x✝

theorem Presupposition.SyntacticEnvironment.Step.truth_fill {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (s : Step Atom) (X : Formula Atom) : Formula.truth I (s.fill X) = truth I s (Formula.truth I X)

theorem Presupposition.SyntacticEnvironment.Step.localContext_eq_inter {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (s : Step Atom) (C : Set W) : localContext I s C = C ∩ localContext I s Set.univ

def Presupposition.SyntacticEnvironment.fill {Atom : Type u_1} : SyntacticEnvironment Atom → Formula Atom → Formula Atom

Fill the gap of an environment.

Equations

• Presupposition.SyntacticEnvironment.fill [] x✝ = x✝
• Presupposition.SyntacticEnvironment.fill (s :: K) x✝ = Presupposition.SyntacticEnvironment.fill K (s.fill x✝)

def Presupposition.SyntacticEnvironment.truth {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) : SyntacticEnvironment Atom → Set W → Set W

The meaning of an environment as a function of the gap's truth set.

Equations

• Presupposition.SyntacticEnvironment.truth I [] x✝ = x✝
• Presupposition.SyntacticEnvironment.truth I (s :: K) x✝ = Presupposition.SyntacticEnvironment.truth I K (Presupposition.SyntacticEnvironment.Step.truth I s x✝)

def Presupposition.SyntacticEnvironment.localContext {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (K : SyntacticEnvironment Atom) (C : Set W) : Set W

[Kar74a]'s local context of the gap of an environment, computed from the root.

Equations

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

@[simp]

theorem Presupposition.SyntacticEnvironment.fill_nil {Atom : Type u_1} (X : Formula Atom) : fill [] X = X

@[simp]

theorem Presupposition.SyntacticEnvironment.fill_cons {Atom : Type u_1} (s : Step Atom) (K : SyntacticEnvironment Atom) (X : Formula Atom) : fill (s :: K) X = K.fill (s.fill X)

theorem Presupposition.SyntacticEnvironment.fill_append {Atom : Type u_1} (K K' : SyntacticEnvironment Atom) (X : Formula Atom) : (K ++ K').fill X = K'.fill (K.fill X)

theorem Presupposition.SyntacticEnvironment.truth_append {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (K K' : SyntacticEnvironment Atom) (d : Set W) : truth I (K ++ K') d = truth I K' (truth I K d)

theorem Presupposition.SyntacticEnvironment.truth_fill {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (K : SyntacticEnvironment Atom) (X : Formula Atom) : Formula.truth I (K.fill X) = truth I K (Formula.truth I X)

@[simp]

theorem Presupposition.SyntacticEnvironment.localContext_nil {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (C : Set W) : localContext I [] C = C

@[simp]

theorem Presupposition.SyntacticEnvironment.localContext_cons {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (s : Step Atom) (K : SyntacticEnvironment Atom) (C : Set W) : localContext I (s :: K) C = Step.localContext I s (localContext I K C)

theorem Presupposition.SyntacticEnvironment.localContext_append {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (K K' : SyntacticEnvironment Atom) (C : Set W) : localContext I (K ++ K') C = localContext I K (localContext I K' C)

theorem Presupposition.SyntacticEnvironment.localContext_eq_inter {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (K : SyntacticEnvironment Atom) (C : Set W) : localContext I K C = C ∩ localContext I K Set.univ

inductive Presupposition.SyntacticEnvironment.Step.SameInitialString {Atom : Type u_1} : Step Atom → Step Atom → Prop

Two steps have the same initial string when a good final may turn one into the other, which it does by replacing the second argument of a first argument, and the connective unless it is if, which precedes its antecedent.

• not {Atom : Type u_1} : Step.not.SameInitialString Step.not
• right {Atom : Type u_1} (c : Connective) (F : Formula Atom) : (Step.right c F).SameInitialString (Step.right c F)
• left {Atom : Type u_1} {c c' : Connective} (hc : c = Connective.cond ↔ c' = Connective.cond) (G G' : Formula Atom) : (Step.left c G).SameInitialString (Step.left c' G')

theorem Presupposition.SyntacticEnvironment.Step.SameInitialString.refl {Atom : Type u_1} (s : Step Atom) : s.SameInitialString s

def Presupposition.SyntacticEnvironment.SameInitialString {Atom : Type u_1} (K K' : SyntacticEnvironment Atom) : Prop

SameInitialString K K' holds when K' keeps the material of K before the gap and replaces what follows it, so that it is K with another good final.

Equations

• K.SameInitialString K' = List.Forall₂ Presupposition.SyntacticEnvironment.Step.SameInitialString K K'

theorem Presupposition.SyntacticEnvironment.SameInitialString.refl {Atom : Type u_1} (K : SyntacticEnvironment Atom) : K.SameInitialString K

theorem Presupposition.SyntacticEnvironment.sameInitialString_append_singleton {Atom : Type u_1} {K L : SyntacticEnvironment Atom} {s : Step Atom} : (K ++ [s]).SameInitialString L ↔ ∃ (K' : SyntacticEnvironment Atom) (s' : Step Atom), L = K' ++ [s'] ∧ K.SameInitialString K' ∧ s.SameInitialString s'

A good final of K ++ [s] is a good final of K inside a good final of the outermost step.

Parsing points

def Presupposition.Connective.rightItems : Connective → ℕ

The number of items of the string that follow the first argument of a connective is two for a conjunction or a disjunction, the connective and the second argument, and one for if, the consequent, since if precedes its antecedent and its separator is forced.

Equations

• Presupposition.Connective.cond.rightItems = 1
• x✝.rightItems = 2

def Presupposition.SyntacticEnvironment.Step.rightItems {Atom : Type u_1} : Step Atom → ℕ

The number of items of the string after the gap of a step; only closing brackets, which are forced, follow the argument of a negation and the second argument of a connective.

Equations

• (Presupposition.SyntacticEnvironment.Step.left c G).rightItems = c.rightItems
• x✝.rightItems = 0

def Presupposition.SyntacticEnvironment.rightItems {Atom : Type u_1} (K : SyntacticEnvironment Atom) : ℕ

The number of items of the string after the gap.

Equations

• K.rightItems = (List.map Presupposition.SyntacticEnvironment.Step.rightItems K).sum

@[simp]

theorem Presupposition.SyntacticEnvironment.rightItems_nil {Atom : Type u_1} : rightItems [] = 0

@[simp]

theorem Presupposition.SyntacticEnvironment.rightItems_cons {Atom : Type u_1} (s : Step Atom) (K : SyntacticEnvironment Atom) : rightItems (s :: K) = s.rightItems + K.rightItems

theorem Presupposition.SyntacticEnvironment.rightItems_append {Atom : Type u_1} (K K' : SyntacticEnvironment Atom) : (K ++ K').rightItems = K.rightItems + K'.rightItems

def Presupposition.SyntacticEnvironment.Step.AgreeUpTo {Atom : Type u_1} (n : ℕ) : Step Atom → Step Atom → Prop

s' keeps the material of s before the gap and its first n items after it.

Equations

• One or more equations did not get rendered due to their size.
• Presupposition.SyntacticEnvironment.Step.AgreeUpTo n Presupposition.SyntacticEnvironment.Step.not x✝ = (x✝ = Presupposition.SyntacticEnvironment.Step.not)
• Presupposition.SyntacticEnvironment.Step.AgreeUpTo n (Presupposition.SyntacticEnvironment.Step.right c F) x✝ = (x✝ = Presupposition.SyntacticEnvironment.Step.right c F)

def Presupposition.SyntacticEnvironment.AgreeUpTo {Atom : Type u_1} : ℕ → SyntacticEnvironment Atom → SyntacticEnvironment Atom → Prop

AgreeUpTo n K K' holds when K' keeps the material of K before the gap and the first n items after it, so that it is K with a good final of the string up to the n-th item, the parsing points of [Kal23].

Equations

• One or more equations did not get rendered due to their size.
• Presupposition.SyntacticEnvironment.AgreeUpTo x✝¹ [] x✝ = (x✝ = [])

theorem Presupposition.SyntacticEnvironment.Step.agreeUpTo_zero_iff {Atom : Type u_1} {s s' : Step Atom} : AgreeUpTo 0 s s' ↔ s.SameInitialString s'

theorem Presupposition.SyntacticEnvironment.agreeUpTo_zero_iff {Atom : Type u_1} {K K' : SyntacticEnvironment Atom} : AgreeUpTo 0 K K' ↔ K.SameInitialString K'

The first parsing point, right after the trigger, admits every good final.

theorem Presupposition.SyntacticEnvironment.Step.AgreeUpTo.refl {Atom : Type u_1} (n : ℕ) (s : Step Atom) : AgreeUpTo n s s

theorem Presupposition.SyntacticEnvironment.AgreeUpTo.refl {Atom : Type u_1} (n : ℕ) (K : SyntacticEnvironment Atom) : AgreeUpTo n K K

theorem Presupposition.SyntacticEnvironment.Step.AgreeUpTo.mono {Atom : Type u_1} {m n : ℕ} {s s' : Step Atom} (h : AgreeUpTo m s s') (hnm : n ≤ m) : AgreeUpTo n s s'

theorem Presupposition.SyntacticEnvironment.AgreeUpTo.mono {Atom : Type u_1} {m n : ℕ} {K K' : SyntacticEnvironment Atom} (h : AgreeUpTo m K K') (hnm : n ≤ m) : AgreeUpTo n K K'

theorem Presupposition.SyntacticEnvironment.Step.agreeUpTo_iff_eq {Atom : Type u_1} {n : ℕ} {s s' : Step Atom} (hn : s.rightItems ≤ n) : AgreeUpTo n s s' ↔ s' = s

theorem Presupposition.SyntacticEnvironment.agreeUpTo_iff_eq {Atom : Type u_1} {n : ℕ} {K K' : SyntacticEnvironment Atom} (hn : K.rightItems ≤ n) : AgreeUpTo n K K' ↔ K' = K

From the last parsing point on, only the environment itself agrees.

theorem Presupposition.SyntacticEnvironment.agreeUpTo_append_singleton {Atom : Type u_1} {n : ℕ} {K L : SyntacticEnvironment Atom} {s : Step Atom} : AgreeUpTo n (K ++ [s]) L ↔ ∃ (K' : SyntacticEnvironment Atom) (s' : Step Atom), L = K' ++ [s'] ∧ AgreeUpTo n K K' ∧ Step.AgreeUpTo (n - K.rightItems) s s'

A good final of K ++ [s] up to a parsing point is a good final of K inside one of s.

The continuations at a parsing point

def Presupposition.SyntacticEnvironment.continuations {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (K : SyntacticEnvironment Atom) : ℕ∞ → Set (Set W → Set W)

The continuations at parsing point n after the gap of K: the truth functions of the good finals that keep the first n items after the gap, and at the last parsing point the sentence's own.

Equations

• One or more equations did not get rendered due to their size.
• Presupposition.SyntacticEnvironment.continuations I K none = {Presupposition.SyntacticEnvironment.truth I K}

@[simp]

theorem Presupposition.SyntacticEnvironment.continuations_top {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (K : SyntacticEnvironment Atom) : continuations I K ⊤ = {truth I K}

theorem Presupposition.SyntacticEnvironment.continuations_natCast {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (n : ℕ) (K : SyntacticEnvironment Atom) : continuations I K ↑n = (fun (x : SyntacticEnvironment Atom) => truth I x) '' {K' : SyntacticEnvironment Atom | AgreeUpTo n K K'}

theorem Presupposition.SyntacticEnvironment.continuations_zero {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (K : SyntacticEnvironment Atom) : continuations I K 0 = (fun (x : SyntacticEnvironment Atom) => truth I x) '' {K' : SyntacticEnvironment Atom | K.SameInitialString K'}

The first parsing point consults every good final.

theorem Presupposition.SyntacticEnvironment.truth_mem_continuations {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (n : ℕ∞) (K : SyntacticEnvironment Atom) : truth I K ∈ continuations I K n

theorem Presupposition.SyntacticEnvironment.antitone_continuations {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (K : SyntacticEnvironment Atom) : Antitone (continuations I K)

A later parsing point consults fewer continuations.

theorem Presupposition.SyntacticEnvironment.continuations_eq_top_of_le {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {n : ℕ} {K : SyntacticEnvironment Atom} (hn : K.rightItems ≤ n) : continuations I K ↑n = continuations I K ⊤

From the last item after the gap on, a parsing point consults only the sentence itself.

def Presupposition.Formula.triggers {Atom : Type u_1} : Formula Atom → List (SyntacticEnvironment Atom × Atom × Atom)

The triggers of a formula, each with its environment and its presupposition and assertion, so that K.fill (trigger p p') = F for every (K, p, p') listed.

Equations

• One or more equations did not get rendered due to their size.
• (Presupposition.Formula.atom p).triggers = []
• (Presupposition.Formula.trigger p p').triggers = [([], p, p')]
• F.not.triggers = List.map (fun (o : Presupposition.SyntacticEnvironment Atom × Atom × Atom) => (o.1 ++ [Presupposition.SyntacticEnvironment.Step.not], o.2)) F.triggers

@[simp]

theorem Presupposition.Formula.triggers_accommodate {Atom : Type u_1} (F : Formula Atom) : F.accommodate.triggers = []

Local accommodation leaves no trigger.

theorem Presupposition.Formula.fill_of_mem_triggers {Atom : Type u_1} {F : Formula Atom} {o : SyntacticEnvironment Atom × Atom × Atom} (h : o ∈ F.triggers) : o.1.fill (trigger o.2.1 o.2.2) = F

def Presupposition.SyntacticEnvironment.TriggerFreeFinal {Atom : Type u_1} (K : SyntacticEnvironment Atom) : Prop

The material after the gap of an environment contains no trigger.

Equations

• K.TriggerFreeFinal = ∀ (c : Presupposition.Connective) (G : Presupposition.Formula Atom), Presupposition.SyntacticEnvironment.Step.left c G ∈ K → G.triggers = []

theorem Presupposition.SyntacticEnvironment.triggerFreeFinal_append {Atom : Type u_1} {K K' : SyntacticEnvironment Atom} : (K ++ K').TriggerFreeFinal ↔ K.TriggerFreeFinal ∧ K'.TriggerFreeFinal

theorem Presupposition.SyntacticEnvironment.triggerFreeFinal_singleton {Atom : Type u_1} {s : Step Atom} : TriggerFreeFinal [s] ↔ ∀ (c : Connective) (G : Formula Atom), s = Step.left c G → G.triggers = []

Karttunen's local contexts from the good finals

theorem Presupposition.SyntacticEnvironment.isTruthFunctional_truth {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (K : SyntacticEnvironment Atom) : IsTruthFunctional (truth I K)

theorem Presupposition.SyntacticEnvironment.isTruthFunctional_of_mem_continuations {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {n : ℕ∞} {K : SyntacticEnvironment Atom} {f : Set W → Set W} (hf : f ∈ continuations I K n) : IsTruthFunctional f

theorem Presupposition.SyntacticEnvironment.dependsAt_truth_cons {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {s : Step Atom} {K : SyntacticEnvironment Atom} {w : W} : DependsAt (truth I (s :: K)) w ↔ DependsAt (Step.truth I s) w ∧ DependsAt (truth I K) w

The formula's truth value depends on the gap of s :: K iff it depends on the gap of s and on the gap of K.

theorem Presupposition.SyntacticEnvironment.dependsAt_right_iff {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (c : Connective) (F : Formula Atom) (w : W) : DependsAt (Step.truth I (Step.right c F)) w ↔ w ∈ Step.localContext I (Step.right c F) Set.univ

The truth value depends on the second argument of a binary connective exactly in its local context.

theorem Presupposition.SyntacticEnvironment.exists_dependsAt_left {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) [Nonempty Atom] (c : Connective) (w : W) : ∃ (G : Formula Atom), DependsAt (Step.truth I (Step.left c G)) w

Some second argument makes the truth value depend on the first argument of a binary connective.

theorem Presupposition.SyntacticEnvironment.exists_dependsAt_iff {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) [Nonempty Atom] (K : SyntacticEnvironment Atom) (w : W) : (∃ (K' : SyntacticEnvironment Atom), K.SameInitialString K' ∧ DependsAt (truth I K') w) ↔ w ∈ localContext I K Set.univ

Some good final makes the truth value at w depend on the gap of K iff w is in [Kar74a]'s local context of the gap.

theorem Presupposition.Formula.middleKleene_ne_zero_iff {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (F : Formula Atom) (w : W) : middleKleene I F w ≠ 0 ↔ ∀ o ∈ F.triggers, w ∈ SyntacticEnvironment.localContext I o.1 Set.univ → w ∈ I o.2.1

The filtering evaluation is defined at w iff every trigger's presupposition holds there whenever w is in the trigger's [Kar74a] local context.

Occurrences

def Presupposition.SyntacticEnvironment.occurrence {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (K : SyntacticEnvironment Atom) (p p' : Atom) : Occurrence W (Set W)

The occurrence of the trigger trigger p p' at the gap of K, with the continuations of its parsing points.

Equations

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

def Presupposition.Formula.occurrences {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (F : Formula Atom) : List (Occurrence W (Set W))

The occurrences of the triggers of a formula.

Equations

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

theorem Presupposition.Formula.forall_mem_occurrences {Atom : Type u_1} {W : Type u_2} {I : Atom → Set W} {F : Formula Atom} {P : Occurrence W (Set W) → Prop} : (∀ o ∈ occurrences I F, P o) ↔ ∀ t ∈ F.triggers, P (SyntacticEnvironment.occurrence I t.1 t.2.1 t.2.2)