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

Left-nested conditional structure: "If (B if A), C"

The structure of an LNC where the outer antecedent is itself a conditional.

Example: "If Kripke was there if Strawson was, Anscomb was there"

• innerAntecedent = "Strawson was there"
• innerConsequent = "Kripke was there"
• outerConsequent = "Anscomb was there"

• innerAntecedent : BProp W

  A: The inner antecedent

• innerConsequent : BProp W

  B: The inner consequent

• outerConsequent : BProp W

  C: The outer consequent

def Semantics.Conditionals.LNC.innerConditional {W : Type u_1} (lnc : LNC W) : BProp W

Get the inner conditional "B if A" as a proposition.

This is the outer antecedent of the full LNC.

Equations

• lnc.innerConditional = Semantics.Conditionals.materialImpB lnc.innerAntecedent lnc.innerConsequent

def Semantics.Conditionals.LNC.semantics {W : Type u_1} (lnc : LNC W) : BProp W

Full LNC semantics using material implication.

"If (B if A), C" = (A → B) → C

Equations

• lnc.semantics = Semantics.Conditionals.materialImpB lnc.innerConditional lnc.outerConsequent

def Semantics.Conditionals.LNC.kratzerSemantics {W : Type u_1} (ctx : KratzerContext W) (lnc : LNC W) : Prop' W

Full LNC semantics using Kratzer-style conditionals.

The outer conditional uses the Kratzer semantics with modal base and ordering source, while the inner conditional is the restrictor.

Equations

• Semantics.Conditionals.LNC.kratzerSemantics ctx lnc = Semantics.Conditionals.kratzerConditional ctx (fun (w : W) => lnc.innerConditional w = true) fun (w : W) => lnc.outerConsequent w = true

inductive Semantics.Conditionals.InnerConditionalContent : Type

Classification of the inner conditional's content.

The content type determines whether the LNC can be interpreted as an HC. Bare conditionals force PC reading; modals/generics allow HC reading.

• bare : InnerConditionalContent

  No modal/generic content → forces PC reading

• modal : InnerConditionalContent

  Has modal verb/operator → allows HC reading

• generic : InnerConditionalContent

  Generic/habitual → allows HC reading

• quantAdv : InnerConditionalContent

  Quantificational adverb (always, usually, etc.) → allows HC reading

instance Semantics.Conditionals.instDecidableEqInnerConditionalContent : DecidableEq InnerConditionalContent

Equations

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

instance Semantics.Conditionals.instReprInnerConditionalContent : Repr InnerConditionalContent

Equations

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

def Semantics.Conditionals.instReprInnerConditionalContent.repr : InnerConditionalContent → ℕ → Std.Format

Equations

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

def Semantics.Conditionals.instBEqInnerConditionalContent.beq : InnerConditionalContent → InnerConditionalContent → Bool

Equations

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

instance Semantics.Conditionals.instBEqInnerConditionalContent : BEq InnerConditionalContent

Equations

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

def Semantics.Conditionals.instInhabitedInnerConditionalContent.default : InnerConditionalContent

Equations

• Semantics.Conditionals.instInhabitedInnerConditionalContent.default = Semantics.Conditionals.InnerConditionalContent.bare

instance Semantics.Conditionals.instInhabitedInnerConditionalContent : Inhabited InnerConditionalContent

Equations

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

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

Does this content type require discourse anchoring for the inner conditional?

Equations

• Semantics.Conditionals.InnerConditionalContent.bare.requiresDiscourseAnchor = true
• Semantics.Conditionals.InnerConditionalContent.modal.requiresDiscourseAnchor = false
• Semantics.Conditionals.InnerConditionalContent.generic.requiresDiscourseAnchor = false
• Semantics.Conditionals.InnerConditionalContent.quantAdv.requiresDiscourseAnchor = false

def Semantics.Conditionals.InnerConditionalContent.allowsHCReading : InnerConditionalContent → Bool

Can this content type be interpreted as an HC?

Equations

• Semantics.Conditionals.InnerConditionalContent.bare.allowsHCReading = false
• Semantics.Conditionals.InnerConditionalContent.modal.allowsHCReading = true
• Semantics.Conditionals.InnerConditionalContent.generic.allowsHCReading = true
• Semantics.Conditionals.InnerConditionalContent.quantAdv.allowsHCReading = true

def Semantics.Conditionals.interpretLNC {W : Type u_1} (ds : Dynamic.State.DiscourseState W) (lnc : LNC W) (content : InnerConditionalContent) (worlds : List W) : ConditionalType

Interpret an LNC given discourse context and content type.

The main result of @cite{cao-white-lassiter-2025}: bare LNCs default to PC interpretation.

Equations

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

def Semantics.Conditionals.lncFelicitous {W : Type u_1} (ds : Dynamic.State.DiscourseState W) (lnc : LNC W) (content : InnerConditionalContent) (worlds : List W) : Bool

