[CL16] — Anankastic conditionals are just conditionals

C&L's central claim: anankastics (eq. 1, the Harlem sentence) need no special compositional treatment, provided (i) want is given the effective-preference reading from § 5 (substrate at Semantics/Attitudes/Desire/Preferential.lean, Preferential.Want) and (ii) the conditional has the double-modal NEC[ψ][MODAL[φ]] LF from § 6. The Hoboken problem (§ 2.3, § 7.1.1) is then solved by consistency-driven vacuous truth: a hypothetical effective preference for Harlem is incompatible with the actual effective preference for Hoboken, so the NEC's modal-base restriction by the antecedent is empty — and the universal NEC is vacuously satisfied.

Scope

In:

• harlemLF — the § 7.1 eq. (87b)/(88) Harlem LF as a composition of existing substrate primitives.
• doubleModalLF — the § 6.1 eq. (77) double-modal schema (inline; not promoted to substrate per the ≥ 2-consumer graduation rule).
• HobokenScenario — minimal 2-world model + the § 7.1.1 headline theorem harlem_true_in_hoboken_scenario.

Out: § 3 review (see Studies/vonFintelIatridou2005.lean); § 4 full near-anankastic taxonomy; § 6.2 Sobel sequences; § 7.1.4 informational asymmetry; § 7.2.3 weak antecedents/consequents. Strong-vs-weak modal distinction is set aside per paper fn. 12.

TODO

A PreferenceStructure → Kratzer.OrderingSource bridge would let the inner MUST be evaluated non-trivially in scenarios where the antecedent restriction does not collapse to vacuous truth. The Hoboken theorem doesn't need it (vacuous truth wins), but a richer-information scenario or the § 7.2 near-anankastic family would. Substrate work, not paper-specific; tracked in Semantics/Attitudes/Preference.lean (maxInducedLe).

Cross-references

• Semantics/Attitudes/Desire/Preferential.lean — Preferential.Want; Semantics/Attitudes/Preference.lean — maxElts_pair_belief_compatible (the load-bearing lemma).
• Studies/vonFintelIatridou2005.lean — vF&I's primary-secondary ordering source analysis that C&L 2016 critiques (paper § 3.2.2).
• Studies/PhillipsBrown2025.lean § 11 — sibling no-go theorem condoravdiLauer_blocks_simultaneous_pq_and_negpq, same consistency-delegation pattern.

§ 6.1 Double-modal compositional schema (eq. 77)

def CondoravdiLauer2016.doubleModalLF {W : Type u} (fOuter : Modality.Kratzer.ModalBase W) (gOuter : Modality.Kratzer.OrderingSource W) (ψ innerModal : W → Prop) (w : W) : Prop

[CL16] eq. (77): If ψ, MODAL[φ] parses as NEC[ψ][MODAL[φ]] when the consequent contains an overt modal claim. Composed from conditionalNecessity (the outer NEC restriction by antecedent, from Semantics/Conditionals/Restrictor.lean) and an arbitrary world-indexed inner-modal proposition.

This is the schema instantiated by harlemLF. Kept inline rather than promoted to Semantics/Conditionals/DoubleModal.lean because no second paper-anchored study currently consumes it (≥ 2-consumer graduation rule). Kaufmann & Schwager 2009 on conditional imperatives would be the natural second consumer.

Equations

• CondoravdiLauer2016.doubleModalLF fOuter gOuter ψ innerModal w = Semantics.Conditionals.Restrictor.conditionalNecessity fOuter gOuter ψ innerModal w

§ 7.1 The Harlem LF (eq. 87b / 88)

def CondoravdiLauer2016.harlemLF {Agent W : Type u} (fBelS : Modality.Kratzer.ModalBase W) (gNorm : Modality.Kratzer.OrderingSource W) (P : Agent → W → PreferenceStructure W) (fHist : Modality.Kratzer.ModalBase W) (gInner : Modality.Kratzer.OrderingSource W) (Ad : Agent) (Harlem ATrain : Set W) (w : W) : Prop

[CL16] eq. (88) at the operator level: the Harlem-sentence LF parameterised over its four contextual backgrounds. NEC_{fBelS, gNorm}[Preferential.Want(Ad, Harlem)] [MUST_{fHist, gInner}[ATrain]].

The four contextual parameters:

