Lassiter (2025): Sorting Out Left-Nested Conditionals

This file formalizes Lassiter's account of left-nested conditionals, conditionals with another conditional in their antecedent, such as Gibbard's If Kripke was there if Strawson was, then Anscomb was there. A conditional is construed as hypothetical or as a premise conditional (Iatridou); a left-nested conditional whose embedded conditional is bare admits only the premise reading, while an embedded modal, adverb of quantification, or generic operator restores the hypothetical one (readings). A sentence is acceptable when some reading open to it meets what its context and diagnostics demand (Acceptable), so for a bare left-nested conditional every diagnostic reduces to the premise reading (acceptable_bare_iff). The paper's eight diagnostics are demands on the reading. A premise reading needs its antecedent given in the discourse and a hypothetical one needs it open (anchoring, the discourse condition felicitous of Iatridou and Haegeman in the two contexts the paper uses, anchoring_iff_felicitous), so bare left-nested conditionals are odd out of the blue and improve once the embedded conditional has been asserted. Japanese -ra and German falls, restricted to hypothetical conditionals, cannot head a bare left-nested conditional, whereas nara and wenn can (heads_bare_iff). The clauses of the embedded conditional take their entailment direction from the main antecedent's (Position.polarity), so a bare left-nested conditional hosts positive polarity items and rejects negative ones, the minimizer lift a finger among them (Israel), in the embedded consequent and hosts them in the embedded antecedent (bare_embedded_consequent, bare_embedded_antecedent), the reverse of what a hypothetical reading would give (polarity_diagnostic). Coordinated antecedents share a reading (Haegeman and Schönenberger), so a bare left-nested conditional coordinates only with a given antecedent (coordination_bare), and initial only with inversion, which forces the hypothetical reading, excludes it (bare_not_hypothetical). demand reads each row's diagnostics off its features, and acceptable_rows checks every row's judgment against the model, interpretation_rows the reading the paper attributes to it.

Implementation notes

Polarity items are sorted by Israel's scalar context types rather than by the Zwarts strength of PolarityItem.Licenser.Licenses. That relation reads a conditional antecedent as anti-additive only modulo its presupposition and lift a finger as needing an anti-additive licensor outright, so it would exclude the minimizer from hypothetical antecedents, against Iatridou's (27a) and the paper's (32); on the scalar account a minimizer needs only a scale-reversing context. The paper's rows carry their features as strings, so shape, markerOf, itemOf, and positionOf are adapters from paperFeatures into the typed model and the fragments' entries; adapters_total checks that every marker and item named in a row resolves, so the row theorems are not vacuous. Gibbard's (4) is annotated with the premise reading it has, in a context where that reading is infelicitous; interpretation_rows therefore checks the attributed reading only on acceptable rows. The speaker-oriented epistemics of section 4, which the paper offers as a direction rather than a result, are not modelled.

References

• [Las25]
• [Gib81]
• [Iat91]
• [Hae03]
• [HS23]
• [Isr01]

inductive Lassiter2025.Content : Type

The content of an embedded conditional.

• bare : Content
• modal : Content
• quantAdv : Content
• generic : Content

@[instance_reducible]

instance Lassiter2025.instDecidableEqContent : DecidableEq Content

Equations

• Lassiter2025.instDecidableEqContent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lassiter2025.instReprContent.repr : Content → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Lassiter2025.instReprContent.repr Lassiter2025.Content.bare prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lassiter2025.Content.bare")).group prec✝

@[instance_reducible]

instance Lassiter2025.instReprContent : Repr Content

Equations

• Lassiter2025.instReprContent = { reprPrec := Lassiter2025.instReprContent.repr }

inductive Lassiter2025.Shape : Type

A conditional's antecedent is simple or is itself a conditional with the given content.

• simple : Shape
• nested (content : Content) : Shape

@[instance_reducible]

instance Lassiter2025.instDecidableEqShape : DecidableEq Shape

Equations

• Lassiter2025.instDecidableEqShape = Lassiter2025.instDecidableEqShape.decEq

def Lassiter2025.instDecidableEqShape.decEq (x✝ x✝¹ : Shape) : Decidable (x✝ = x✝¹)

Equations