Check if an LNC is felicitous in a given discourse state.

Equations

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

theorem Semantics.Conditionals.bare_lnc_as_pc {W : Type u_1} (ds : Dynamic.State.DiscourseState W) (lnc : LNC W) (worlds : List W) : interpretLNC ds lnc InnerConditionalContent.bare worlds = ConditionalType.premise

Main result: Bare LNCs default to PC interpretation.

When the inner conditional has bare content (no modal/generic/quantAdv), the LNC is interpreted as a premise conditional, regardless of discourse.

theorem Semantics.Conditionals.modal_lnc_allows_hc {W : Type u_1} (ds : Dynamic.State.DiscourseState W) (lnc : LNC W) (worlds : List W) (h_no_echo : echoesDiscourse ds lnc.innerConditional worlds = false) : interpretLNC ds lnc InnerConditionalContent.modal worlds = ConditionalType.hypothetical

Exception: Modal LNCs can be HCs.

When the inner conditional has modal content, the LNC can be interpreted as either HC or PC, depending on discourse context.

theorem Semantics.Conditionals.modal_lnc_prefers_pc {W : Type u_1} (ds : Dynamic.State.DiscourseState W) (lnc : LNC W) (worlds : List W) (h_echo : echoesDiscourse ds lnc.innerConditional worlds = true) : interpretLNC ds lnc InnerConditionalContent.modal worlds = ConditionalType.premise

Modal LNCs prefer PC when discourse anchor exists.

theorem Semantics.Conditionals.lnc_grounded {W : Type u_1} (ctx : KratzerContext W) (lnc : LNC W) : LNC.kratzerSemantics ctx lnc = kratzerConditional ctx (fun (w : W) => lnc.innerConditional w = true) fun (w : W) => lnc.outerConsequent w = true

LNC semantics grounded in Kratzer.

The LNC semantics is compositionally derived from Kratzer's conditional semantics - it's not stipulated specially for LNCs.

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

Left-nested conditional with metadata for analysis.

• lnc : LNC W

  The LNC structure

• content : InnerConditionalContent

  Content type of inner conditional

• sentence : String

  String representation for display

• notes : String

  Notes on interpretation

def Semantics.Conditionals.AnnotatedLNC.interpret {W : Type u_1} (alnc : AnnotatedLNC W) (ds : Dynamic.State.DiscourseState W) (worlds : List W) : ConditionalType

Get interpretation in discourse context

Equations

• alnc.interpret ds worlds = Semantics.Conditionals.interpretLNC ds alnc.lnc alnc.content worlds

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

Check felicity

Equations

• alnc.isFelicitous ds worlds = Semantics.Conditionals.lncFelicitous ds alnc.lnc alnc.content worlds

def Semantics.Conditionals.AnnotatedLNC.innerAntecedentPolarity {W : Type u_1} (alnc : AnnotatedLNC W) (ds : Dynamic.State.DiscourseState W) (worlds : List W) : ConditionalPolarityContext

Get polarity context for inner conditional antecedent

Equations

• alnc.innerAntecedentPolarity ds worlds = Semantics.Conditionals.ConditionalPolarityContext.fromConditionalType (alnc.interpret ds worlds)

Polarity Patterns (@cite{cao-white-lassiter-2025}, Section 4)

@cite{gibbard-1981}

The PC analysis of LNCs predicts specific polarity patterns:

In the embedded consequent (B in "if (B if A), C")

• PPIs licensed: "If John helped someone if asked, we're in good shape"
• NPIs blocked: "*If John helped anyone if asked, we're in good shape"

In the inner antecedent (A)

• This position is DE regardless of HC/PC reading
• But polarity licensing also depends on epistemic status

The embedded consequent patterns are diagnostic because:

• In HCs: the embedded consequent is in an epistemic uncertainty context
• In PCs: the embedded consequent is treated as established

structure Semantics.Conditionals.EmbeddedConsequentPolarity : Type

Polarity licensing in the embedded consequent position.

Following @cite{cao-white-lassiter-2025}: the embedded consequent of an LNC (the B position in "if (B if A), C") shows polarity patterns consistent with PC reading.

• licensesPPI : Bool

  Whether the LNC licenses PPIs in B position

• licensesNPI : Bool

  Whether the LNC licenses NPIs in B position

def Semantics.Conditionals.embeddedConsequentPolarity (ct : ConditionalType) : EmbeddedConsequentPolarity

Get polarity licensing for embedded consequent based on LNC interpretation.

Equations

• Semantics.Conditionals.embeddedConsequentPolarity Semantics.Conditionals.ConditionalType.hypothetical = { licensesPPI := false, licensesNPI := true }
• Semantics.Conditionals.embeddedConsequentPolarity Semantics.Conditionals.ConditionalType.premise = { licensesPPI := true, licensesNPI := false }

theorem Semantics.Conditionals.bare_lnc_licenses_ppi_in_B : (embeddedConsequentPolarity ConditionalType.premise).licensesPPI = true

