inductive Semantics.Conditionals.ConditionalType : Type

The two fundamental conditional interpretation types.

Following @cite{cao-white-lassiter-2025} and building on @cite{iatridou-1991}, @cite{haegeman-2003}:

• Hypothetical (HC): Antecedent is supposed; speaker uncertain about its truth
• Premise (PC): Antecedent echoes prior discourse; no uncertainty implication

Key diagnostics:

• HC can't be paraphrased with "given that/since"
• PC can be paraphrased with "given that/since"
• HC licenses NPIs in antecedent
• PC licenses PPIs in antecedent

• hypothetical : ConditionalType
• premise : ConditionalType

instance Semantics.Conditionals.instDecidableEqConditionalType : DecidableEq ConditionalType

Equations

• Semantics.Conditionals.instDecidableEqConditionalType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Conditionals.instReprConditionalType.repr : ConditionalType → ℕ → Std.Format

Equations

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

instance Semantics.Conditionals.instReprConditionalType : Repr ConditionalType

Equations

• Semantics.Conditionals.instReprConditionalType = { reprPrec := Semantics.Conditionals.instReprConditionalType.repr }

instance Semantics.Conditionals.instBEqConditionalType : BEq ConditionalType

Equations

• Semantics.Conditionals.instBEqConditionalType = { beq := Semantics.Conditionals.instBEqConditionalType.beq }

def Semantics.Conditionals.instBEqConditionalType.beq : ConditionalType → ConditionalType → Bool

Equations

• Semantics.Conditionals.instBEqConditionalType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Conditionals.instInhabitedConditionalType.default : ConditionalType

Equations

• Semantics.Conditionals.instInhabitedConditionalType.default = Semantics.Conditionals.ConditionalType.hypothetical

instance Semantics.Conditionals.instInhabitedConditionalType : Inhabited ConditionalType

Equations

• Semantics.Conditionals.instInhabitedConditionalType = { default := Semantics.Conditionals.instInhabitedConditionalType.default }

def Semantics.Conditionals.ConditionalType.impliesUncertainty : ConditionalType → Bool

Whether a conditional type implies speaker uncertainty about the antecedent

Equations

• Semantics.Conditionals.ConditionalType.hypothetical.impliesUncertainty = true
• Semantics.Conditionals.ConditionalType.premise.impliesUncertainty = false

def Semantics.Conditionals.ConditionalType.requiresDiscourseAnchor : ConditionalType → Bool

Whether a conditional type requires discourse anchoring

Equations

• Semantics.Conditionals.ConditionalType.hypothetical.requiresDiscourseAnchor = false
• Semantics.Conditionals.ConditionalType.premise.requiresDiscourseAnchor = true

@[reducible, inline]

abbrev Semantics.Conditionals.ConditionalType.canUseGivenThat (ct : ConditionalType) : Bool

Can this conditional type be paraphrased with "given that" or "since"?

Definitionally equal to requiresDiscourseAnchor: a conditional admits "given that" paraphrase iff its antecedent is discourse-anchored.

Equations

• ct.canUseGivenThat = ct.requiresDiscourseAnchor

def Semantics.Conditionals.echoesDiscourse {W : Type u_1} (ds : Dynamic.State.DiscourseState W) (p : BProp W) (worlds : List W) : Bool

Check whether a proposition "echoes" the current discourse state.

A proposition p echoes the discourse if:

1. It is entailed by some speaker commitment (dcS), OR
2. It is entailed by some common ground proposition (cg)

This captures the requirement that premise conditionals must have their antecedent grounded in prior discourse.

Equations

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

def Semantics.Conditionals.consistentWithDiscourse {W : Type u_1} (ds : Dynamic.State.DiscourseState W) (p : BProp W) (worlds : List W) : Bool

Weaker echo check: proposition is merely consistent with discourse.

This is a looser condition - the antecedent is at least compatible with what's been established, even if not explicitly entailed.

Equations

• Semantics.Conditionals.consistentWithDiscourse ds p worlds = worlds.any fun (w : W) => ds.compatible w && p w

def Semantics.Conditionals.pcFelicitous {W : Type u_1} (ds : Dynamic.State.DiscourseState W) (antecedent : BProp W) (worlds : List W) : Bool

Felicity condition for premise conditionals.

A PC "if p, then q" is felicitous in discourse state ds iff:

