The focus particles only, even and too

This file defines the exclusive only, the additives such as too, and the scalar presupposition of even, with propositions as Set W. Following Coppock and Beaver, only relates its prejacent to a set of alternative propositions ranked by strength: it presupposes that some true alternative is at least as strong as the prejacent and asserts that no true alternative is stronger. On the entailment scale the assertion is the exclusion Exhaustification.excludes, and with the prejacent among the alternatives the presupposition is the prejacent itself, von Fintel's entry for propositional only; on the identity scale the assertion is Rooth's.

An additive particle asserts its prejacent and presupposes what only asserts to be false, that some true alternative lies beyond the prejacent on the scale. On the identity scale this is Rullmann's true alternative other than the prejacent, and on the entailment scale Beaver and Clark's true alternative that the prejacent does not entail, the stronger of the two.

A likelihood is a monotone map from propositions into a partial order, so that a stronger proposition is at most as likely; the presupposition of even, after Karttunen and Peters, is that the prejacent is less likely than every focus alternative.

Main definitions

• Focus.Particles.atLeast, Focus.Particles.atMost: some true alternative is at least as strong as the prejacent, and no true alternative is stronger.
• Focus.Particles.only: the exclusive, presupposing atLeast and asserting atMost.
• Focus.Particles.additivePresup, Focus.Particles.additive: the presupposition of an additive particle, the complement of atMost, and the additive, presupposing it and asserting the prejacent.
• Focus.Particles.evenPresup: the prejacent is less likely than every alternative.

Main results

• Focus.Particles.only_subset_eq, Focus.Particles.posExt_only_subset: on the entailment scale only presupposes its prejacent and asserts the exclusion, and is true exactly where the exhaustification Exhaustification.exh is.
• Focus.Particles.atMost_eq_eq_atMost_subset: the identity-scale assertion is the entailment-scale one when the prejacent entails no other alternative.
• Focus.Particles.antitone_atMost: on a scale refining entailment, strengthening the prejacent strengthens the assertion.
• Focus.Particles.additivePresup_eq_compl_atMost, Focus.Particles.only_eq_one_iff_additive_ne_one: the additive presupposes what only denies, so where the prejacent and the presupposition of only hold, exactly one of the two is true.
• Focus.Particles.additivePresup_subset_eq_empty, Focus.Particles.mem_additivePresup_eq: an alternative the prejacent entails satisfies the identity-scale presupposition but not the entailment-scale one, Beaver and Clark's Sam is happy. #He's ecstatic too.
• Focus.Particles.not_evenPresup_of_subset: under a monotone likelihood an alternative that entails the prejacent refutes the presupposition of even, the clash from which Lahiri derives the distribution of even one items.
• Focus.Particles.evenPresup_iff_ne: when the prejacent entails every alternative, the presupposition asks only that no alternative be exactly as likely.

Implementation notes

The scale is a relation S, with S q p read as q being at least as strong as p; the entailment scale is (· ⊆ ·). Coppock and Beaver's existential presupposition is used rather than Beaver and Clark's, which also requires the lower-ranked alternatives to be false. Francescotti weakens the universal force of the presupposition of even to a majority threshold, in Studies/Francescotti1995.lean. The presupposition of an additive is existential and pointwise; Kripke, and Beaver and Clark after him, argue that too needs a salient antecedent in the discourse, which is not modelled here.

References

• [CB14]
• [BC08]
• [Kri09c]
• [Roo92]
• [Rul03]
• [vF99a]
• [KP79]
• [Lah98]
• [Crn14]
• [Fra95]

Only

def Focus.Particles.atLeast {W : Type u_1} (S : Set W → Set W → Prop) (C : Set (Set W)) (p : Set W) : Set W

