def Semantics.Conditionals.materialImp {W : Type u_1} (p q : Prop' W) : Prop' W

Material conditional: p → q ≡ ¬p ∨ q

This is the classical truth-functional conditional. True whenever the antecedent is false or the consequent is true.

Note: The material conditional is already defined in Core.Proposition as pimp. We re-export it here for convenience.

Equations

• Semantics.Conditionals.materialImp p q = Core.Proposition.Classical.pimp W p q

def Semantics.Conditionals.materialImpB {W : Type u_1} (p q : BProp W) : BProp W

Decidable version of material implication

Equations

• Semantics.Conditionals.materialImpB p q w = (!p w || q w)

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

Strict conditional: true at w iff the material conditional holds at all accessible worlds.

□(p → q) ≡ ∀w' ∈ R(w). p(w') → q(w')

This is the modal "necessitation" of the material conditional. Used in deontic and epistemic conditionals.

Parameters:

• access: The accessibility relation R : W → Set W
• p: The antecedent proposition
• q: The consequent proposition

Equations

• Semantics.Conditionals.strictImp access p q w = ∀ w' ∈ access w, p w' → q w'

def Semantics.Conditionals.strictImpFinite {W : Type u_1} (access : W → List W) (p q : BProp W) : BProp W

Strict implication with finite accessibility (for computation)

Equations

• Semantics.Conditionals.strictImpFinite access p q w = (access w).all fun (w' : W) => !p w' || q w'

structure Semantics.Conditionals.SimilarityOrdering (W : Type u_1) : Type u_1

A similarity ordering on worlds.

For variably strict conditionals, we need a notion of "closest" p-worlds. This is typically modeled as a preorder on worlds centered at each world.

closer w w₁ w₂ means w₁ is at least as similar to w as w₂ is.

• closer : W → W → W → Prop

  w₁ is at least as close to w as w₂

• refl (w₀ w : W) : self.closer w₀ w w

  Reflexivity: at each center, every world is at least as close as itself. This makes closer w₀ a preorder at every center w₀.

• trans (w w₁ w₂ w₃ : W) : self.closer w w₁ w₂ → self.closer w w₂ w₃ → self.closer w w₁ w₃

  Transitivity

def Semantics.Conditionals.SimilarityOrdering.atCenter {W : Type u_1} (sim : SimilarityOrdering W) (w₀ : W) : Core.Order.NormalityOrder W

The NormalityOrder centered at world w₀: le w₁ w₂ iff w₁ is at least as close to w₀ as w₂ is. Connects Lewis/Stalnaker conditionals to the default reasoning infrastructure (optimal, refine, respects, CR1–CR4).

Equations

• sim.atCenter w₀ = { le := sim.closer w₀, le_refl := ⋯, le_trans := ⋯ }

def Semantics.Conditionals.variablyStrictImp {W : Type u_1} (sim : SimilarityOrdering W) (allWorlds : Set W) (p q : Prop' W) : Prop' W

Variably strict conditional (@cite{stalnaker-1968}/@cite{lewis-1973}):

"If p, then q" is true at w iff:

• Either there are no p-worlds (vacuous truth), or
• Some p-world is such that q holds at all p-worlds at least as close

This captures the intuition that conditionals quantify over "nearby" worlds where the antecedent holds.

Equations

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

def Semantics.Conditionals.conditionalPerfection {W : Type u_1} (p q : Prop' W) : Prop' W

Conditional perfection: the inference from "if A then C" to "if not A then not C".

This is NOT valid for material conditionals but IS observed pragmatically. The RSA model in GrusdtLassiterFranke2022 derives this as an implicature.

Equations

• Semantics.Conditionals.conditionalPerfection p q = Semantics.Conditionals.materialImp (Core.Proposition.Classical.pnot W p) (Core.Proposition.Classical.pnot W q)

theorem Semantics.Conditionals.modus_ponens {W : Type u_1} (p q : Prop' W) (w : W) (h_imp : materialImp p q w) (h_p : p w) : q w

Modus ponens: from (p → q) and p, derive q.

theorem Semantics.Conditionals.contraposition {W : Type u_1} (p q : Prop' W) : Core.Proposition.Classical.entails W (materialImp p q) (materialImp (Core.Proposition.Classical.pnot W q) (Core.Proposition.Classical.pnot W p))

Contraposition: (p → q) entails (¬q → ¬p).

theorem Semantics.Conditionals.perfection_not_entailed : ∃ (W : Type) (p : Prop' W) (q : Prop' W) (w : W), materialImp p q w ∧ ¬conditionalPerfection p q w

Conditional perfection is NOT semantically entailed.

There exists a world where (p → q) is true but (¬p → ¬q) is false. This shows that "perfection" (the biconditional reading) is a pragmatic inference, not a semantic entailment.

Counterexample: World where p is false, q is true. Then (p → q) is vacuously true, but (¬p → ¬q) = (true → false) = false.

theorem Semantics.Conditionals.perfection_not_entailed_variablyStrict : ∃ (W : Type) (sim : SimilarityOrdering W) (domain : Set W) (p : Prop' W) (q : Prop' W) (w : W), variablyStrictImp sim domain p q w ∧ ¬conditionalPerfection p q w

Conditional perfection is NOT semantically entailed (variably strict).

Even under @cite{stalnaker-1968}/@cite{lewis-1973} variably strict semantics (stronger than material implication), the conditional does not entail its converse. There exist a similarity ordering, propositions p and q, and a world w such that "if p then q" holds but "if ¬p then ¬q" does not.

Counterexample: W = Bool, p = (· = true), q = (fun _ => True), w = false. The conditional holds (the only p-world is true, where q holds trivially), but perfection fails (¬p(false) is true but ¬q(false) is false).

theorem Semantics.Conditionals.strict_implies_material {W : Type u_1} (R : W → Set W) (p q : Prop' W) (w : W) : w ∈ R w → strictImp R p q w → materialImp p q w

Strict conditional implies material conditional.

If w is accessible from itself (reflexive accessibility), then □(p → q) at w implies (p → q) at w.

def Semantics.Conditionals.SimilarityOrdering.isCentered {W : Type u_1} (sim : SimilarityOrdering W) : Prop

A centered similarity ordering: the actual world is always strictly closest to itself.

This is the "strong centering" axiom: w is strictly closer to itself than any other world.

Equations

• sim.isCentered = ∀ (w w' : W), w ≠ w' → sim.closer w w w' ∧ ¬sim.closer w w' w

theorem Semantics.Conditionals.variably_strict_implies_material {W : Type u_1} (sim : SimilarityOrdering W) (domain : Set W) (p q : Prop' W) (w : W) (hw : w ∈ domain) (hp : p w) (h_centered : sim.isCentered) : variablyStrictImp sim domain p q w → materialImp p q w

Variably strict conditional implies material conditional (with centered similarity).

If there is a p-world, the similarity ordering is centered, and the variably strict conditional holds, then the material conditional holds at the actual world.

The centering axiom ensures that if p holds at w, then w is the unique closest p-world to itself, so q must hold at w.

Kratzer Conditionals

@cite{nadathur-lauer-2020} @cite{stalnaker-1968}

This section provides a polymorphic, Set-based version of Kratzer's conditional semantics for use in mathematical proofs.

For the computable, List-based version with concrete examples and proven properties (preorder, duality, K axiom, etc.), see: Linglib.Theories.Semantics.Modality.Kratzer

Both use the same CORRECT subset-based ordering from @cite{kratzer-1981}: w₁ ≤_A w₂ iff {p ∈ A : w₂ ∈ p} ⊆ {p ∈ A : w₁ ∈ p}

structure Semantics.Conditionals.KratzerContext (W : Type u_1) : Type u_1

Kratzer's semantics for conditionals uses:

1. A modal base f : W → Set W (epistemic, circumstantial, etc.)
2. An ordering source g : W → Set (Prop' W) (stereotypical, deontic, etc.)

The conditional "if p, then q" is true at w iff q holds at the "best" p-worlds according to the ordering.

• modalBase : W → Set W

  Modal base: accessible worlds from w

• orderingSource : W → Set (Prop' W)

  Ordering source: propositions that induce a preference

def Semantics.Conditionals.kratzerBetter {W : Type u_1} (os : Set (Prop' W)) (w₁ w₂ : W) : Prop

Kratzer's ordering relation (Set-based version for proofs).

w₁ is at least as good as w₂ according to ordering source os iff every proposition in os satisfied by w₂ is also satisfied by w₁.

This is the correct subset-based ordering from @cite{kratzer-1981}. Equivalent to atLeastAsGoodAs in Kratzer.lean (which uses Lists for computation).

NOT a counting-based ordering (which would be incorrect).

Equations

• Semantics.Conditionals.kratzerBetter os w₁ w₂ = ({p : Prop' W | p ∈ os ∧ p w₂} ⊆ {p : Prop' W | p ∈ os ∧ p w₁})

def Semantics.Conditionals.kratzerConditional {W : Type u_1} (ctx : KratzerContext W) (p q : Prop' W) : Prop' W

Kratzer-style conditional semantics.

"If p, then q" is true at w iff at the best p-worlds (in the modal base, according to the ordering source), q holds.

Best worlds are those maximal under kratzerBetter: w' is best if for all w'' in pWorlds, if w' ≤ w'' then w'' ≤ w' (i.e., they're equivalent).

Equations

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

def Semantics.Conditionals.indicativeConditional {W : Type u_1} (p q : Prop' W) : Prop' W

Indicative conditional (epistemic, open).

"If A, then C" in the indicative mood - the standard conditional for reasoning about what we expect to be true if A turns out to be true.

This is just the material conditional: ¬A ∨ C.

Equations

• Semantics.Conditionals.indicativeConditional p q = Semantics.Conditionals.materialImp p q

def Semantics.Conditionals.subjunctiveConditional {W : Type u_1} (sim : SimilarityOrdering W) (domain : Set W) (p q : Prop' W) : Prop' W

Subjunctive conditional (counterfactual).

"If A were the case, then C would be the case" - the conditional for reasoning about non-actual possibilities.

This uses the variably strict semantics: at the closest A-worlds, C holds.

Equations

• Semantics.Conditionals.subjunctiveConditional sim domain p q = Semantics.Conditionals.variablyStrictImp sim domain p q

theorem Semantics.Conditionals.subjunctive_implies_indicative {W : Type u_1} (sim : SimilarityOrdering W) (domain : Set W) (p q : Prop' W) (w : W) (hw : w ∈ domain) (hp : p w) (h_centered : sim.isCentered) : subjunctiveConditional sim domain p q w → indicativeConditional p q w

Subjunctive implies indicative (when the antecedent holds at the actual world).

If "if p were, then q would" is true at w, and p holds at w, then q holds at w. This shows that subjunctive conditionals are stronger than indicatives in this sense.

Requires a centered similarity ordering (the actual world is closest to itself).

Selection Functions

Stalnaker's selection function approach to counterfactuals:

• A selection function s : W × 𝒫(W) → W selects THE closest antecedent-world
• "If A were, C would be" is true iff C holds at s(w, ⦃A⦄)

Key distinction from @cite{lewis-1973}:

• @cite{lewis-1973}: Universal quantification over all closest A-worlds
• @cite{stalnaker-1968}: Selection of a single A-world (with supervaluation for ties)

This is formalized for use in @cite{ramotowska-santorio-2025} analysis of counterfactual force under quantifiers.

structure Semantics.Conditionals.SelectionFunction (W : Type u_1) : Type u_1

A selection function picks the unique closest antecedent-world.

s w A returns the closest A-world to w, or w itself if no A-worlds exist.

Constraints (from @cite{stalnaker-1968}):

1. Success: If A is non-empty, s(w, A) ∈ A
2. Strong Centering: If w ∈ A, then s(w, A) = w

• select : W → Set W → W

  The selection function

• success (w : W) (A : Set W) : A.Nonempty → self.select w A ∈ A

  Success: selected world is in the antecedent (if nonempty)

• centering (w : W) (A : Set W) : w ∈ A → self.select w A = w

  Strong centering: if actual world satisfies antecedent, select it

def Semantics.Conditionals.candidateSelections {W : Type u_1} (sim : SimilarityOrdering W) (domain : Set W) (w : W) (A : Set W) : Set W

Candidate selection functions induced by a comparative similarity ordering.

Given an ordering, a selection function is "legitimate" iff it always selects a world that is closest (minimal w.r.t. the ordering).

This is the connection between @cite{lewis-1973}/Kratzer orderings and @cite{stalnaker-1968} selection.

Equations

• Semantics.Conditionals.candidateSelections sim domain w A = {w' : W | w' ∈ A ∩ domain ∧ ∀ w'' ∈ A ∩ domain, sim.closer w w' w''}

def Semantics.Conditionals.selectionalCounterfactual {W : Type u_1} (s : SelectionFunction W) (allWorlds : Set W) (p q : Prop' W) : Prop' W

Counterfactual via selection function (Stalnaker semantics).

"If A were, C would be" is true at w iff C holds at the selected A-world.

Equations

• Semantics.Conditionals.selectionalCounterfactual s allWorlds p q w = ({w' : W | w' ∈ allWorlds ∧ p w'} = ∅ ∨ q (s.select w {w' : W | w' ∈ allWorlds ∧ p w'}))

def Semantics.Conditionals.comparativeCloseness {W : Type u_1} (sim : SimilarityOrdering W) (w₀ w₁ w₂ : W) : Prop

Comparative closeness relation derived from a similarity ordering.

w₁ ≤_w₀ w₂ means w₁ is at least as similar to w₀ as w₂ is. This is the @cite{lewis-1973} notation.

Equations

• (w₁ ≤[sim,w₀] w₂) = sim.closer w₀ w₁ w₂

def Semantics.Conditionals.«term_≤[_,_]_» : Lean.TrailingParserDescr

Equations

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

Selection via Intervention

A key insight: selection functions can be grounded in causal models.

Given a causal model, s(w, A) = the world resulting from intervening to make A true at w (Pearl's do(A)).

This connects:

• Stalnaker selection → Causal intervention
• "If A were" → do(A)
• Counterfactual dependence → Causal necessity

See Theories/NadathurLauer2020/ for the causal model infrastructure.

Assertability vs Truth

The key insight from @cite{grusdt-lassiter-franke-2022} is that the ASSERTABILITY of a conditional depends on P(C|A), not its truth conditions.

A conditional "if A then C" is assertable when P(C|A) is high (> θ).

This is formalized in Assertability.lean, where we define:

• conditionalProbability : WorldState → ℚ
• assertable : WorldState → ℚ → Bool

The RSA model then explains pragmatic phenomena (conditional perfection, missing-link infelicity) through reasoning about assertability.