Conditional operators

[Lew73b] [Sta68]

The basic conditional operators. A conditional operator sends an antecedent and a consequent (propositions qua Set W) to the proposition expressed by the conditional; rival theories differ in the carrier the operator is derived from. Comparisons and non-entailments between operators are stated over this shared signature.

Main definitions

• materialImp p q: the truth-functional conditional; w ∈ materialImp p q iff w ∈ p → w ∈ q.
• strictImp access p q: the strict conditional over an accessibility map access : I → Set W (a modal base); i ∈ strictImp access p q iff access i ∩ p ⊆ q.
• variablyStrictImp sim allWorlds p q: the [Sta68] / [Lew73b] variably strict conditional — vacuously true without antecedent worlds, otherwise some closest antecedent world settles the consequent.
• conditionalPerfection p q: the perfected ("only if") reading, materialImp pᶜ qᶜ.

Main results

• strictImp_anti_left: antecedent strengthening — valid for the strict conditional, the signature property variably strict semantics rejects.
• mem_strictImp_of_subset / not_subset_of_mem_strictImp: a strict conditional whose consequent exhausts the domain is trivially true; a true non-trivial one has an antecedent that excludes a live world ([Sta75], [vF99a], [Miz24]).
• strict_implies_material / variably_strict_implies_material: both modal operators refine the material conditional (under reflexivity / centering).
• perfection_not_entailed / perfection_not_entailed_variablyStrict: conditional perfection is not entailed, even variably strictly — it is a pragmatic inference ([GLF22]).

The Kratzer restrictor conditional (necessity over a restricted conversational background) lives in Conditionals/Restrictor.lean, which bridges to strictImp via conditionalNecessity_iff_mem_strictImp.

Material conditional

def Semantics.Conditionals.materialImp {W : Type u_2} (p q : Set W) : Set W

The material conditional: true wherever the antecedent fails or the consequent holds (pᶜ ∪ q). Classical semantics keeps this literal meaning and derives its apparent exceptions pragmatically ([GLF22]).

Equations

• Semantics.Conditionals.materialImp p q = {w : W | w ∈ p → w ∈ q}

@[simp]

theorem Semantics.Conditionals.mem_materialImp {W : Type u_2} {p q : Set W} {w : W} : w ∈ materialImp p q ↔ w ∈ p → w ∈ q

theorem Semantics.Conditionals.contraposition {W : Type u_2} {p q : Set W} : materialImp p q ⊆ materialImp qᶜ pᶜ

Contraposition, valid for the material conditional. [Sta75] (§4) observes that it fails for indicative conditionals under his semantics — see Studies/Stalnaker1975.

Strict conditional

def Semantics.Conditionals.strictImp {I : Type u_1} {W : Type u_2} (access : I → Set W) (p q : Set W) : Set I

The strict conditional over an accessibility map: the consequent holds throughout the accessible antecedent worlds, access i ∩ p ⊆ q. The evaluation points I may differ from the worlds W quantified over — e.g. a historical modal base WorldTimeIndex W T → Set W evaluates at world-time indices ([Con02]); the classical case is I = W.

Equations

• Semantics.Conditionals.strictImp access p q = {i : I | access i ∩ p ⊆ q}

@[simp]

theorem Semantics.Conditionals.mem_strictImp {I : Type u_1} {W : Type u_2} {access : I → Set W} {p q : Set W} {i : I} : i ∈ strictImp access p q ↔ access i ∩ p ⊆ q

theorem Semantics.Conditionals.mem_strictImp_forall {I : Type u_1} {W : Type u_2} {access : I → Set W} {p q : Set W} {i : I} : i ∈ strictImp access p q ↔ ∀ w ∈ access i, w ∈ p → w ∈ q

The quantifier reading of the strict conditional.

theorem Semantics.Conditionals.strictImp_mono_right {I : Type u_1} {W : Type u_2} {access : I → Set W} {p q q' : Set W} (hq : q ⊆ q') : strictImp access p q ⊆ strictImp access p q'

The strict conditional is monotone in its consequent.

theorem Semantics.Conditionals.strictImp_anti_left {I : Type u_1} {W : Type u_2} {access : I → Set W} {p p' q : Set W} (hp : p' ⊆ p) : strictImp access p q ⊆ strictImp access p' q

Antecedent strengthening: the strict conditional is antitone in its antecedent — the signature property of strict (and material) conditionals that variably strict semantics rejects ([Lew73b] Sobel sequences).

