Premise sets

Kratzer's premise semantics: a premise set is a list of propositions over an index type, a proposition follows from it when it holds throughout the set's intersection, and the set is consistent when that intersection is inhabited. Must and can in view of a conversational background f are consequence from, and compatibility with, f i (Definitions 5 and 6); when f i may be inconsistent they are restated over its consistent sublists (Definitions 7 and 8), and the two pairs agree on consistent backgrounds. Nothing here commits to what an index is: worlds, situations, or times.

Main definitions

• propIntersection A: the indices satisfying every member of A, Kratzer's ⋂A.
• followsFrom p A, isConsistent A, isCompatibleWith p A.
• mustInView, canInView: Definitions 5 and 6.
• mustInView', canInView': Definitions 7 and 8, over consistentSublists.

Main results

• mustInView_iff_mustInView'_of_consistent, canInView_iff_canInView'_of_consistent: the revised operators agree with the original ones on a consistent premise set.
• canInView_iff_not_mustInView_not, canInView'_iff_not_mustInView'_not: each pair of operators is dual, can being the negation of must not.
• canInView'_of_mem, mustInView'_of_forall_isCompatibleWith: Definition 8 holds of a premise itself, and Definition 7 of a premise compatible with every consistent sublist.

References

• [A. Kratzer, What 'must' and 'can' must and can mean (1977)][kratzer-1977]
• [A. Kratzer, Modals and Conditionals (2012)][kratzer-2012]

Primitives on premise sets

def Modality.Kratzer.propIntersection {W : Type u_1} (props : List (W → Prop)) : Set W

The intersection of a list of propositions: indices satisfying all of them.

Equations

• Modality.Kratzer.propIntersection props = {i : W | ∀ p ∈ props, p i}

def Modality.Kratzer.followsFrom {W : Type u_1} (p : W → Prop) (A : List (W → Prop)) : Prop

A proposition p follows from a premise set A iff ⋂ A ⊆ {i | p i} ([kratzer-1977] p. 31).

Equations

• Modality.Kratzer.followsFrom p A = (Modality.Kratzer.propIntersection A ⊆ {i : W | p i})

def Modality.Kratzer.isConsistent {W : Type u_1} (A : List (W → Prop)) : Prop

A premise set is consistent iff ⋂ A is non-empty ([kratzer-1977] p. 31).

Equations

• Modality.Kratzer.isConsistent A = (Modality.Kratzer.propIntersection A).Nonempty

def Modality.Kratzer.isCompatibleWith {W : Type u_1} (p : W → Prop) (A : List (W → Prop)) : Prop

A proposition p is compatible with A iff A ∪ {p} is consistent.

Equations

• Modality.Kratzer.isCompatibleWith p A = Modality.Kratzer.isConsistent (p :: A)

theorem Modality.Kratzer.mem_propIntersection {W : Type u_1} {A : List (W → Prop)} {i : W} : i ∈ propIntersection A ↔ ∀ p ∈ A, p i

theorem Modality.Kratzer.propIntersection_subset {W : Type u_1} {x : W → Prop} {A : List (W → Prop)} (hx : x ∈ A) : propIntersection A ⊆ {i : W | x i}

The intersection of a premise set is contained in each of its members.

theorem Modality.Kratzer.propIntersection_nil {W : Type u_1} : propIntersection [] = Set.univ

theorem Modality.Kratzer.propIntersection_cons {W : Type u_1} (p : W → Prop) (A : List (W → Prop)) : propIntersection (p :: A) = {i : W | p i} ∩ propIntersection A

theorem Modality.Kratzer.propIntersection_singleton {W : Type u_1} (p : W → Prop) : propIntersection [p] = {i : W | p i}

theorem Modality.Kratzer.isCompatibleWith_iff_exists {W : Type u_1} {p : W → Prop} {A : List (W → Prop)} : isCompatibleWith p A ↔ ∃ i ∈ propIntersection A, p i

