Premise Sets and Logical Relations

@cite{kratzer-1977} @cite{kratzer-1981} @cite{kratzer-2012}

Generic, modality-agnostic primitives over premise sets — finite collections of propositions over an arbitrary index type. These are the logical primitives on which Kratzer's modal semantics, ordering sources, conditional restriction, and lumping all rest, but they have no built-in commitment to "worlds" vs. "situations" vs. "times": they make sense for any Index : Type* of points at which propositions are evaluated.

Why this lives in Core/Logic/Intensional/

A premise set is a List (Index → Prop). The notions of consistency, following from, and compatibility are purely set-theoretic facts about extensions in Index — they are about logical relations on propositions, not about modality. Modal operators (necessity, possibility) are then defined in terms of these primitives, but the primitives themselves should be available to any module that wants to talk about premises (counterfactual analysis, discourse update, situation lumping, …).

Mathlib-style discipline

Propositions are Index → Prop (mathlib-native), extensions are Set Index (also mathlib-native). All predicates return Prop; we reason classically and do not register Decidable instances. Callers who need decidability can supply it locally via [DecidablePred p] in their own theorems; the core intensional algebra is purely classical.

Key definitions

• propExtension — extension of a proposition ({i | p i} as a Set Index)
• propIntersection — intersection of a list of propositions (Set Index)
• followsFrom — p follows from A iff ⋂ A ⊆ {i | p i} (Kratzer p. 31)
• isConsistent — A is consistent iff ⋂ A is non-empty
• isCompatibleWith — p is compatible with A iff A ∪ {p} is consistent

Kratzer 1977 Definitions 5–8

• mustInView (Def 5) — must p in view of f at i iff p follows from f i
• canInView (Def 6) — can p in view of f at i iff p is compatible with f i

When f i may be inconsistent, Kratzer revises these in terms of maximally consistent subsets:

• consistentSublists — X_{f(i)} in Kratzer's notation
• mustInView' (Def 7) — every consistent subset has a consistent extension from which p follows
• canInView' (Def 8) — some consistent subset has a consistent extension that remains consistent with p

The revised definitions reduce to the original ones when the premise set is itself consistent (mustInView_iff_mustInView'_of_consistent).

Primitives on premise sets

def Core.Logic.Intensional.Premise.propExtension {Index : Type u_1} (p : Index → Prop) : Set Index

The extension of a proposition: the set of indices at which it holds.

Equations

• Core.Logic.Intensional.Premise.propExtension p = {i : Index | p i}

def Core.Logic.Intensional.Premise.propIntersection {Index : Type u_1} (props : List (Index → Prop)) : Set Index

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

Equations

• Core.Logic.Intensional.Premise.propIntersection props = {i : Index | ∀ p ∈ props, p i}

def Core.Logic.Intensional.Premise.followsFrom {Index : Type u_1} (p : Index → Prop) (A : List (Index → Prop)) : Prop

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

Equations

• Core.Logic.Intensional.Premise.followsFrom p A = (Core.Logic.Intensional.Premise.propIntersection A ⊆ Core.Logic.Intensional.Premise.propExtension p)

def Core.Logic.Intensional.Premise.isConsistent {Index : Type u_1} (A : List (Index → Prop)) : Prop

A premise set is consistent iff ⋂ A is non-empty (@cite{kratzer-1977} p. 31).

Equations

• Core.Logic.Intensional.Premise.isConsistent A = (Core.Logic.Intensional.Premise.propIntersection A).Nonempty

def Core.Logic.Intensional.Premise.isCompatibleWith {Index : Type u_1} (p : Index → Prop) (A : List (Index → Prop)) : Prop

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

Equations

• Core.Logic.Intensional.Premise.isCompatibleWith p A = Core.Logic.Intensional.Premise.isConsistent (p :: A)

Kratzer 1977 Definitions 5–6: must/can in view of

def Core.Logic.Intensional.Premise.mustInView {Index : Type u_1} (f : Index → List (Index → Prop)) (p : Index → Prop) (i : Index) : Prop

Def 5 (@cite{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

• Core.Logic.Intensional.Premise.mustInView f p i = Core.Logic.Intensional.Premise.followsFrom p (f i)

def Core.Logic.Intensional.Premise.canInView {Index : Type u_1} (f : Index → List (Index → Prop)) (p : Index → Prop) (i : Index) : Prop

Def 6 (@cite{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

• Core.Logic.Intensional.Premise.canInView f p i = Core.Logic.Intensional.Premise.isCompatibleWith p (f i)

Kratzer 1977 Definitions 7–8: revised must/can for inconsistent premise sets

def Core.Logic.Intensional.Premise.consistentSublists {Index : Type u_1} (A : List (Index → Prop)) : Set (List (Index → 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

• Core.Logic.Intensional.Premise.consistentSublists A = {B : List (Index → Prop) | B ∈ A.sublists ∧ Core.Logic.Intensional.Premise.isConsistent B}

def Core.Logic.Intensional.Premise.mustInView' {Index : Type u_1} (f : Index → List (Index → Prop)) (p : Index → Prop) (i : Index) : Prop

Def 7 (@cite{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

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

def Core.Logic.Intensional.Premise.canInView' {Index : Type u_1} (f : Index → List (Index → Prop)) (p : Index → Prop) (i : Index) : Prop

Def 8 (@cite{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

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

Monotonicity helpers

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

theorem Core.Logic.Intensional.Premise.propIntersection_anti_of_subset {Index : Type u_1} {A B : List (Index → 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 Core.Logic.Intensional.Premise.followsFrom_mono_of_subset {Index : Type u_1} {p : Index → Prop} {A B : List (Index → Prop)} (h : A ⊆ B) (hp : followsFrom p A) : followsFrom p B

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

theorem Core.Logic.Intensional.Premise.isCompatibleWith_anti_of_subset {Index : Type u_1} {p : Index → Prop} {A B : List (Index → 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 Core.Logic.Intensional.Premise.self_mem_consistentSublists {Index : Type u_1} {A : List (Index → Prop)} (h : isConsistent A) : A ∈ consistentSublists A

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

theorem Core.Logic.Intensional.Premise.subset_of_mem_consistentSublists {Index : Type u_1} {A B : List (Index → Prop)} (h : B ∈ consistentSublists A) : B ⊆ A

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

Reduction to the unrevised definitions

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 Core.Logic.Intensional.Premise.mustInView_iff_mustInView'_of_consistent {Index : Type u_1} (f : Index → List (Index → Prop)) (p : Index → Prop) (i : Index) (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 Core.Logic.Intensional.Premise.canInView_iff_canInView'_of_consistent {Index : Type u_1} (f : Index → List (Index → Prop)) (p : Index → Prop) (i : Index) (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.