The restrictor theory of conditionals

This file defines the restrictor conditional. On the restrictor analysis of Lewis and Kratzer an if-clause is not a connective but restricts the modal base of a possibly covert modal, so if α, must β is necessity over the modal base restricted by α and if α, might β possibility over it. The restrictor conditional is the conditional over the best accessible antecedent-worlds under the preorders the ordering source induces (orderingImp), its might is the might of that conditional, and with an empty ordering source it is the strict conditional.

Main definitions

• Restrictor.conditionalNecessity, Restrictor.conditionalPossibility: if α, must β and if α, might β.

Main results

• Restrictor.conditionalNecessity_iff_mem_orderingImp, Restrictor.conditionalPossibility_iff_mem_might: the restrictor conditionals are the conditional over the best accessible antecedent-worlds and its might.
• Restrictor.restrictor_eq_strict: with an empty ordering source it is the strict conditional.

References

• D. Lewis, Adverbs of Quantification (1975)
• A. Kratzer, Conditionals (1986)
• A. Kratzer, Modals and Conditionals (2012)

def Conditional.Restrictor.conditionalNecessity {W : Type u_1} (f g : Modality.Background W) (α β : W → Prop) (w : W) : Prop

If α, must β on the restrictor analysis is necessity over the modal base restricted by α.

Equations

• Conditional.Restrictor.conditionalNecessity f g α β w = Modality.necessity (f.restrict α) g β w

def Conditional.Restrictor.conditionalPossibility {W : Type u_1} (f g : Modality.Background W) (α β : W → Prop) (w : W) : Prop

If α, might β on the restrictor analysis is possibility over the modal base restricted by α.

Equations

• Conditional.Restrictor.conditionalPossibility f g α β w = Modality.possibility (f.restrict α) g β w

theorem Conditional.Restrictor.conditionalNecessity_iff_mem_orderingImp {W : Type u_1} (f g : Modality.Background W) (α β : W → Prop) (w : W) : conditionalNecessity f g α β w ↔ w ∈ orderingImp f.accessibleWorlds (fun (w : W) => Modality.premisePreorder (g w)) {v : W | α v} {v : W | β v}

If α, must β is the conditional over the best accessible α-worlds, under the preorders the ordering source induces.

theorem Conditional.Restrictor.conditionalPossibility_iff_mem_might {W : Type u_1} (f g : Modality.Background W) (α β : W → Prop) (w : W) : conditionalPossibility f g α β w ↔ w ∈ might (orderingImp f.accessibleWorlds fun (w : W) => Modality.premisePreorder (g w)) {v : W | α v} {v : W | β v}

If α, might β is the might of the conditional over the best accessible α-worlds.

theorem Conditional.Restrictor.restrictor_eq_strict {W : Type u_1} (f : Modality.Background W) (α β : W → Prop) (w : W) : conditionalNecessity f ⊥ α β w ↔ w ∈ strictImp f.accessibleWorlds {v : W | α v} {v : W | β v}

With an empty ordering source, if α, must β is the strict conditional over the accessible worlds.

theorem Conditional.Restrictor.vacuous_conditional {W : Type u_1} (f g : Modality.Background W) (α β : W → Prop) (w : W) (h : ∀ w' ∈ f.accessibleWorlds w, ¬α w') : conditionalNecessity f g α β w

If α, must β holds vacuously when no accessible world satisfies α.

theorem Conditional.Restrictor.material_from_restrictor {W : Type u_1} (f : Modality.Background W) (α β : W → Prop) (w : W) (hTotal : f.accessibleWorlds w = {w}) : conditionalNecessity f ⊥ α β w ↔ α w → β w

With the evaluation world as its only accessible world and an empty ordering source, if α, must β is the material conditional.