Presuppositional exhaustification

The presuppositional exhaustivity operator pex^{IE+II} of Del Pinal, Bassi and Sauerland, extending the pex^{IE} of Bassi, Del Pinal and Sauerland, asserts its prejacent alone. It presupposes that the relevant innocently excludable alternatives are false and that the relevant innocently includable ones other than the prejacent are homogeneous, true together or false together, so negation denies the assertion and leaves the presupposition. When the prejacent lies between the meet and the join of those alternatives, as ◇(p ∨ q) lies between ◇p ∧ ◇q and ◇p ∨ ◇q, homogeneity makes it true where all of them are and false where none is.

Main declarations

• pexIEII: the operator.
• pexIEII_eq_one_iff_forall_mem, pexIEII_eq_neg_one_iff_forall_notMem: a prejacent between the meet and the join of its relevant includable alternatives is true together with all of them and false together with all of them.

References

• [DPBS24]
• [BDPS21]
• [BLF20]

noncomputable def Exhaustification.pexIEII {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (Rc : Set (Set World)) : World → SignType

pex^{IE+II} asserts the prejacent and presupposes that the innocently excludable alternatives in the relevance set Rc are false and that the innocently includable ones in it, other than the prejacent, are homogeneous.

Equations

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

theorem Exhaustification.pexIEII_ne_zero_iff {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {Rc : Set (Set World)} {w : World} : pexIEII ALT φ Rc w ≠ 0 ↔ (∀ (ψ : Set World), IsInnocentlyExcludable ALT φ ψ → ψ ∈ Rc → w ∉ ψ) ∧ Homogeneity.Homogeneous (II ALT φ \ {φ} ∩ Rc) w

pex^{IE+II} is defined where the excludable alternatives in Rc are false and the includable ones in it other than the prejacent are homogeneous.

theorem Exhaustification.pexIEII_eq_one_iff {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {Rc : Set (Set World)} {w : World} : pexIEII ALT φ Rc w = 1 ↔ pexIEII ALT φ Rc w ≠ 0 ∧ w ∈ φ

pex^{IE+II} asserts its prejacent.

theorem Exhaustification.pexIEII_eq_neg_one_iff {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {Rc : Set (Set World)} {w : World} : pexIEII ALT φ Rc w = -1 ↔ pexIEII ALT φ Rc w ≠ 0 ∧ w ∉ φ

Negated, pex^{IE+II} denies its prejacent and keeps its presupposition.

theorem Exhaustification.pexIEII_eq_one_iff_forall_mem {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {Rc : Set (Set World)} {w : World} (hl : ⋂₀ (II ALT φ \ {φ} ∩ Rc) ⊆ φ) (hu : φ ⊆ ⋃₀ (II ALT φ \ {φ} ∩ Rc)) : pexIEII ALT φ Rc w = 1 ↔ pexIEII ALT φ Rc w ≠ 0 ∧ ∀ α ∈ II ALT φ \ {φ} ∩ Rc, w ∈ α

A prejacent between the meet and the join of its relevant includable alternatives is true under pex exactly where the presupposition holds and all of them are true.

theorem Exhaustification.pexIEII_eq_neg_one_iff_forall_notMem {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {Rc : Set (Set World)} {w : World} (hl : ⋂₀ (II ALT φ \ {φ} ∩ Rc) ⊆ φ) (hu : φ ⊆ ⋃₀ (II ALT φ \ {φ} ∩ Rc)) : pexIEII ALT φ Rc w = -1 ↔ pexIEII ALT φ Rc w ≠ 0 ∧ ∀ α ∈ II ALT φ \ {φ} ∩ Rc, w ∉ α

A prejacent between the meet and the join of its relevant includable alternatives is false under pex exactly where the presupposition holds and all of them are false.

theorem Exhaustification.pexIEII_ne_zero_iff_of_inter_eq_empty {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {Rc : Set (Set World)} {w : World} (h : II ALT φ \ {φ} ∩ Rc = ∅) : pexIEII ALT φ Rc w ≠ 0 ↔ ∀ (ψ : Set World), IsInnocentlyExcludable ALT φ ψ → ψ ∈ Rc → w ∉ ψ

With no relevant includable alternative besides the prejacent, as for a basic scalar sentence, the presupposition is that the relevant excludable alternatives are false.