• Lassiter2025.instDecidableEqShape.decEq Lassiter2025.Shape.simple Lassiter2025.Shape.simple = isTrue ⋯
• Lassiter2025.instDecidableEqShape.decEq Lassiter2025.Shape.simple (Lassiter2025.Shape.nested content) = isFalse ⋯
• Lassiter2025.instDecidableEqShape.decEq (Lassiter2025.Shape.nested content) Lassiter2025.Shape.simple = isFalse ⋯
• Lassiter2025.instDecidableEqShape.decEq (Lassiter2025.Shape.nested a) (Lassiter2025.Shape.nested b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Lassiter2025.instReprShape : Repr Shape

Equations

• Lassiter2025.instReprShape = { reprPrec := Lassiter2025.instReprShape.repr }

def Lassiter2025.instReprShape.repr : Shape → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Lassiter2025.instReprShape.repr Lassiter2025.Shape.simple prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lassiter2025.Shape.simple")).group prec✝

def Lassiter2025.readings : Shape → Finset Conditional.Reading

The readings open to a conditional, where a bare embedded conditional leaves only the premise reading.

Equations

• Lassiter2025.readings (Lassiter2025.Shape.nested Lassiter2025.Content.bare) = {Conditional.Reading.premise}
• Lassiter2025.readings x✝ = {Conditional.Reading.hypothetical, Conditional.Reading.premise}

def Lassiter2025.Acceptable (s : Shape) (ok : Conditional.Reading → Prop) : Prop

A conditional is acceptable under a demand on its reading iff some reading open to it meets the demand.

Equations

• Lassiter2025.Acceptable s ok = ∃ ct ∈ Lassiter2025.readings s, ok ct

@[instance_reducible]

instance Lassiter2025.instDecidableAcceptableOfDecidablePredReading (s : Shape) (ok : Conditional.Reading → Prop) [DecidablePred ok] : Decidable (Acceptable s ok)

Equations

• Lassiter2025.instDecidableAcceptableOfDecidablePredReading s ok = id inferInstance

theorem Lassiter2025.acceptable_bare_iff (ok : Conditional.Reading → Prop) : Acceptable (Shape.nested Content.bare) ok ↔ ok Conditional.Reading.premise

A bare left-nested conditional meets a demand iff the premise reading does.

theorem Lassiter2025.readings_of_ne_bare {s : Shape} (h : s ≠ Shape.nested Content.bare) : readings s = Finset.univ

Every other conditional is open to both readings.

theorem Lassiter2025.acceptable_iff_of_ne_bare {s : Shape} (h : s ≠ Shape.nested Content.bare) (ok : Conditional.Reading → Prop) : Acceptable s ok ↔ ∃ (ct : Conditional.Reading), ok ct

Every other conditional meets a demand iff some reading does.

Discourse anchoring, sections 2.1, 2.4, and 2.5

A premise conditional needs its antecedent given, explicitly or by inference, in the prior discourse, and a hypothetical one needs it open. Coordinated antecedents share a reading, and initial only with subject–auxiliary inversion forces the hypothetical reading ([HS23]).

def Lassiter2025.anchoring (isGiven : Prop) (ct : Conditional.Reading) : Prop

The antecedent's discourse status demands a reading, the premise reading for a given antecedent and the hypothetical reading for an open one.

Equations

• Lassiter2025.anchoring isGiven ct = (ct = Conditional.Reading.premise ↔ isGiven)

@[instance_reducible]

instance Lassiter2025.instDecidablePredReadingAnchoringOfDecidable (isGiven : Prop) [Decidable isGiven] : DecidablePred (anchoring isGiven)

Equations

• Lassiter2025.instDecidablePredReadingAnchoringOfDecidable isGiven x✝ = { decide := decide (x✝ = Conditional.Reading.premise) == decide isGiven, reflects_decide := ⋯ }

def Lassiter2025.felicitous {A : Type u_1} {W : Type u_2} (K : Commitment.Table A W) (p : Set W) : Conditional.Reading → Prop

A reading is felicitous for the antecedent p in the commitment table K when p meets its discourse condition ([Iat91], [Hae03]). A hypothetical conditional leaves p undecided in the common ground, and a premise conditional needs p committed to by some participant or already in the common ground.

Equations

• Lassiter2025.felicitous K p Conditional.Reading.hypothetical = ¬(Question.polar p).DecidedBy K.commonGround
• Lassiter2025.felicitous K p Conditional.Reading.premise = ((∃ (a : A), p ∈ K.discourseCommitments a) ∨ p ∈ K.commonGround)

theorem Lassiter2025.felicitous_iff_of_mem_commonGround {A : Type u_1} {W : Type u_2} {K : Commitment.Table A W} {p : Set W} (h : p ∈ K.commonGround) {ct : Conditional.Reading} : felicitous K p ct ↔ ct = Conditional.Reading.premise

An antecedent the common ground entails is read as a premise.

theorem Lassiter2025.felicitous_iff_of_not_decidedBy {A : Type u_1} {W : Type u_2} {K : Commitment.Table A W} {p : Set W} (h₁ : ∀ (a : A), p ∉ K.discourseCommitments a) (h₂ : ¬(Question.polar p).DecidedBy K.commonGround) {ct : Conditional.Reading} : felicitous K p ct ↔ ct = Conditional.Reading.hypothetical

An antecedent nobody has committed to and whose polar question is open is read hypothetically.

theorem Lassiter2025.anchoring_iff_felicitous {A : Type u_1} {W : Type u_2} {K : Commitment.Table A W} {p : Set W} (h : p ∈ K.commonGround ∨ (∀ (a : A), p ∉ K.discourseCommitments a) ∧ ¬(Question.polar p).DecidedBy K.commonGround) (ct : Conditional.Reading) : anchoring (p ∈ K.commonGround) ct ↔ felicitous K p ct

anchoring is the felicity condition in the two contexts the paper uses: one whose common ground entails the antecedent, and one in which nobody has committed to it and its polar question is open.

theorem Lassiter2025.bare_not_hypothetical : ¬Acceptable (Shape.nested Content.bare) fun (x : Conditional.Reading) => x = Conditional.Reading.hypothetical

Gibbard's puzzle is that a bare left-nested conditional has no reading out of the blue, (4), and none under only-inversion, which forces the hypothetical reading, (38b) and (39b).

theorem Lassiter2025.bare_premise : Acceptable (Shape.nested Content.bare) fun (x : Conditional.Reading) => x = Conditional.Reading.premise

A bare left-nested conditional is a premise conditional once its embedded conditional has been asserted, (11)–(13).

theorem Lassiter2025.hypothetical_of_ne_bare (c : Content) (h : c ≠ Content.bare) : Acceptable (Shape.nested c) fun (x : Conditional.Reading) => x = Conditional.Reading.hypothetical

The exception of section 3 is that a modal, quantificational, or generic embedded conditional admits the hypothetical reading, (40)–(43).

theorem Lassiter2025.not_acceptable_coordination_of_not_iff (s : Shape) {g₁ g₂ : Prop} (h : ¬(g₁ ↔ g₂)) : ¬Acceptable s fun (ct : Conditional.Reading) => anchoring g₁ ct ∧ anchoring g₂ ct

Coordinated antecedents share a reading, so a conditional whose antecedents differ in discourse status has none, (33).

theorem Lassiter2025.coordination_bare (g₁ g₂ : Prop) : (Acceptable (Shape.nested Content.bare) fun (ct : Conditional.Reading) => anchoring g₁ ct ∧ anchoring g₂ ct) ↔ g₁ ∧ g₂

A bare left-nested conditional coordinates with a simple antecedent iff both are given, (34) against (35).

Markers, section 2.2

theorem Lassiter2025.heads_bare_iff (m : Conditional.Marker) : (Acceptable (Shape.nested Content.bare) fun (x : Conditional.Reading) => x ∈ m.readings) ↔ Conditional.Reading.premise ∈ m.readings

A marker heads a bare left-nested conditional iff it can mark a premise conditional: nara and wenn do, (18) and (23), -ra and falls do not, (19) and (24).

Polarity items, section 2.3

HCs take negative polarity items in their antecedents and not positive ones, and PCs the reverse ([Iat91]). [Isr01] derives the two classes: an item is sensitive to scale-reversing or scale-preserving contexts (Israel2001.PolarityItem.contextType), and the downward-entailing positions are the reversing ones. The embedded conditional sits in the main antecedent, so each of its clauses composes its own entailment direction with the main antecedent's.

inductive Lassiter2025.Position : Type

A clause of the main conditional, or of the embedded conditional in its antecedent.

• main (c : Conditional.Clause) : Position
• embedded (c : Conditional.Clause) : Position

@[instance_reducible]

instance Lassiter2025.instDecidableEqPosition : DecidableEq Position

Equations

• Lassiter2025.instDecidableEqPosition = Lassiter2025.instDecidableEqPosition.decEq

def Lassiter2025.instDecidableEqPosition.decEq (x✝ x✝¹ : Position) : Decidable (x✝ = x✝¹)

Equations

• Lassiter2025.instDecidableEqPosition.decEq (Lassiter2025.Position.main a) (Lassiter2025.Position.main b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Lassiter2025.instDecidableEqPosition.decEq (Lassiter2025.Position.main c) (Lassiter2025.Position.embedded c_1) = isFalse ⋯
• Lassiter2025.instDecidableEqPosition.decEq (Lassiter2025.Position.embedded c) (Lassiter2025.Position.main c_1) = isFalse ⋯
• Lassiter2025.instDecidableEqPosition.decEq (Lassiter2025.Position.embedded a) (Lassiter2025.Position.embedded b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Lassiter2025.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Lassiter2025.instReprPosition : Repr Position

Equations

• Lassiter2025.instReprPosition = { reprPrec := Lassiter2025.instReprPosition.repr }

def Lassiter2025.Position.polarity (ct : Conditional.Reading) : Position → SignType

The entailment direction of a position under a reading of the main conditional. A main clause has its reading's direction, and a clause of the embedded conditional, read hypothetically, composes its direction with the main antecedent's.

Equations

• Lassiter2025.Position.polarity ct (Lassiter2025.Position.main c) = ct.clausePolarity c
• Lassiter2025.Position.polarity ct (Lassiter2025.Position.embedded c) = ct.clausePolarity Conditional.Clause.antecedent * Conditional.Reading.hypothetical.clausePolarity c

def Lassiter2025.Position.contextType (ct : Conditional.Reading) (pos : Position) : Polarity

The scalar context a position provides, which downward-entailing positions reverse.

Equations

• Lassiter2025.Position.contextType ct pos = if Lassiter2025.Position.polarity ct pos = -1 then Polarity.negative else Polarity.positive

def Lassiter2025.admits (ct : Conditional.Reading) (pos : Position) (e : PolarityItem) : Prop

The item e is admitted at pos under the reading ct when the position provides the context it is sensitive to.

Equations

• Lassiter2025.admits ct pos e = (Israel2001.PolarityItem.contextType e = some (Lassiter2025.Position.contextType ct pos))

@[instance_reducible]

instance Lassiter2025.instDecidableAdmits (ct : Conditional.Reading) (pos : Position) (e : PolarityItem) : Decidable (admits ct pos e)

Equations

• Lassiter2025.instDecidableAdmits ct pos e = Lassiter2025.instDecidableAdmits._aux_1 ct pos e

theorem Lassiter2025.polarity_embedded_consequent (ct : Conditional.Reading) : Position.polarity ct (Position.embedded Conditional.Clause.consequent) = ct.clausePolarity Conditional.Clause.antecedent

The embedded consequent takes the main antecedent's direction.

theorem Lassiter2025.polarity_embedded_antecedent : Position.polarity Conditional.Reading.premise (Position.embedded Conditional.Clause.antecedent) = -1 ∧ Position.polarity Conditional.Reading.hypothetical (Position.embedded Conditional.Clause.antecedent) = 1

The embedded antecedent reverses it.

theorem Lassiter2025.bare_embedded_consequent (e : PolarityItem) : (Acceptable (Shape.nested Content.bare) fun (x : Conditional.Reading) => admits x (Position.embedded Conditional.Clause.consequent) e) ↔ Israel2001.PolarityItem.contextType e = some Polarity.positive

In the consequent of its embedded conditional, a bare left-nested conditional hosts items sensitive to preserving contexts, rather pleased in (29), and not the minimizer lifted a finger of (30).

theorem Lassiter2025.bare_embedded_antecedent (e : PolarityItem) : (Acceptable (Shape.nested Content.bare) fun (x : Conditional.Reading) => admits x (Position.embedded Conditional.Clause.antecedent) e) ↔ Israel2001.PolarityItem.contextType e = some Polarity.negative

In the antecedent of its embedded conditional, a bare left-nested conditional hosts items sensitive to reversing contexts: lifted a finger in (32b).

theorem Lassiter2025.polarity_diagnostic : admits Conditional.Reading.hypothetical (Position.embedded Conditional.Clause.consequent) English.PolarityItems.liftAFinger ∧ ¬admits Conditional.Reading.hypothetical (Position.embedded Conditional.Clause.consequent) English.PolarityItems.rather

The diagnostic has force because on a hypothetical reading the embedded consequent would reverse the scale, admitting lifted a finger and rejecting rather, the reverse of (29) and (30).

The paper's examples

def Lassiter2025.shape (row : Datum) : Shape

The row's shape, read from its is_lnc and content features.

Equations

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

def Lassiter2025.markerOf (row : Datum) : Option Conditional.Marker

The fragment entry for the row's main conditional marker.

Equations

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

def Lassiter2025.itemOf (row : Datum) : Option PolarityItem

The fragment entry for the row's polarity item.

Equations

• Lassiter2025.itemOf row = row.parse? "item" (List.map (fun (p : PolarityItem) => (p.form, p)) English.PolarityItems.allPolarityItems)

def Lassiter2025.positionOf (row : Datum) : Option Position

The position of the row's polarity item.

Equations

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

def Lassiter2025.flag? (row : Datum) (key : String) : Option Bool

A Boolean feature of the row, when annotated.

Equations

• Lassiter2025.flag? row key = match row.feature? key with | some "true" => some true | some "false" => some false | x => none

def Lassiter2025.demand (row : Datum) (ct : Conditional.Reading) : Prop

The row's diagnostics demand of the reading that its marker mark it, that its antecedent and any coordinated antecedent have the discourse status the reading needs, that only-inversion force the hypothetical reading, and that its polarity item be admitted at its position.

Equations

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

@[instance_reducible]

instance Lassiter2025.instDecidableDemand (row : Datum) (ct : Conditional.Reading) : Decidable (demand row ct)

Equations

• Lassiter2025.instDecidableDemand row ct = id inferInstance

theorem Lassiter2025.adapters_total (row : Datum) : row ∈ Examples.all → ((row.feature? "marker").isSome = true → (markerOf row).isSome = true) ∧ ((row.feature? "item").isSome = true → (itemOf row).isSome = true)

Every marker and item a row names resolves to a fragment entry.

theorem Lassiter2025.acceptable_rows (row : Datum) : row ∈ Examples.all → (row.JudgedFelicitous ↔ Acceptable (shape row) (demand row))

Every row is judged felicitous iff some reading open to its shape meets its demand. Gibbard's (4) fails out of the blue and (11)–(14) succeed once the embedded conditional has been asserted; nara and wenn head the bare left-nested conditionals of (18) and (23), -ra and falls of (19) and (24) do not; rather survives in the embedded consequent of (29) and lifted a finger does not, in (30), nor in the consequent of (31), while it is licensed in the embedded antecedent of (32b); (34) coordinates two given antecedents and (33) and (35) mix; (36) inverts with an open antecedent, (37b) with a given one, (38b) and (39b) in a bare left-nested conditional; and (40)–(43) are hypothetical with an open antecedent.

def Lassiter2025.label : Conditional.Reading → String

The paper's label for a reading.

Equations

• Lassiter2025.label Conditional.Reading.hypothetical = "HC"
• Lassiter2025.label Conditional.Reading.premise = "PC"

theorem Lassiter2025.interpretation_rows (row : Datum) : row ∈ Examples.all → row.JudgedFelicitous → ∀ (ct : Conditional.Reading), row.feature? "interpretation" = some (label ct) → ∀ (ct' : Conditional.Reading), ct' ∈ readings (shape row) ∧ demand row ct' ↔ ct' = ct

On every felicitous row, the reading the paper attributes is the one reading open to its shape that meets its demand.