Kalomoiros (2023): Presupposition and Its (A-)Symmetries

Limited Symmetry is a theory of presupposition projection that checks Transparency at every point of the parse after a trigger. At a parsing point a sentence is stably true (false) at a world when every good final of the string up to that point makes it true (false) there. The constraint requires, at every trigger, every parsing point after it and every assertion, that the worlds of the context where the sentence is stably true (false) stay so when the trigger is replaced by its assertion: the presupposition is stably transparent for the good finals at each parsing point (Presupposition.StablyTransparent). This file covers the dissertation's first system, over the propositional fragment of Schlenker's language.

The good finals at the first parsing point after a trigger are all of Schlenker's incremental ones, and at the last only the sentence itself, so Limited Symmetry lies between Schlenker's incremental and symmetric Transparency (LimitedSymmetry.of_transparency, LimitedSymmetry.transparency). The constraint is stated on the occurrences of a sentence's triggers (Presupposition.Occurrence), so it applies as it stands wherever a sentence type supplies its occurrences and their parsing points.

Main statements

• limitedSymmetry_and_left, limitedSymmetry_and_right, limitedSymmetry_or_left: conjunction is asymmetric, a trigger in the first conjunct needing the context to entail its presupposition and one in the second only that the first conjunct does, while a first disjunct is filtered by the second.
• limitedSymmetry_not, limitedSymmetry_if_not_left_iff_or: a negated sentence respects the constraint iff the sentence does, but a negation inside a coordination changes its polarity, so that a conditional with a negated antecedent behaves like a disjunction.
• limitedSymmetryAt_iff, limitedSymmetryAt_iff_funs: the constraint is checked world by world, on the truth functions the good finals realize there, which makes each of the dissertation's facts a computation.
• LimitedSymmetry.of_transparency, LimitedSymmetry.transparency: incremental Transparency implies Limited Symmetry, which implies symmetric Transparency.

Implementation notes

• A trigger trigger p a presupposes p and asserts a. The dissertation writes p'p with the prime on the presupposition, the reverse of Schlenker's convention.
• The parsing points after a trigger are represented by SyntacticEnvironment.AgreeUpTo, which counts the connective after a first argument and the second argument as one item each and ignores closing brackets. Points inside the second argument add no condition, since the constraint is checked world by world and the argument's value at a world is either still open or already fixed.
• A context is a set of worlds, and the assertions the constraint quantifies over are propositions.

TODO

• Two conditions printed in the dissertation differ from what the constraint gives, for a conditional whose antecedent conjoins a negated trigger (not_limitedSymmetry_if_not_and_of_printed) and for the second trigger of a conjunction with a negated first conjunct (not_limitedSymmetryAt_not_and_second_of_printed).
• Facts 3.4.7 and 3.4.9, stated for arbitrary sentences, are not formalized, nor is the postposed conditional of Fact 3.4.6, which is outside the language.

References

• [Kal23]
• [Sch09a]

The constraint

