@cite{condoravdi-lauer-2016} — 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 Theories/Semantics/Attitudes/CondoravdiLauer.lean) 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 Phenomena/Conditionals/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 Core/Order/PreferenceStructure/MaxInducedOrdering.lean:12-15.

Cross-references

• Theories/Semantics/Attitudes/CondoravdiLauer.lean — wantEP and wantEP_jointly_belief_consistent (the load-bearing lemma).
• Phenomena/Conditionals/Studies/vonFintelIatridou2005.lean — vF&I's primary-secondary ordering source analysis that C&L 2016 critiques (paper § 3.2.2).
• Phenomena/Modality/Studies/PhillipsBrown2025.lean § 11 — sibling no-go theorem condoravdiLauer_blocks_simultaneous_pq_and_negpq, same consistency-of-EP delegation pattern.

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.doubleModalLF {W : Type u} (fOuter : Core.Logic.Intensional.ModalBase W) (gOuter : Core.Logic.Intensional.OrderingSource W) (ψ innerModal : W → Prop) (w : W) : Prop

@cite{condoravdi-lauer-2016} 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 Theories/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 Theories/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

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

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.harlemLF {Agent W : Type u} (fBelS : Core.Logic.Intensional.ModalBase W) (gNorm : Core.Logic.Intensional.OrderingSource W) {B : Agent → W → Set W} (EP : Semantics.Attitudes.CondoravdiLauer.EffectivePreferentialBackground Agent W B) (fHist : Core.Logic.Intensional.ModalBase W) (gInner : Core.Logic.Intensional.OrderingSource W) (Ad : Agent) (Harlem ATrain : Set W) (w : W) : Prop

@cite{condoravdi-lauer-2016} eq. (88) at the operator level: the Harlem-sentence LF parameterised over its four contextual backgrounds. NEC_{fBelS, gNorm}[wantEP(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; historicalNecessity substrate exists at Theories/Semantics/Modality/Temporal.lean:119, 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 (= maxOrderingSource EP Ad), 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.

theorem Phenomena.Conditionals.Studies.CondoravdiLauer2016.harlemLF_eq_doubleModalLF {Agent W : Type u} (fBelS : Core.Logic.Intensional.ModalBase W) (gNorm : Core.Logic.Intensional.OrderingSource W) {B : Agent → W → Set W} (EP : Semantics.Attitudes.CondoravdiLauer.EffectivePreferentialBackground Agent W B) (fHist : Core.Logic.Intensional.ModalBase W) (gInner : Core.Logic.Intensional.OrderingSource W) (Ad : Agent) (Harlem ATrain : Set W) (w : W) : harlemLF fBelS gNorm EP fHist gInner Ad Harlem ATrain w = doubleModalLF fBelS gNorm (fun (w' : W) => Semantics.Attitudes.CondoravdiLauer.wantEP EP Ad Harlem w') (fun (w' : W) => Semantics.Modality.Kratzer.necessity fHist gInner (fun (x : W) => x ∈ ATrain) w') w

The Harlem LF instantiates the eq. (77) double-modal schema by construction. Documentation theorem (the equality is rfl).

§ 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 Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.World : Type

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

Equations

• Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.World = Fin 2

@[reducible, inline]

abbrev Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.wActual : World

The actual world (Hoboken scenario).

Equations

• Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.wActual = 0

def Phenomena.Conditionals.Studies.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

• Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.Harlem = {1}

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.Hoboken : Set World

Equations

• Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.Hoboken = {0}

def Phenomena.Conditionals.Studies.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

• Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.belAd x✝¹ x✝ = Set.univ

theorem Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.harlem_inter_hoboken_eq_empty : Harlem ∩ Hoboken = ∅

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

noncomputable def Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.epAtW0 : Core.Order.EffectivePreference World Set.univ

Effective preference at w₀: Ad effectively prefers Hoboken.

Equations

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

noncomputable def Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.epAtW1 : Core.Order.EffectivePreference World Set.univ

Effective preference at w₁: Ad effectively prefers Harlem.

Equations

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

noncomputable def Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.EP : Semantics.Attitudes.CondoravdiLauer.EffectivePreferentialBackground Unit World belAd

The effective preferential background: at w₀ Hoboken-preferring, at w₁ Harlem-preferring. 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 Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.wantEP_hoboken_at_wActual : Semantics.Attitudes.CondoravdiLauer.wantEP EP () Hoboken wActual

At wActual = w₀: Ad effectively prefers Hoboken.

theorem Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.not_wantEP_harlem_at_wActual : ¬Semantics.Attitudes.CondoravdiLauer.wantEP EP () Harlem wActual

The crux: at wActual, Ad does NOT effectively prefer Harlem. By wantEP_jointly_belief_consistent, if Ad effectively preferred both Hoboken and Harlem, then (Hoboken ∩ Harlem) ∩ B Ad wActual ≠ ∅. But Hoboken ∩ Harlem = ∅, contradiction.

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.fBelS : Core.Logic.Intensional.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

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.gNorm : Core.Logic.Intensional.OrderingSource World

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

Equations

• Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.gNorm = Core.Logic.Intensional.emptyBackground

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.fHist : Core.Logic.Intensional.ModalBase World

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

Equations

• Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.fHist = Core.Logic.Intensional.emptyBackground

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.gInner : Core.Logic.Intensional.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

• Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.gInner = Core.Logic.Intensional.emptyBackground

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.ATrain : Set World

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

Equations

• Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.ATrain = Set.univ

theorem Phenomena.Conditionals.Studies.CondoravdiLauer2016.HobokenScenario.harlem_true_in_hoboken_scenario : harlemLF fBelS gNorm EP 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 wantEP EP Ad Harlem removes wActual from the accessible set (by not_wantEP_harlem_at_wActual, derived from the consistency of EP 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 of EP alone suffices. This is the formal core of C&L's claim that anankastics need no special compositional treatment.

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_2_intend : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_3_plan : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_4_goal : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_5_chocolate : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_19_chess : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_20_chess_conditional : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_28_invite : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_29a_vaccine_safe : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_29b_vaccine : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_31_disneyworld : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_38_exemption : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_39a_disaster : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_40a_dress : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_46_neg_letter_grade : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_52_picnic_hiking : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_55_chess_incompat : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_61_concorde : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_63_poodle_dog : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_82a_dog_tax : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_92_vladivostok : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_91a_virus_no : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.cl2016_112a_inclined_harlem : Data.Examples.LinguisticExample

Equations

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

def Phenomena.Conditionals.Studies.CondoravdiLauer2016.Examples.all : List Data.Examples.LinguisticExample

Equations

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