• The antecedent p echoes prior discourse (dcS or cg)

This is the key felicity requirement that distinguishes PC from HC.

Equations

• Semantics.Conditionals.pcFelicitous ds antecedent worlds = Semantics.Conditionals.echoesDiscourse ds antecedent worlds

def Semantics.Conditionals.hcFelicitous {W : Type u_1} (ds : Dynamic.State.DiscourseState W) (antecedent : BProp W) (worlds : List W) : Bool

Felicity condition for hypothetical conditionals.

An HC "if p, then q" is felicitous in discourse state ds iff:

• The antecedent p is consistent with cg (not contradicted)
• The antecedent p is not already established (some uncertainty)

Note: The second condition is captured implicitly - if p were established, a PC reading would be preferred.

Equations

• Semantics.Conditionals.hcFelicitous ds antecedent worlds = Semantics.Conditionals.consistentWithDiscourse ds antecedent worlds

inductive Semantics.Conditionals.AntecedentStatus : Type

Epistemic status of an antecedent for polarity licensing purposes.

This is the key insight: polarity licensing in conditional antecedents depends on BOTH monotonicity (semantic) AND epistemic status (discourse).

• hypothetical: Speaker treats antecedent as uncertain → licenses NPIs
• established: Speaker treats antecedent as given → licenses PPIs

• hypothetical : AntecedentStatus
• established : AntecedentStatus

instance Semantics.Conditionals.instDecidableEqAntecedentStatus : DecidableEq AntecedentStatus

Equations

• Semantics.Conditionals.instDecidableEqAntecedentStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Conditionals.instReprAntecedentStatus : Repr AntecedentStatus

Equations

• Semantics.Conditionals.instReprAntecedentStatus = { reprPrec := Semantics.Conditionals.instReprAntecedentStatus.repr }

def Semantics.Conditionals.instReprAntecedentStatus.repr : AntecedentStatus → ℕ → Std.Format

Equations

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

instance Semantics.Conditionals.instBEqAntecedentStatus : BEq AntecedentStatus

Equations

• Semantics.Conditionals.instBEqAntecedentStatus = { beq := Semantics.Conditionals.instBEqAntecedentStatus.beq }

def Semantics.Conditionals.instBEqAntecedentStatus.beq : AntecedentStatus → AntecedentStatus → Bool

Equations

• Semantics.Conditionals.instBEqAntecedentStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Conditionals.instInhabitedAntecedentStatus.default : AntecedentStatus

Equations

• Semantics.Conditionals.instInhabitedAntecedentStatus.default = Semantics.Conditionals.AntecedentStatus.hypothetical

instance Semantics.Conditionals.instInhabitedAntecedentStatus : Inhabited AntecedentStatus

Equations

• Semantics.Conditionals.instInhabitedAntecedentStatus = { default := Semantics.Conditionals.instInhabitedAntecedentStatus.default }

def Semantics.Conditionals.ConditionalType.toAntecedentStatus : ConditionalType → AntecedentStatus

Get the antecedent status from a conditional type.

Equations

• Semantics.Conditionals.ConditionalType.hypothetical.toAntecedentStatus = Semantics.Conditionals.AntecedentStatus.hypothetical
• Semantics.Conditionals.ConditionalType.premise.toAntecedentStatus = Semantics.Conditionals.AntecedentStatus.established

structure Semantics.Conditionals.ConditionalPolarityContext : Type

Full polarity context for conditional antecedents.

Separates the two factors that determine polarity licensing:

1. monotonicity: Semantic DE/UE property (conditional antecedents are DE)
2. epistemicStatus: Discourse-level status (uncertain vs established)

NPI licensing requires: DE monotonicity + hypothetical status PPI licensing requires: established status (monotonicity irrelevant)

• monotonicity : Core.NaturalLogic.ContextPolarity

  Semantic monotonicity (conditional antecedents are always DE)

• epistemicStatus : AntecedentStatus

  Discourse-level epistemic status

def Semantics.Conditionals.instDecidableEqConditionalPolarityContext.decEq (x✝ x✝¹ : ConditionalPolarityContext) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Conditionals.instDecidableEqConditionalPolarityContext : DecidableEq ConditionalPolarityContext

Equations

• Semantics.Conditionals.instDecidableEqConditionalPolarityContext = Semantics.Conditionals.instDecidableEqConditionalPolarityContext.decEq