• fBelS — modal base of NEC, "speaker's true beliefs" (paper p. 41).
• gNorm — ordering source of NEC, "stereotypical" (paper § 6.1).
• fHist — modal base of MUST, "historical alternatives at time t" (paper p. 42; the historical-alternatives substrate lives in Semantics/Modality/HistoricalAlternatives.lean, but the v1 LF here takes an arbitrary modal base because the Hoboken theorem doesn't constrain it).
• gInner — ordering source of MUST. Paper eq. (88) uses g_epA (= fun w => (P Ad w).maxElts), but the bridge from Set (Set W) to the List-valued OrderingSource is deferred (see TODO in the module docstring); v1 takes gInner as a parameter.

Equations

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

§ 7.1.1 Hoboken scenario — the headline theorem

A minimal two-world model: w₀ (actual, Ad effectively prefers Hoboken) and w₁ (hypothetical, Ad effectively prefers Harlem). The two destination propositions are disjoint, and Ad knows this (B = univ contains both worlds and Harlem ∩ Hoboken = ∅).

The headline (§ 7.1.1, p. 44): the Harlem sentence comes out true at w₀ despite Ad's actual preference for Hoboken — solving the conflicting-goals problem § 2.3 raised against Sæbø's analysis.

@[reducible, inline]

abbrev CondoravdiLauer2016.HobokenScenario.World : Type

Two-world model: w₀ (Hoboken-world) and w₁ (Harlem-world).

Equations

• CondoravdiLauer2016.HobokenScenario.World = Fin 2

@[reducible, inline]

abbrev CondoravdiLauer2016.HobokenScenario.wActual : World

The actual world (Hoboken scenario).

Equations

• CondoravdiLauer2016.HobokenScenario.wActual = 0

def CondoravdiLauer2016.HobokenScenario.Harlem : Set World

The destination propositions. Disjoint by construction (Harlem ∩ Hoboken = ∅) — Ad cannot go to both places in the same time frame, per paper p. 7 / eq. (90).

Equations

• CondoravdiLauer2016.HobokenScenario.Harlem = {1}

def CondoravdiLauer2016.HobokenScenario.Hoboken : Set World

Equations

• CondoravdiLauer2016.HobokenScenario.Hoboken = {0}

def CondoravdiLauer2016.HobokenScenario.belAd : Unit → World → Set World

Ad's belief state: full epistemic uncertainty (both worlds are belief-possible). B Ad w = Set.univ for both Ad ∈ Unit and w ∈ World.

Equations

• CondoravdiLauer2016.HobokenScenario.belAd x✝¹ x✝ = Set.univ

theorem CondoravdiLauer2016.HobokenScenario.harlem_inter_hoboken_eq_empty : Harlem ∩ Hoboken = ∅

The propositions are disjoint at the world level (eq. 90).

def CondoravdiLauer2016.HobokenScenario.prefBg : Unit → World → PreferenceStructure World

The preferential background: Hoboken-preferring at w₀, Harlem-preferring at w₁. Uses if-on-decidable equality to keep the reduction simple at the use sites.

Equations

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

theorem CondoravdiLauer2016.HobokenScenario.prefBg_consistent (u : Unit) (w : World) : (prefBg u w).consistent (belAd u w)

prefBg is Ad's effective preference function (C&L (68)): pointwise consistent with the belief state.

theorem CondoravdiLauer2016.HobokenScenario.hoboken_wanted_at_wActual : Desire.Preferential.Want prefBg () Hoboken wActual

At wActual = w₀: Ad effectively prefers Hoboken.

theorem CondoravdiLauer2016.HobokenScenario.harlem_not_wanted_at_wActual : ¬Desire.Preferential.Want prefBg () Harlem wActual

The crux: at wActual, Ad does NOT effectively prefer Harlem. Two maximal preferences of a consistent structure must meet inside the belief state (maxElts_pair_belief_compatible), but Hoboken ∩ Harlem = ∅.

def CondoravdiLauer2016.HobokenScenario.fBelS : Modality.Kratzer.ModalBase World

Speaker's modal base: knows the actual world. fBelS(w) = {w} is the simplest realization of "speaker's true beliefs" — the standard omniscient case where vacuous truth wins.

Equations

• CondoravdiLauer2016.HobokenScenario.fBelS w = [fun (x : CondoravdiLauer2016.HobokenScenario.World) => x = w]

def CondoravdiLauer2016.HobokenScenario.gNorm : Modality.Kratzer.OrderingSource World

Empty (stereotypical) ordering source — minimal choice; the Hoboken theorem doesn't depend on its content.

Equations

• CondoravdiLauer2016.HobokenScenario.gNorm = Modality.Kratzer.emptyBackground

def CondoravdiLauer2016.HobokenScenario.fHist : Modality.Kratzer.ModalBase World

Inner modal base (paper f^t_hist) — paper-local placeholder.

Equations

• CondoravdiLauer2016.HobokenScenario.fHist = Modality.Kratzer.emptyBackground

def CondoravdiLauer2016.HobokenScenario.gInner : Modality.Kratzer.OrderingSource World

Inner ordering source (paper g_epA) — paper-local placeholder. The Hoboken theorem's vacuous-truth doesn't constrain gInner; this is just a typed stub. See module docstring TODO on the bridge.

Equations

• CondoravdiLauer2016.HobokenScenario.gInner = Modality.Kratzer.emptyBackground

def CondoravdiLauer2016.HobokenScenario.ATrain : Set World

The A-train proposition (arbitrary; the Hoboken theorem doesn't constrain it).

Equations

• CondoravdiLauer2016.HobokenScenario.ATrain = Set.univ

theorem CondoravdiLauer2016.HobokenScenario.harlem_true_in_hoboken_scenario : harlemLF fBelS gNorm prefBg fHist gInner () Harlem ATrain wActual

Paper § 7.1.1 headline theorem (eq. 88 evaluated at the Hoboken scenario). The Harlem sentence is true at wActual — solving the conflicting-goals problem § 2.3 raised against Sæbø 2001.

Mechanism: the NEC's modal base is fBelS = [(· = wActual)], so accessibleWorlds fBelS wActual = {wActual}. Restricting by the antecedent Preferential.Want prefBg Ad Harlem removes wActual from the accessible set (by harlem_not_wanted_at_wActual, derived from the consistency of the background and Harlem ∩ Hoboken = ∅), leaving the empty set. The NEC quantifies over bestWorlds of that empty set, which is empty, so the NEC is vacuously true.

The inner MUST is never evaluated — consistency alone suffices. This is the formal core of C&L's claim that anankastics need no special compositional treatment.