theorem Modality.Kratzer.isCompatibleWith_iff_not_followsFrom_not {W : Type u_1} {p : W → Prop} {A : List (W → Prop)} : isCompatibleWith p A ↔ ¬followsFrom (fun (i : W) => ¬p i) A

Duality: p is compatible with A iff ¬p does not follow from A.

Definitions 5 and 6: must and can in view of

def Modality.Kratzer.mustInView {W : Type u_1} (f : W → List (W → Prop)) (p : W → Prop) (i : W) : Prop

Def 5 ([kratzer-1977]): must p in view of f at index i iff p follows from the premise set f i.

ν(p, f) = {i : ⋂(f i) ⊆ p}

Equations

• Modality.Kratzer.mustInView f p i = Modality.Kratzer.followsFrom p (f i)

def Modality.Kratzer.canInView {W : Type u_1} (f : W → List (W → Prop)) (p : W → Prop) (i : W) : Prop

Def 6 ([kratzer-1977]): can p in view of f at index i iff p is compatible with the premise set f i.

μ(p, f) = {i : ⋂((f i) ∪ {p}) ≠ ∅}

Equations

• Modality.Kratzer.canInView f p i = Modality.Kratzer.isCompatibleWith p (f i)

Definitions 7 and 8: must and can over consistent sublists

def Modality.Kratzer.consistentSublists {W : Type u_1} (A : List (W → Prop)) : Set (List (W → Prop))

The set of consistent sublists of a premise set: X_A = {B ⊆ A : consistent B}. Kratzer's revised definitions quantify over these to handle inconsistent A.

Concretely: a sublist B of A such that B is consistent.

Equations

• Modality.Kratzer.consistentSublists A = {B : List (W → Prop) | B ∈ A.sublists ∧ Modality.Kratzer.isConsistent B}

def Modality.Kratzer.mustInView' {W : Type u_1} (f : W → List (W → Prop)) (p : W → Prop) (i : W) : Prop

Def 7 ([kratzer-1977]): the revised necessity operator that handles possibly inconsistent premise sets.

must p in view of f at i iff for every consistent subset B of f i, there exists a consistent subset C ⊇ B such that p follows from C.

Original notation: ν(p, f) = {i : ∀B[B ∈ X_{f(i)} → ∃C[C ∈ X_{f(i)} ∧ B ⊆ C ∧ ⋂C ⊆ p]]}

Equations

• Modality.Kratzer.mustInView' f p i = ∀ B ∈ Modality.Kratzer.consistentSublists (f i), ∃ C ∈ Modality.Kratzer.consistentSublists (f i), B ⊆ C ∧ Modality.Kratzer.followsFrom p C

def Modality.Kratzer.canInView' {W : Type u_1} (f : W → List (W → Prop)) (p : W → Prop) (i : W) : Prop

Def 8 ([kratzer-1977]): the revised possibility operator that handles possibly inconsistent premise sets.

can p in view of f at i iff there exists a consistent subset B of f i such that for every consistent subset C ⊇ B, the set C ∪ {p} is consistent.

Original notation: μ(p, f) = {i : ∃B[B ∈ X_{f(i)} ∧ ∀C[(C ∈ X_{f(i)} ∧ B ⊆ C) → consistent(C ∪ {p})]]}

Equations

• Modality.Kratzer.canInView' f p i = ∃ B ∈ Modality.Kratzer.consistentSublists (f i), ∀ C ∈ Modality.Kratzer.consistentSublists (f i), B ⊆ C → Modality.Kratzer.isCompatibleWith p C

Monotonicity

The reduction theorems below need three monotonicity facts about the premise algebra. They are proved here once and reused.

theorem Modality.Kratzer.propIntersection_anti_of_subset {W : Type u_1} {A B : List (W → Prop)} (h : A ⊆ B) : propIntersection B ⊆ propIntersection A

propIntersection is anti-monotone in the premise list: more premises can only shrink the set of indices satisfying all of them.