theorem Semantics.Conditionals.mem_strictImp_of_subset {I : Type u_1} {W : Type u_2} {access : I → Set W} {p q : Set W} {i : I} (h : access i ⊆ q) : i ∈ strictImp access p q

Triviality: when the consequent already holds throughout the accessible worlds, the strict conditional holds for any antecedent — the if-clause does no work ([Sta75], [vF99a]; the Anderson-conditional application is [Miz24] §2).

theorem Semantics.Conditionals.not_subset_of_mem_strictImp {I : Type u_1} {W : Type u_2} {access : I → Set W} {p q : Set W} {i : I} (hm : i ∈ strictImp access p q) (hq : ¬access i ⊆ q) : ¬access i ⊆ p

Informativity: a true strict conditional whose consequent is not trivial over the accessible worlds has an antecedent that excludes at least one accessible world (Set.not_subset gives the witness form) ([Miz24] §2).

theorem Semantics.Conditionals.strict_implies_material {W : Type u_2} {p q : Set W} {w : W} {R : W → Set W} (h_refl : w ∈ R w) (h : w ∈ strictImp R p q) : w ∈ materialImp p q

With reflexive access, the strict conditional refines the material one.

Variably strict conditional

def Semantics.Conditionals.variablyStrictImp {W : Type u_2} (sim : Core.Order.SimilarityOrdering W) (allWorlds p q : Set W) : Set W

The variably strict conditional ([Sta68] / [Lew73b]): vacuously true if the domain has no antecedent worlds; otherwise true iff some antecedent world settles the consequent throughout all antecedent worlds at least as close. (SimilarityOrdering and its constructors live in Core.Order.SimilarityOrdering.)

Equations

• Semantics.Conditionals.variablyStrictImp sim allWorlds p q = {w : W | allWorlds ∩ p = ∅ ∨ ∃ w' ∈ allWorlds ∩ p, ∀ w'' ∈ allWorlds ∩ p, (w'' ≤[sim,w] w') → w'' ∈ q}

@[simp]

theorem Semantics.Conditionals.mem_variablyStrictImp {W : Type u_2} {p q : Set W} {w : W} {sim : Core.Order.SimilarityOrdering W} {allWorlds : Set W} : w ∈ variablyStrictImp sim allWorlds p q ↔ allWorlds ∩ p = ∅ ∨ ∃ w' ∈ allWorlds ∩ p, ∀ w'' ∈ allWorlds ∩ p, (w'' ≤[sim,w] w') → w'' ∈ q

theorem Semantics.Conditionals.variably_strict_implies_material {W : Type u_2} {p q : Set W} {w : W} {sim : Core.Order.SimilarityOrdering W} {allWorlds : Set W} (hw : w ∈ allWorlds) (hp : w ∈ p) (h_centered : sim.isCentered) (h : w ∈ variablyStrictImp sim allWorlds p q) : w ∈ materialImp p q

With centered similarity, the variably strict conditional refines the material one at antecedent worlds: w is its own unique closest antecedent world, so the consequent must hold there.

Conditional perfection

def Semantics.Conditionals.conditionalPerfection {W : Type u_2} (p q : Set W) : Set W

Conditional perfection: the strengthened converse reading of a conditional ("if not A, not C"), as materialImp pᶜ qᶜ. Observed pragmatically but not entailed (perfection_not_entailed); [GLF22] derive it as an RSA implicature.

Equations

• Semantics.Conditionals.conditionalPerfection p q = Semantics.Conditionals.materialImp pᶜ qᶜ

theorem Semantics.Conditionals.perfection_not_entailed : ∃ (W : Type) (p : Set W) (q : Set W), ∃ w ∈ materialImp p q, w ∉ conditionalPerfection p q

Conditional perfection is not entailed: the material conditional can hold (vacuously, at an antecedent-false world) where its perfection fails.

theorem Semantics.Conditionals.perfection_not_entailed_variablyStrict : ∃ (W : Type) (sim : Core.Order.SimilarityOrdering W) (domain : Set W) (p : Set W) (q : Set W), ∃ w ∈ variablyStrictImp sim domain p q, w ∉ conditionalPerfection p q

Perfection is not entailed even variably strictly: the [Sta68] / [Lew73b] semantics is stronger than material implication, yet still does not entail the converse.