atLeast S C p holds where some true alternative in C is at least as strong as p on the scale S ([CB14]'s MIN).

Equations

• Focus.Particles.atLeast S C p = {w : W | ∃ q ∈ C, w ∈ q ∧ S q p}

def Focus.Particles.atMost {W : Type u_1} (S : Set W → Set W → Prop) (C : Set (Set W)) (p : Set W) : Set W

atMost S C p holds where every true alternative in C is at most as strong as p on the scale S ([CB14]'s MAX).

Equations

• Focus.Particles.atMost S C p = {w : W | ∀ q ∈ C, w ∈ q → S p q}

noncomputable def Focus.Particles.only {W : Type u_1} (S : Set W → Set W → Prop) (C : Set (Set W)) (p : Set W) : W → SignType

Only p over the alternatives C ranked by S presupposes atLeast S C p and asserts atMost S C p ([CB14]'s (73)).

Equations

• Focus.Particles.only S C p = (Focus.Particles.atLeast S C p).indicator fun (w : W) => SignType.ofProp (w ∈ Focus.Particles.atMost S C p)

@[simp]

theorem Focus.Particles.mem_atLeast {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} {w : W} : w ∈ atLeast S C p ↔ ∃ q ∈ C, w ∈ q ∧ S q p

@[simp]

theorem Focus.Particles.mem_atMost {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} {w : W} : w ∈ atMost S C p ↔ ∀ q ∈ C, w ∈ q → S p q

@[simp]

theorem Focus.Particles.only_eq_zero_iff {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} {w : W} : only S C p w = 0 ↔ w ∉ atLeast S C p

theorem Focus.Particles.support_only {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} : Function.support (only S C p) = atLeast S C p

Only is defined exactly where its presupposition atLeast S C p holds.

@[simp]

theorem Focus.Particles.only_eq_one_iff {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} {w : W} : only S C p w = 1 ↔ w ∈ atLeast S C p ∧ w ∈ atMost S C p

@[simp]

theorem Focus.Particles.only_eq_neg_one_iff {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} {w : W} : only S C p w = -1 ↔ w ∈ atLeast S C p ∧ w ∉ atMost S C p

theorem Focus.Particles.notMem_atMost {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p q : Set W} {w : W} (hq : q ∈ C) (hw : w ∈ q) (h : ¬S p q) : w ∉ atMost S C p

A true alternative that p does not reach on the scale refutes the assertion.

theorem Focus.Particles.antitone_atMost {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} (hS : ∀ ⦃p q r : Set W⦄, p ⊆ q → S q r → S p r) : Antitone (atMost S C)

On a scale on which a weaker proposition never outranks a stronger one, strengthening the prejacent strengthens the assertion.

The entailment scale

theorem Focus.Particles.atMost_subset {W : Type u_1} {C : Set (Set W)} {p : Set W} : atMost (fun (x1 x2 : Set W) => x1 ⊆ x2) C p = Exhaustification.excludes C p

On the entailment scale the assertion is the exclusion Exhaustification.excludes.

theorem Focus.Particles.atLeast_subset_subset {W : Type u_1} {C : Set (Set W)} {p : Set W} : atLeast (fun (x1 x2 : Set W) => x1 ⊆ x2) C p ⊆ p

On the entailment scale the presupposition entails the prejacent.

theorem Focus.Particles.atLeast_subset_eq {W : Type u_1} {C : Set (Set W)} {p : Set W} (hp : p ∈ C) : atLeast (fun (x1 x2 : Set W) => x1 ⊆ x2) C p = p

On the entailment scale, with the prejacent among the alternatives, the presupposition is the prejacent.

theorem Focus.Particles.only_subset_eq {W : Type u_1} {C : Set (Set W)} {p : Set W} (hp : p ∈ C) : only (fun (x1 x2 : Set W) => x1 ⊆ x2) C p = p.indicator fun (w : W) => SignType.ofProp (w ∈ Exhaustification.excludes C p)

On the entailment scale, with the prejacent among the alternatives, only presupposes its prejacent and asserts the exclusion ([vF99a]'s (68a)).

theorem Focus.Particles.posExt_only_subset {W : Type u_1} {C : Set (Set W)} {p : Set W} (hp : p ∈ C) : Trivalent.posExt (only (fun (x1 x2 : Set W) => x1 ⊆ x2) C p) = Exhaustification.exh C p

On the entailment scale only is true exactly where the exhaustification Exhaustification.exh is.

The identity scale

theorem Focus.Particles.atMost_eq_eq_atMost_subset {W : Type u_1} {C : Set (Set W)} {p : Set W} (h : ∀ q ∈ C, p ⊆ q → q = p) : atMost (fun (x1 x2 : Set W) => x1 = x2) C p = atMost (fun (x1 x2 : Set W) => x1 ⊆ x2) C p

When the prejacent entails no other alternative, the identity-scale assertion, that every true alternative is the prejacent, is the entailment-scale one.

Additives

def Focus.Particles.additivePresup {W : Type u_1} (S : Set W → Set W → Prop) (C : Set (Set W)) (p : Set W) : Set W

additivePresup S C p holds where some true alternative in C is one that p does not reach on the scale S, on the identity scale an alternative other than the prejacent ([Rul03]'s (15)) and on the entailment scale one that the prejacent does not entail ([BC08]).

Equations

• Focus.Particles.additivePresup S C p = {w : W | ∃ q ∈ C, w ∈ q ∧ ¬S p q}

noncomputable def Focus.Particles.additive {W : Type u_1} (S : Set W → Set W → Prop) (C : Set (Set W)) (p : Set W) : W → SignType

An additive particle, too or also, presupposes additivePresup S C p and asserts its prejacent p.

Equations

• Focus.Particles.additive S C p = (Focus.Particles.additivePresup S C p).indicator fun (w : W) => SignType.ofProp (w ∈ p)

@[simp]

theorem Focus.Particles.mem_additivePresup {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} {w : W} : w ∈ additivePresup S C p ↔ ∃ q ∈ C, w ∈ q ∧ ¬S p q

theorem Focus.Particles.additivePresup_eq_compl_atMost {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} : additivePresup S C p = (atMost S C p)ᶜ

The additive presupposes exactly what only asserts to be false.

@[simp]

theorem Focus.Particles.additive_eq_zero_iff {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} {w : W} : additive S C p w = 0 ↔ w ∉ additivePresup S C p

theorem Focus.Particles.support_additive {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} : Function.support (additive S C p) = additivePresup S C p

The additive is defined exactly where its presupposition holds.

@[simp]

theorem Focus.Particles.additive_eq_one_iff {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} {w : W} : additive S C p w = 1 ↔ w ∈ additivePresup S C p ∧ w ∈ p

@[simp]

theorem Focus.Particles.additive_eq_neg_one_iff {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} {w : W} : additive S C p w = -1 ↔ w ∈ additivePresup S C p ∧ w ∉ p

theorem Focus.Particles.only_eq_one_iff_additive_ne_one {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} {w : W} (hw : w ∈ p) (hl : w ∈ atLeast S C p) : only S C p w = 1 ↔ additive S C p w ≠ 1

Where the prejacent and the presupposition of only hold, only is true exactly where the additive is not.

theorem Focus.Particles.additivePresup_mono {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} {C' : Set (Set W)} (h : C ⊆ C') : additivePresup S C p ⊆ additivePresup S C' p

More alternatives make the presupposition easier to satisfy.

theorem Focus.Particles.additivePresup_insert_self {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} (h : S p p) : additivePresup S (insert p C) p = additivePresup S C p

On a reflexive scale the prejacent is never its own witness.

theorem Focus.Particles.additivePresup_anti {W : Type u_1} {S : Set W → Set W → Prop} {C : Set (Set W)} {p : Set W} {S' : Set W → Set W → Prop} (h : ∀ (p q : Set W), S p q → S' p q) : additivePresup S' C p ⊆ additivePresup S C p

A scale relating more propositions gives a stronger presupposition.

theorem Focus.Particles.additivePresup_subset_subset_eq {W : Type u_1} {C : Set (Set W)} {p : Set W} : additivePresup (fun (x1 x2 : Set W) => x1 ⊆ x2) C p ⊆ additivePresup (fun (x1 x2 : Set W) => x1 = x2) C p

The entailment-scale presupposition is the stronger.

theorem Focus.Particles.additivePresup_subset_eq_empty {W : Type u_1} {C : Set (Set W)} {p : Set W} (h : ∀ q ∈ C, p ⊆ q) : additivePresup (fun (x1 x2 : Set W) => x1 ⊆ x2) C p = ∅

When the prejacent entails every alternative the entailment-scale presupposition fails, as in Sam is happy. #He's ecstatic too ([BC08]'s (3.39)).

theorem Focus.Particles.mem_additivePresup_eq {W : Type u_1} {C : Set (Set W)} {p q : Set W} {w : W} (hq : q ∈ C) (hw : w ∈ q) (hne : q ≠ p) : w ∈ additivePresup (fun (x1 x2 : Set W) => x1 = x2) C p

A true alternative other than the prejacent satisfies the identity-scale presupposition, even one that the prejacent entails.

theorem Focus.Particles.additivePresup_eq_eq_subset {W : Type u_1} {C : Set (Set W)} {p : Set W} (h : ∀ q ∈ C, p ⊆ q → q = p) : additivePresup (fun (x1 x2 : Set W) => x1 = x2) C p = additivePresup (fun (x1 x2 : Set W) => x1 ⊆ x2) C p

When the prejacent entails no other alternative, the two scales give the same presupposition.

Even

def Focus.Particles.evenPresup {W : Type u_1} {α : Type u_2} [PartialOrder α] (μ : Set W → α) (p : Set W) (alts : Set (Set W)) : Prop

The scalar presupposition of even ([KP79]) under a likelihood μ holds when the prejacent p is less likely than every focus alternative.

Equations

• Focus.Particles.evenPresup μ p alts = ∀ q ∈ alts, μ p < μ q

theorem Focus.Particles.not_evenPresup_of_subset {W : Type u_1} {α : Type u_2} [PartialOrder α] {μ : Set W → α} {p q : Set W} {alts : Set (Set W)} (hμ : Monotone μ) (hq : q ∈ alts) (hqp : q ⊆ p) : ¬evenPresup μ p alts

Under a likelihood respecting entailment, an alternative that entails the prejacent is at least as likely and so refutes the presupposition of even.

theorem Focus.Particles.evenPresup_iff_ne {W : Type u_1} {α : Type u_2} [PartialOrder α] {μ : Set W → α} {p : Set W} {alts : Set (Set W)} (hμ : Monotone μ) (h : ∀ q ∈ alts, p ⊆ q) : evenPresup μ p alts ↔ ∀ q ∈ alts, μ p ≠ μ q

When the prejacent entails every alternative, the presupposition of even asks only that no alternative be exactly as likely.