theorem Modality.Kratzer.followsFrom_mono_of_subset {W : Type u_1} {p : W → Prop} {A B : List (W → Prop)} (h : A ⊆ B) (hp : followsFrom p A) : followsFrom p B

followsFrom is monotone in the premise list: more premises only add consequences.

theorem Modality.Kratzer.isCompatibleWith_anti_of_subset {W : Type u_1} {p : W → Prop} {A B : List (W → Prop)} (h : B ⊆ A) (hp : isCompatibleWith p A) : isCompatibleWith p B

isCompatibleWith is anti-monotone in the premise list: removing premises can only make a proposition easier to be compatible with.

theorem Modality.Kratzer.self_mem_consistentSublists {W : Type u_1} {A : List (W → Prop)} (h : isConsistent A) : A ∈ consistentSublists A

A consistent premise list is itself a member of its own consistent sublist powerset.

theorem Modality.Kratzer.subset_of_mem_consistentSublists {W : Type u_1} {A B : List (W → Prop)} (h : B ∈ consistentSublists A) : B ⊆ A

Every element of consistentSublists A is a ⊆-subset of A.

Reduction to Definitions 5 and 6

When the premise set f i is itself consistent, Kratzer's revised definitions collapse to the original Defs 5–6: there is no "inconsistency to repair." The witness for both directions is f i itself — it is a sublist of itself, it is consistent by hypothesis, and B ⊆ f i for every B ∈ consistentSublists (f i).

theorem Modality.Kratzer.mustInView_iff_mustInView'_of_consistent {W : Type u_1} (f : W → List (W → Prop)) (p : W → Prop) (i : W) (h : isConsistent (f i)) : mustInView' f p i ↔ mustInView f p i

When f i is consistent, the revised necessity operator coincides with the original.

theorem Modality.Kratzer.canInView_iff_canInView'_of_consistent {W : Type u_1} (f : W → List (W → Prop)) (p : W → Prop) (i : W) (h : isConsistent (f i)) : canInView' f p i ↔ canInView f p i

When f i is consistent, the revised possibility operator coincides with the original.

Duality

Can is the negation of must not under both pairs of definitions, since compatibility with a premise set is the failure of the negation to follow from it.

theorem Modality.Kratzer.canInView_iff_not_mustInView_not {W : Type u_1} (f : W → List (W → Prop)) (p : W → Prop) (i : W) : canInView f p i ↔ ¬mustInView f (fun (j : W) => ¬p j) i

theorem Modality.Kratzer.canInView'_iff_not_mustInView'_not {W : Type u_1} (f : W → List (W → Prop)) (p : W → Prop) (i : W) : canInView' f p i ↔ ¬mustInView' f (fun (j : W) => ¬p j) i

theorem Modality.Kratzer.mustInView'_iff_not_canInView'_not {W : Type u_1} (f : W → List (W → Prop)) (p : W → Prop) (i : W) : mustInView' f p i ↔ ¬canInView' f (fun (j : W) => ¬p j) i

Sufficient conditions for Definitions 7 and 8

theorem Modality.Kratzer.canInView'_of_mem {W : Type u_1} {f : W → List (W → Prop)} {p : W → Prop} {i : W} {B : List (W → Prop)} (hB : B ∈ consistentSublists (f i)) (hp : p ∈ B) : canInView' f p i

A premise in a consistent sublist is possible under Definition 8: every consistent extension still contains it.

theorem Modality.Kratzer.mustInView'_of_forall_isCompatibleWith {W : Type u_1} {f : W → List (W → Prop)} {p : W → Prop} {A : List (W → Prop)} {i : W} (hf : f i = p :: A) (h : ∀ B ∈ consistentSublists (f i), isCompatibleWith p B) : mustInView' f p i

The head of the premise set is necessary under Definition 7 when it is compatible with every consistent sublist: a sublist without it extends by it, one with it entails it.