Conditional Semantics

@cite{lewis-1973} @cite{stalnaker-1968}

Compositional semantics for conditional sentences.

Overview

This module provides the semantic building blocks for conditionals:

1. Material conditional: p → q = ¬p ∨ q (classical logic)
2. Strict conditional: □(p → q) - necessity of material conditional
3. Variably strict conditional: @cite{stalnaker-1968}/@cite{lewis-1973}-style conditionals

The Material Conditional Problem

The material conditional (p → q ≡ ¬p ∨ q) has well-known problems:

• "If pigs fly, then the moon is cheese" comes out true
• It doesn't capture "If A, then C" as speakers use it

However, following @cite{grusdt-lassiter-franke-2022}, we can maintain classical semantics while deriving apparent exceptions through RSA pragmatics. The key is that conditionals assert high conditional probability, not material implication.

def Semantics.Conditionals.materialImp {W : Type u_1} (p q : Set W) : Set 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.

Equivalent to pᶜ ∪ q in mathlib's Set algebra; written here in set-builder form to keep the conditional name discourse-meaningful.

Equations

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

def Semantics.Conditionals.strictImp {W : Type u_1} (access : W → Set W) (p q : Set W) : Set 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'

SimilarityOrdering and its constructors (ofBool, atCenter) live in Core.Order.SimilarityOrdering since they are general-purpose primitives used by counterfactuals, alternative-sensitive operators, and causal psycholinguistic models. They are re-exported above via open Core.Order.

def Semantics.Conditionals.variablyStrictImp {W : Type u_1} (sim : Core.Order.SimilarityOrdering W) (allWorlds p q : Set W) : Set 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 : Set W) : Set 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 pᶜ qᶜ

theorem Semantics.Conditionals.modus_ponens {W : Type u_1} (p q : Set 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 : Set W) : materialImp p q ⊆ materialImp qᶜ pᶜ

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

theorem Semantics.Conditionals.perfection_not_entailed : ∃ (W : Type) (p : Set W) (q : Set 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 : Core.Order.SimilarityOrdering W) (domain : Set W) (p : Set W) (q : Set 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 : Set 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.

SimilarityOrdering.isCentered lives in Core.Order.SimilarityOrdering (re-exported above).

theorem Semantics.Conditionals.variably_strict_implies_material {W : Type u_1} (sim : Core.Order.SimilarityOrdering W) (domain p q : Set 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.

KratzerContext/kratzerBetter/kratzerConditional previously lived here as a Set-based parallel to the canonical List-based Kratzer machinery in Theories/Semantics/Modality/Kratzer/. They were a third parallel formalization (alongside Kratzer/Operators and the late lumping CF in Conditionals/PremiseSemantic.lean) and have been deleted in favour of Restrictor.conditionalNecessity (which calls the canonical Kratzer.necessity directly). The sole consumer (LeftNested.lean) now uses conditionalNecessity.