def Kalomoiros2023.LimitedSymmetryAt {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (C : Set W) (K : Presupposition.SyntacticEnvironment Atom) (p : Atom) : Prop

The constraint of Definition 3.4.4 at one trigger, with presupposition p at the gap of K. At every parsing point after the trigger and for every assertion D, the worlds where the sentence is stably true (false) are worlds where it is stably true (false) with the presupposition deleted: the presupposition is stably transparent at every parsing point.

Equations

• Kalomoiros2023.LimitedSymmetryAt I C K p = ∀ (n : ℕ∞), Presupposition.StablyTransparent C (Presupposition.SyntacticEnvironment.continuations I K n) (I p)

def Kalomoiros2023.LimitedSymmetry {W : Type u_2} {α : Type u_3} [SemilatticeInf α] (C : Set W) (os : List (Presupposition.Occurrence W α)) : Prop

A sentence satisfies Limited Symmetry in C when the constraint holds at every trigger (Definition 3.4.4).

Equations

• Kalomoiros2023.LimitedSymmetry C os = ∀ o ∈ os, ∀ (n : ℕ∞), o.StablyTransparent n C

theorem Kalomoiros2023.limitedSymmetry_occurrences_iff {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {F : Presupposition.Formula Atom} : LimitedSymmetry C (Presupposition.Formula.occurrences I F) ↔ ∀ t ∈ F.triggers, LimitedSymmetryAt I C t.1 t.2.1

theorem Kalomoiros2023.limitedSymmetryAt_iff_forall_le {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {K : Presupposition.SyntacticEnvironment Atom} {p : Atom} : LimitedSymmetryAt I C K p ↔ ∀ n ≤ K.rightItems, Presupposition.StablyTransparent C (Presupposition.SyntacticEnvironment.continuations I K ↑n) (I p)

The parsing points after a trigger are those up to the last item after the gap, as Definition 3.4.4 counts them; from there on only the sentence itself is consulted.

theorem Kalomoiros2023.limitedSymmetryAt_iff {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (C : Set W) (K : Presupposition.SyntacticEnvironment Atom) (p : Atom) : LimitedSymmetryAt I C K p ↔ ∀ w ∈ C, w ∉ I p → ∀ n ≤ K.rightItems, ((∀ (K' : Presupposition.SyntacticEnvironment Atom), Presupposition.SyntacticEnvironment.AgreeUpTo n K K' → w ∈ Presupposition.SyntacticEnvironment.truth I K' ∅) → ∀ (K' : Presupposition.SyntacticEnvironment Atom), Presupposition.SyntacticEnvironment.AgreeUpTo n K K' → w ∈ Presupposition.SyntacticEnvironment.truth I K' Set.univ) ∧ ((∀ (K' : Presupposition.SyntacticEnvironment Atom), Presupposition.SyntacticEnvironment.AgreeUpTo n K K' → w ∉ Presupposition.SyntacticEnvironment.truth I K' ∅) → ∀ (K' : Presupposition.SyntacticEnvironment Atom), Presupposition.SyntacticEnvironment.AgreeUpTo n K K' → w ∉ Presupposition.SyntacticEnvironment.truth I K' Set.univ)

The constraint is checked world by world. At a world where the presupposition fails, whenever every good final at a parsing point makes the sentence true (false) with a false gap, every good final makes it true (false) with a true gap.

Between incremental and symmetric Transparency

theorem Kalomoiros2023.LimitedSymmetry.of_transparency {W : Type u_2} {α : Type u_3} [SemilatticeInf α] {C : Set W} {os : List (Presupposition.Occurrence W α)} (h : Schlenker2009.Transparency Schlenker2009.Version.incremental C os) : LimitedSymmetry C os

Incremental Transparency implies Limited Symmetry, since every parsing point consults fewer continuations than the first.

theorem Kalomoiros2023.LimitedSymmetry.transparency {W : Type u_2} {α : Type u_3} [SemilatticeInf α] {C : Set W} {os : List (Presupposition.Occurrence W α)} (h : LimitedSymmetry C os) : Schlenker2009.Transparency Schlenker2009.Version.symmetric C os

Limited Symmetry implies symmetric Transparency, since at the last parsing point the only continuation is the sentence's own.

The truth functions of the good finals

def Kalomoiros2023.evalB : Presupposition.Connective → Bool → Bool → Bool

A connective's truth function on booleans.

Equations

• Kalomoiros2023.evalB Presupposition.Connective.conj x✝¹ x✝ = (x✝¹ && x✝)
• Kalomoiros2023.evalB Presupposition.Connective.cond x✝¹ x✝ = (!x✝¹ || x✝)
• Kalomoiros2023.evalB Presupposition.Connective.disj x✝¹ x✝ = (x✝¹ || x✝)

theorem Kalomoiros2023.decide_eval (c : Presupposition.Connective) (a b : Prop) : decide (c.eval a b) = evalB c (decide a) (decide b)

noncomputable def Kalomoiros2023.val {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (w : W) (F : Presupposition.Formula Atom) : Bool

The truth value at w of a formula.

Equations

• Kalomoiros2023.val I w F = decide (w ∈ Presupposition.Formula.truth I F)

def Kalomoiros2023.compat : Presupposition.Connective → List Presupposition.Connective

The connectives that may follow a first argument when no item after the gap is fixed.

Equations

• Kalomoiros2023.compat Presupposition.Connective.cond = [Presupposition.Connective.cond]
• Kalomoiros2023.compat x✝ = [Presupposition.Connective.conj, Presupposition.Connective.disj]

theorem Kalomoiros2023.mem_compat {c c' : Presupposition.Connective} : c' ∈ compat c ↔ (c = Presupposition.Connective.cond ↔ c' = Presupposition.Connective.cond)

noncomputable def Kalomoiros2023.stepFuns {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (w : W) (n : ℕ) : Presupposition.SyntacticEnvironment.Step Atom → List (Bool → Bool)

The truth functions at w of the good finals of a step up to parsing point n, as functions of the gap's truth value.

Equations

• One or more equations did not get rendered due to their size.
• Kalomoiros2023.stepFuns I w n Presupposition.SyntacticEnvironment.Step.not = [not]
• Kalomoiros2023.stepFuns I w n (Presupposition.SyntacticEnvironment.Step.right c F) = [Kalomoiros2023.evalB c (Kalomoiros2023.val I w F)]

noncomputable def Kalomoiros2023.funs {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (w : W) : ℕ → Presupposition.SyntacticEnvironment Atom → List (Bool → Bool)

The truth functions at w of the good finals of an environment up to parsing point n.

Equations

• One or more equations did not get rendered due to their size.
• Kalomoiros2023.funs I w x✝ [] = [id]

theorem Kalomoiros2023.forall_formula_iff {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) [Nonempty Atom] (w : W) (Q : Prop → Prop) : (∀ (G : Presupposition.Formula Atom), Q (w ∈ Presupposition.Formula.truth I G)) ↔ Q True ∧ Q False

A formula can be true or false at any world.

theorem Kalomoiros2023.forall_stepAgree_iff {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) [Nonempty Atom] (w : W) (n : ℕ) (s : Presupposition.SyntacticEnvironment.Step Atom) (X : Set W) (R : Bool → Prop) : (∀ (s' : Presupposition.SyntacticEnvironment.Step Atom), Presupposition.SyntacticEnvironment.Step.AgreeUpTo n s s' → R (decide (w ∈ Presupposition.SyntacticEnvironment.Step.truth I s' X))) ↔ ∀ f ∈ stepFuns I w n s, R (f (decide (w ∈ X)))

theorem Kalomoiros2023.forall_agreeUpTo_iff {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) [Nonempty Atom] (w : W) (n : ℕ) (K : Presupposition.SyntacticEnvironment Atom) (X : Set W) (R : Bool → Prop) : (∀ (K' : Presupposition.SyntacticEnvironment Atom), Presupposition.SyntacticEnvironment.AgreeUpTo n K K' → R (decide (w ∈ Presupposition.SyntacticEnvironment.truth I K' X))) ↔ ∀ f ∈ funs I w n K, R (f (decide (w ∈ X)))

The good finals at a parsing point realize, at each world, the truth functions funs.

theorem Kalomoiros2023.limitedSymmetryAt_iff_funs {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (C : Set W) (K : Presupposition.SyntacticEnvironment Atom) (p : Atom) : LimitedSymmetryAt I C K p ↔ ∀ w ∈ C, w ∉ I p → ∀ n ≤ K.rightItems, ((∀ f ∈ funs I w n K, f false = true) → ∀ f ∈ funs I w n K, f true = true) ∧ ((∀ f ∈ funs I w n K, f false = false) → ∀ f ∈ funs I w n K, f true = false)

Definition 3.4.4 world by world, as a condition on the truth functions of the good finals.

What the constraint requires

theorem Kalomoiros2023.limitedSymmetry_of_triggers {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {F : Presupposition.Formula Atom} {K : Presupposition.SyntacticEnvironment Atom} {p a : Atom} (h : F.triggers = [(K, p, a)]) : LimitedSymmetry C (Presupposition.Formula.occurrences I F) ↔ LimitedSymmetryAt I C K p

theorem Kalomoiros2023.limitedSymmetry_trigger {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p a : Atom} : LimitedSymmetry C (Presupposition.Formula.occurrences I (Presupposition.Formula.trigger p a)) ↔ C ⊆ I p

A trigger standing alone requires the context to entail its presupposition.

theorem Kalomoiros2023.limitedSymmetry_and_left {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p a q : Atom} : LimitedSymmetry C (Presupposition.Formula.occurrences I (Presupposition.Formula.bin Presupposition.Connective.conj (Presupposition.Formula.trigger p a) (Presupposition.Formula.atom q))) ↔ C ⊆ I p

(p'p and q) requires the context to entail p' (Fact 3.4.1, p. 124).

theorem Kalomoiros2023.limitedSymmetry_and_right {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p a q : Atom} : LimitedSymmetry C (Presupposition.Formula.occurrences I (Presupposition.Formula.bin Presupposition.Connective.conj (Presupposition.Formula.atom q) (Presupposition.Formula.trigger p a))) ↔ C ⊆ {w : W | w ∈ I q → w ∈ I p}

(q and p'p) requires the context to entail q → p' (Fact 3.4.2, p. 126).

theorem Kalomoiros2023.limitedSymmetry_or_left {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p a q : Atom} : LimitedSymmetry C (Presupposition.Formula.occurrences I (Presupposition.Formula.bin Presupposition.Connective.disj (Presupposition.Formula.trigger p a) (Presupposition.Formula.atom q))) ↔ C ⊆ {w : W | w ∉ I q → w ∈ I p}

(p'p or q) requires the context to entail ¬q → p' (Fact 3.4.3, p. 127).

theorem Kalomoiros2023.limitedSymmetry_if_left {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p a q : Atom} : LimitedSymmetry C (Presupposition.Formula.occurrences I (Presupposition.Formula.bin Presupposition.Connective.cond (Presupposition.Formula.trigger p a) (Presupposition.Formula.atom q))) ↔ C ⊆ I p

(if p'p. q) requires the context to entail p' (Fact 3.4.4, p. 128).

theorem Kalomoiros2023.limitedSymmetry_if_right {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p a q : Atom} : LimitedSymmetry C (Presupposition.Formula.occurrences I (Presupposition.Formula.bin Presupposition.Connective.cond (Presupposition.Formula.atom q) (Presupposition.Formula.trigger p a))) ↔ C ⊆ {w : W | w ∈ I q → w ∈ I p}

(if q. p'p) requires the context to entail q → p' (Fact 3.4.5, p. 129).

theorem Kalomoiros2023.limitedSymmetry_if_not_left {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p a q : Atom} : LimitedSymmetry C (Presupposition.Formula.occurrences I (Presupposition.Formula.bin Presupposition.Connective.cond (Presupposition.Formula.trigger p a).not (Presupposition.Formula.atom q))) ↔ C ⊆ {w : W | w ∉ I q → w ∈ I p}

(if (not p'p). q) requires the context to entail ¬q → p', as (p'p or q) does (the first half of Fact 3.4.10, p. 136).

theorem Kalomoiros2023.limitedSymmetry_if_not_left_iff_or {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p a q : Atom} : LimitedSymmetry C (Presupposition.Formula.occurrences I (Presupposition.Formula.bin Presupposition.Connective.cond (Presupposition.Formula.trigger p a).not (Presupposition.Formula.atom q))) ↔ LimitedSymmetry C (Presupposition.Formula.occurrences I (Presupposition.Formula.bin Presupposition.Connective.disj (Presupposition.Formula.trigger p a) (Presupposition.Formula.atom q)))

(if (not p'p). q) respects the constraint iff (p'p or q) does (Fact 3.4.10, p. 136).

theorem Kalomoiros2023.limitedSymmetry_if_not_and {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p a q r : Atom} : LimitedSymmetry C (Presupposition.Formula.occurrences I (Presupposition.Formula.bin Presupposition.Connective.cond (Presupposition.Formula.bin Presupposition.Connective.conj (Presupposition.Formula.trigger p a).not (Presupposition.Formula.atom q)) (Presupposition.Formula.atom r))) ↔ C ⊆ {w : W | w ∈ I q → w ∉ I r → w ∈ I p}

(if ((not p'p) and q). r) requires the context to entail (q ∧ ¬r) → p'. Fact 3.4.8 (p. 134) prints (q ∧ r) → p' and omits the derivation (not_limitedSymmetry_if_not_and_of_printed).

theorem Kalomoiros2023.not_limitedSymmetry_if_not_and_of_printed {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {p a q r : Atom} {w : W} (hq : w ∈ I q) (hr : w ∉ I r) (hp : w ∉ I p) : {w} ⊆ {w : W | w ∈ I q → w ∈ I r → w ∈ I p} ∧ ¬LimitedSymmetry {w} (Presupposition.Formula.occurrences I (Presupposition.Formula.bin Presupposition.Connective.cond (Presupposition.Formula.bin Presupposition.Connective.conj (Presupposition.Formula.trigger p a).not (Presupposition.Formula.atom q)) (Presupposition.Formula.atom r)))

The condition printed in Fact 3.4.8 is not the constraint's, since a context where q holds and r and p' fail entails (q ∧ r) → p' but violates the constraint.

theorem Kalomoiros2023.limitedSymmetryAt_and_first {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p q b : Atom} : LimitedSymmetryAt I C [Presupposition.SyntacticEnvironment.Step.left Presupposition.Connective.conj (Presupposition.Formula.trigger q b)] p ↔ C ⊆ I p

In (p'p and q'q) the first trigger requires the context to entail p' (Fact 3.4.11, p. 137).

theorem Kalomoiros2023.limitedSymmetryAt_not_and_first {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p q b : Atom} : LimitedSymmetryAt I C [Presupposition.SyntacticEnvironment.Step.not, Presupposition.SyntacticEnvironment.Step.left Presupposition.Connective.conj (Presupposition.Formula.trigger q b)] p ↔ C ⊆ {w : W | w ∈ I q → w ∈ I b → w ∈ I p}

In ((not p'p) and q'q) the first trigger requires the context to entail q'q → p' (Fact 3.4.12, p. 137).

theorem Kalomoiros2023.limitedSymmetryAt_not_and_second {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p a q : Atom} : LimitedSymmetryAt I C [Presupposition.SyntacticEnvironment.Step.right Presupposition.Connective.conj (Presupposition.Formula.trigger p a).not] q ↔ C ⊆ {w : W | w ∉ I p ∩ I a → w ∈ I q}

In ((not p'p) and q'q) the second trigger requires the context to entail (not p'p) → q', filtering by the first conjunct. Fact 3.4.12 (p. 137) prints p'p → q'.

theorem Kalomoiros2023.limitedSymmetryAt_or_first {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p q b : Atom} : LimitedSymmetryAt I C [Presupposition.SyntacticEnvironment.Step.left Presupposition.Connective.disj (Presupposition.Formula.trigger q b)] p ↔ C ⊆ {w : W | w ∈ I p ∨ w ∈ I q ∩ I b}

In (p'p or q'q) the first trigger requires the context to entail p' or q'q (Fact 3.4.13, p. 138).

theorem Kalomoiros2023.limitedSymmetryAt_or_second {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p a q : Atom} : LimitedSymmetryAt I C [Presupposition.SyntacticEnvironment.Step.right Presupposition.Connective.disj (Presupposition.Formula.trigger p a)] q ↔ C ⊆ {w : W | w ∈ I q ∨ w ∈ I p ∩ I a}

In (p'p or q'q) the second trigger requires the context to entail q' or p'p (Fact 3.4.13, p. 138).

theorem Kalomoiros2023.limitedSymmetryAt_not_or_first {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p q b : Atom} : LimitedSymmetryAt I C [Presupposition.SyntacticEnvironment.Step.not, Presupposition.SyntacticEnvironment.Step.left Presupposition.Connective.disj (Presupposition.Formula.trigger q b)] p ↔ C ⊆ I p

In ((not p'p) or q'q) the first trigger requires the context to entail p' (Fact 3.4.14, p. 138).

theorem Kalomoiros2023.limitedSymmetry_and_or {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} {p a q r : Atom} : LimitedSymmetry C (Presupposition.Formula.occurrences I (Presupposition.Formula.bin Presupposition.Connective.disj (Presupposition.Formula.bin Presupposition.Connective.conj (Presupposition.Formula.trigger p a) (Presupposition.Formula.atom q)) (Presupposition.Formula.atom r))) ↔ C ⊆ {w : W | w ∈ I q → w ∈ I p ∨ w ∈ I r}

((p'p and q) or r) requires the context to entail q → (p' ∨ r), the second conjunct filtering symmetrically, before the highest connective (Fact 3.4.15, p. 138).

theorem Kalomoiros2023.not_limitedSymmetryAt_not_and_second_of_printed {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {p a q : Atom} {w : W} (hp : w ∉ I p) (hq : w ∉ I q) : {w} ⊆ {w : W | w ∈ I p ∩ I a → w ∈ I q} ∧ ¬LimitedSymmetryAt I {w} [Presupposition.SyntacticEnvironment.Step.right Presupposition.Connective.conj (Presupposition.Formula.trigger p a).not] q

The condition printed in Fact 3.4.12 for the second trigger is not the constraint's, since a context where p' and q' fail entails p'p → q' but violates the constraint.

Negation

theorem Kalomoiros2023.forall_agreeUpTo_append_not {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {n : ℕ} {K : Presupposition.SyntacticEnvironment Atom} {w : W} {X : Set W} (P : Prop → Prop) : (∀ (L : Presupposition.SyntacticEnvironment Atom), Presupposition.SyntacticEnvironment.AgreeUpTo n (K ++ [Presupposition.SyntacticEnvironment.Step.not]) L → P (w ∈ Presupposition.SyntacticEnvironment.truth I L X)) ↔ ∀ (K' : Presupposition.SyntacticEnvironment Atom), Presupposition.SyntacticEnvironment.AgreeUpTo n K K' → P (w ∉ Presupposition.SyntacticEnvironment.truth I K' X)

theorem Kalomoiros2023.limitedSymmetry_not {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {C : Set W} (A : Presupposition.Formula Atom) : LimitedSymmetry C (Presupposition.Formula.occurrences I A.not) ↔ LimitedSymmetry C (Presupposition.Formula.occurrences I A)

A sentence respects the constraint iff its negation does (Proposition 3.4.1, p. 130).