Restrictor Theory of Conditionals

@cite{kratzer-1986} @cite{kratzer-2012}

Kratzer's restrictor analysis: if-clauses restrict the modal domain rather than functioning as binary connectives. "If α, (must) β" is analyzed as modal necessity/possibility over the modal base restricted by α.

This module bridges Conditionals/Basic.lean and Modality/Kratzer.lean, deriving conditional truth conditions from modal restriction.

Core Thesis

If-clauses are not propositional connectives. They are restrictors of the modal base. "If it rains, the streets are wet" does not express a binary relation between two propositions. Instead, "if it rains" restricts the modal base to rain-worlds, and the (possibly covert) necessity operator quantifies over the best of those worlds.

Key Result

restrictor_eq_strict: with empty ordering source, Kratzer's conditional necessity (∀w' ∈ Best(f+α, ∅, w). β(w')) equals the strict conditional (∀w' ∈ ∩f(w). α(w') → β(w')) from Conditionals/Basic.lean.

Core definitions

def Semantics.Conditionals.Restrictor.conditionalNecessity {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (g : Core.Logic.Intensional.OrderingSource W) (α β : W → Prop) (w : W) : Prop

If α, must β under the restrictor analysis: necessity over the α-restricted modal base.

Equations

• Semantics.Conditionals.Restrictor.conditionalNecessity f g α β w = Semantics.Modality.Kratzer.necessity (Semantics.Modality.Kratzer.restrictedBase f α) g β w

def Semantics.Conditionals.Restrictor.conditionalPossibility {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (g : Core.Logic.Intensional.OrderingSource W) (α β : W → Prop) (w : W) : Prop

If α, might β under the restrictor analysis: possibility over the α-restricted modal base.

Equations

• Semantics.Conditionals.Restrictor.conditionalPossibility f g α β w = Semantics.Modality.Kratzer.possibility (Semantics.Modality.Kratzer.restrictedBase f α) g β w

Structural lemma

theorem Semantics.Conditionals.Restrictor.restricted_accessible_eq {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (α : W → Prop) (w : W) : Modality.Kratzer.accessibleWorlds (Modality.Kratzer.restrictedBase f α) w = {w' : W | w' ∈ Modality.Kratzer.accessibleWorlds f w ∧ α w'}

Restricted accessible worlds = α-worlds within the original accessible worlds.

Main bridge theorems

theorem Semantics.Conditionals.Restrictor.restrictor_eq_strict {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (α β : W → Prop) (w : W) : conditionalNecessity f Core.Logic.Intensional.emptyBackground α β w ↔ ∀ w' ∈ Modality.Kratzer.accessibleWorlds f w, α w' → β w'

Restrictor = Strict conditional.

With empty ordering source, "if α, must β" equals "□_f(α → β)".

Properties

theorem Semantics.Conditionals.Restrictor.conditional_duality {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (g : Core.Logic.Intensional.OrderingSource W) (α β : W → Prop) (w : W) : conditionalNecessity f g α β w ↔ ¬conditionalPossibility f g α (fun (w' : W) => ¬β w') w

Conditional duality: "if α, must β" ↔ ¬"if α, might ¬β".

theorem Semantics.Conditionals.Restrictor.vacuous_conditional {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (g : Core.Logic.Intensional.OrderingSource W) (α β : W → Prop) (w : W) (h : ∀ w' ∈ Modality.Kratzer.accessibleWorlds f w, ¬α w') : conditionalNecessity f g α β w

Vacuous conditional: if no accessible worlds satisfy α, conditional necessity holds vacuously.

theorem Semantics.Conditionals.Restrictor.material_from_restrictor {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (α β : W → Prop) (w : W) (hTotal : Modality.Kratzer.accessibleWorlds f w = {w}) : conditionalNecessity f Core.Logic.Intensional.emptyBackground α β w ↔ α w → β w

Material conditional as degenerate case: with totally realistic base and empty ordering, "if α, must β" reduces to material implication.

theorem Semantics.Conditionals.Restrictor.restrictor_monotone {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (α₁ α₂ : W → Prop) (w : W) (h : ∀ (w' : W), α₂ w' → α₁ w') (w' : W) : w' ∈ Modality.Kratzer.accessibleWorlds (Modality.Kratzer.restrictedBase f α₂) w → w' ∈ Modality.Kratzer.accessibleWorlds (Modality.Kratzer.restrictedBase f α₁) w

Restrictor monotonicity: if α₂ entails α₁, then the α₂-restricted base is contained in the α₁-restricted base.

theorem Semantics.Conditionals.Restrictor.double_restriction {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (α₁ α₂ : W → Prop) (w : W) : Modality.Kratzer.accessibleWorlds (Modality.Kratzer.restrictedBase (Modality.Kratzer.restrictedBase f α₁) α₂) w = Modality.Kratzer.accessibleWorlds (Modality.Kratzer.restrictedBase f fun (w' : W) => α₁ w' ∧ α₂ w') w

Double restriction: restricting by α₁ then α₂ equals restricting by (α₁ ∧ α₂).

theorem Semantics.Conditionals.Restrictor.restrictor_strengthens {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (α : W → Prop) (w w' : W) : w' ∈ Modality.Kratzer.accessibleWorlds (Modality.Kratzer.restrictedBase f α) w → w' ∈ Modality.Kratzer.accessibleWorlds f w

Restrictor strengthening: adding a restrictor α to a modal base can only shrink (or preserve) the set of accessible worlds.

theorem Semantics.Conditionals.Restrictor.conditional_K {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (g : Core.Logic.Intensional.OrderingSource W) (α β γ : W → Prop) (w : W) (hImpl : conditionalNecessity f g α (fun (w' : W) => β w' → γ w') w) (hBeta : conditionalNecessity f g α β w) : conditionalNecessity f g α γ w

Conditional K axiom: conditional necessity distributes over implication.

Prop-level bridge

theorem Semantics.Conditionals.Restrictor.conditionalNecessity_iff_domainRestricted {W : Type u_1} (f : Core.Logic.Intensional.ModalBase W) (α β : W → Prop) (w : W) : conditionalNecessity f Core.Logic.Intensional.emptyBackground α β w ↔ ∀ w' ∈ Modality.Kratzer.accessibleWorlds f w, α w' → β w'

conditionalNecessity (with empty ordering source) corresponds to domainRestrictedConditional at the Prop level.