def Semantics.Conditionals.instReprConditionalPolarityContext.repr : ConditionalPolarityContext → ℕ → Std.Format

Equations

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

instance Semantics.Conditionals.instReprConditionalPolarityContext : Repr ConditionalPolarityContext

Equations

• Semantics.Conditionals.instReprConditionalPolarityContext = { reprPrec := Semantics.Conditionals.instReprConditionalPolarityContext.repr }

def Semantics.Conditionals.ConditionalPolarityContext.fromConditionalType (ct : ConditionalType) : ConditionalPolarityContext

Create polarity context from conditional type.

All conditional antecedents are semantically DE; the epistemic status varies based on whether it's an HC or PC.

Equations

• Semantics.Conditionals.ConditionalPolarityContext.fromConditionalType ct = { epistemicStatus := ct.toAntecedentStatus }

def Semantics.Conditionals.ConditionalPolarityContext.licensesNPI (ctx : ConditionalPolarityContext) : Bool

Does this context license NPIs?

NPIs require BOTH:

1. Downward-entailing monotonicity (semantic)
2. Hypothetical epistemic status (discourse)

This explains why PCs block NPIs despite being DE!

Equations

• ctx.licensesNPI = (ctx.monotonicity == Core.NaturalLogic.ContextPolarity.downward && ctx.epistemicStatus == Semantics.Conditionals.AntecedentStatus.hypothetical)

def Semantics.Conditionals.ConditionalPolarityContext.licensesPPI (ctx : ConditionalPolarityContext) : Bool

Does this context license PPIs?

PPIs are licensed when the antecedent has established status. (Monotonicity is irrelevant for PPI licensing.)

Equations

• ctx.licensesPPI = (ctx.epistemicStatus == Semantics.Conditionals.AntecedentStatus.established)

theorem Semantics.Conditionals.pc_felicity {W : Type u_1} (ds : Dynamic.State.DiscourseState W) (p : BProp W) (worlds : List W) : pcFelicitous ds p worlds = echoesDiscourse ds p worlds

PCs are felicitous iff antecedent echoes prior discourse.

This is the defining felicity condition for premise conditionals.

theorem Semantics.Conditionals.hc_licenses_npi : (ConditionalPolarityContext.fromConditionalType ConditionalType.hypothetical).licensesNPI = true

HCs license NPIs in the antecedent.

Because HCs have both:

• DE monotonicity (semantic property of conditional antecedents)
• Hypothetical epistemic status (speaker uncertainty)

theorem Semantics.Conditionals.pc_licenses_ppi : (ConditionalPolarityContext.fromConditionalType ConditionalType.premise).licensesPPI = true

PCs license PPIs in the antecedent.

Because PCs have established epistemic status.

theorem Semantics.Conditionals.pc_blocks_npi : (ConditionalPolarityContext.fromConditionalType ConditionalType.premise).licensesNPI = false

PCs do NOT license NPIs in the antecedent.

Despite being semantically DE, PCs lack the hypothetical epistemic status required for NPI licensing. This is the key insight from @cite{cao-white-lassiter-2025}.

theorem Semantics.Conditionals.hc_blocks_ppi : (ConditionalPolarityContext.fromConditionalType ConditionalType.hypothetical).licensesPPI = false

HCs do NOT license PPIs in the antecedent.

Because HCs have hypothetical (not established) epistemic status.

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

A conditional with its interpretation type made explicit.

This bundles the antecedent, consequent, and interpretation type together. Useful for analyzing how different readings affect discourse update.

• antecedent : BProp W

  The antecedent proposition

• consequent : BProp W

  The consequent proposition

• condType : ConditionalType

  The interpretation type (HC or PC)

def Semantics.Conditionals.TypedConditional.semantics {W : Type u_1} (tc : TypedConditional W) : BProp W

Get the semantic content (same for both HC and PC)

Equations

• tc.semantics = Semantics.Conditionals.materialImpB tc.antecedent tc.consequent

def Semantics.Conditionals.TypedConditional.isFelicitous {W : Type u_1} (tc : TypedConditional W) (ds : Dynamic.State.DiscourseState W) (worlds : List W) : Bool

Check felicity in a given discourse state

Equations

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