Bare LNCs license PPIs in embedded consequent.

theorem Semantics.Conditionals.bare_lnc_blocks_npi_in_B : (embeddedConsequentPolarity ConditionalType.premise).licensesNPI = false

Bare LNCs block NPIs in embedded consequent.

inductive Semantics.Conditionals.PartyWorld : Type

Simple world type for LNC examples.

Based on the Gibbard scenario: Strawson, Kripke, and Anscomb may or may not have attended a party.

• sOnly : PartyWorld
• kOnly : PartyWorld
• aOnly : PartyWorld
• sk : PartyWorld
• sa : PartyWorld
• ka : PartyWorld
• ska : PartyWorld
• none_ : PartyWorld

instance Semantics.Conditionals.instDecidableEqPartyWorld : DecidableEq PartyWorld

Equations

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

def Semantics.Conditionals.instReprPartyWorld.repr : PartyWorld → ℕ → Std.Format

Equations

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

instance Semantics.Conditionals.instReprPartyWorld : Repr PartyWorld

Equations

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

def Semantics.Conditionals.instBEqPartyWorld.beq : PartyWorld → PartyWorld → Bool

Equations

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

instance Semantics.Conditionals.instBEqPartyWorld : BEq PartyWorld

Equations

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

def Semantics.Conditionals.instInhabitedPartyWorld.default : PartyWorld

Equations

• Semantics.Conditionals.instInhabitedPartyWorld.default = Semantics.Conditionals.PartyWorld.sOnly

instance Semantics.Conditionals.instInhabitedPartyWorld : Inhabited PartyWorld

Equations

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

instance Semantics.Conditionals.instFiniteWorldsPartyWorld : Core.Proposition.FiniteWorlds PartyWorld

Equations

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

def Semantics.Conditionals.PartyWorld.strawsonAttended : BProp PartyWorld

Equations

• Semantics.Conditionals.PartyWorld.sOnly.strawsonAttended = true
• Semantics.Conditionals.PartyWorld.sk.strawsonAttended = true
• Semantics.Conditionals.PartyWorld.sa.strawsonAttended = true
• Semantics.Conditionals.PartyWorld.ska.strawsonAttended = true
• x✝.strawsonAttended = false

def Semantics.Conditionals.PartyWorld.kripkeAttended : BProp PartyWorld

Equations

• Semantics.Conditionals.PartyWorld.kOnly.kripkeAttended = true
• Semantics.Conditionals.PartyWorld.sk.kripkeAttended = true
• Semantics.Conditionals.PartyWorld.ka.kripkeAttended = true
• Semantics.Conditionals.PartyWorld.ska.kripkeAttended = true
• x✝.kripkeAttended = false

def Semantics.Conditionals.PartyWorld.anscombAttended : BProp PartyWorld

Equations

• Semantics.Conditionals.PartyWorld.aOnly.anscombAttended = true
• Semantics.Conditionals.PartyWorld.sa.anscombAttended = true
• Semantics.Conditionals.PartyWorld.ka.anscombAttended = true
• Semantics.Conditionals.PartyWorld.ska.anscombAttended = true
• x✝.anscombAttended = false

def Semantics.Conditionals.PartyWorld.gibbardLNC : LNC PartyWorld

Gibbard's example LNC: "If Kripke was there if Strawson was, Anscomb was there"

Equations

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

Summary

This module provides:

Types

• LNC: Left-nested conditional structure
• InnerConditionalContent: Content type classification (bare/modal/generic/quantAdv)
• AnnotatedLNC: LNC with metadata for analysis
• EmbeddedConsequentPolarity: Polarity licensing in embedded consequent

Key Operations

• LNC.innerConditional: Extract the inner conditional proposition
• LNC.semantics: Material implication semantics
• LNC.kratzerSemantics: Kratzer-style semantics
• interpretLNC: Determine HC/PC interpretation based on content and discourse
• lncFelicitous: Check felicity in discourse context
• embeddedConsequentPolarity: Get polarity licensing for embedded position

Theorems

• bare_lnc_as_pc: Bare LNCs default to PC interpretation
• modal_lnc_allows_hc: Modal LNCs can be HCs (when no discourse anchor)
• modal_lnc_prefers_pc: Modal LNCs prefer PC when discourse anchor exists
• lnc_grounded: LNC semantics from Kratzer conditionals
• bare_lnc_licenses_ppi_in_B: Bare LNCs license PPIs in embedded consequent
• bare_lnc_blocks_npi_in_B: Bare LNCs block NPIs in embedded consequent

Insight

Bare LNCs force PC interpretation because the inner conditional (a propositional object) inherently requires discourse anchoring to be supposed. This explains:

1. Why bare LNCs sound odd out of the blue
2. Why they improve with discourse context
3. Why they pattern with PCs for polarity licensing
4. Why modal/generic LNCs allow HC readings