def Semantics.Conditionals.TypedConditional.antecedentPolarityContext {W : Type u_1} (tc : TypedConditional W) : ConditionalPolarityContext

Get the polarity context for the antecedent

Equations

• tc.antecedentPolarityContext = Semantics.Conditionals.ConditionalPolarityContext.fromConditionalType tc.condType

theorem Semantics.Conditionals.hc_pc_same_semantics {W : Type u_1} (p q : BProp W) : { antecedent := p, consequent := q, condType := ConditionalType.hypothetical }.semantics = { antecedent := p, consequent := q, condType := ConditionalType.premise }.semantics

HCs and PCs have identical truth conditions.

The distinction is entirely in felicity/discourse conditions, not semantics. Both are interpreted via the same conditional semantics (material, strict, Kratzer, etc.).

inductive Semantics.Conditionals.ConditionalMarkerType : Type

Cross-linguistic conditional markers and their type restrictions.

Some languages have distinct lexical items for HC vs PC conditionals. This captures the typological pattern.

Note: pcOnly is currently uninstantiated across known languages; included for typological completeness.

• hcOnly : ConditionalMarkerType
• pcOnly : ConditionalMarkerType
• both : ConditionalMarkerType

instance Semantics.Conditionals.instDecidableEqConditionalMarkerType : DecidableEq ConditionalMarkerType

Equations

• Semantics.Conditionals.instDecidableEqConditionalMarkerType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Conditionals.instReprConditionalMarkerType.repr : ConditionalMarkerType → ℕ → Std.Format

Equations

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

instance Semantics.Conditionals.instReprConditionalMarkerType : Repr ConditionalMarkerType

Equations

• Semantics.Conditionals.instReprConditionalMarkerType = { reprPrec := Semantics.Conditionals.instReprConditionalMarkerType.repr }

instance Semantics.Conditionals.instBEqConditionalMarkerType : BEq ConditionalMarkerType

Equations

• Semantics.Conditionals.instBEqConditionalMarkerType = { beq := Semantics.Conditionals.instBEqConditionalMarkerType.beq }

def Semantics.Conditionals.instBEqConditionalMarkerType.beq : ConditionalMarkerType → ConditionalMarkerType → Bool

Equations

• Semantics.Conditionals.instBEqConditionalMarkerType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Semantics.Conditionals.ConditionalMarker : Type

Cross-linguistic conditional marker datum.

Per-language marker entries live in Fragments/{Language}/Conditionals.lean.

• language : String
• marker : String
• gloss : String
• markerType : ConditionalMarkerType
• notes : String

def Semantics.Conditionals.instReprConditionalMarker.repr : ConditionalMarker → ℕ → Std.Format

Equations

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

instance Semantics.Conditionals.instReprConditionalMarker : Repr ConditionalMarker

Equations

• Semantics.Conditionals.instReprConditionalMarker = { reprPrec := Semantics.Conditionals.instReprConditionalMarker.repr }

Summary

This module provides:

Types

• ConditionalType: HC vs PC distinction
• AntecedentStatus: Epistemic status for polarity
• ConditionalPolarityContext: Full polarity context (monotonicity + epistemic)
• TypedConditional: Conditional with explicit interpretation type
• ConditionalMarkerType / ConditionalMarker: Marker type vocabulary (per-language data in Fragments/{Language}/Conditionals.lean)

Key Operations

• echoesDiscourse: Check if proposition echoes prior discourse
• pcFelicitous: Felicity condition for premise conditionals
• hcFelicitous: Felicity condition for hypothetical conditionals
• licensesNPI: Check if context licenses NPIs
• licensesPPI: Check if context licenses PPIs

Theorems

• hc_pc_same_semantics: HCs and PCs have identical truth conditions
• hc_licenses_npi: HCs license NPIs in antecedent
• pc_licenses_ppi: PCs license PPIs in antecedent
• pc_blocks_npi: PCs do NOT license NPIs (key insight!)
• hc_blocks_ppi: HCs do NOT license PPIs

Insight

The HC/PC distinction is DISCOURSE-LEVEL, not semantic. The polarity licensing pattern requires separating:

1. Monotonicity (semantic) - always DE in conditional antecedents
2. Epistemic status (discourse) - uncertain (HC) vs established (PC)

This explains the apparent paradox that PCs block NPIs despite being semantically DE: NPI licensing requires BOTH DE + uncertain status.