Documentation

Linglib.Studies.VonFintelIatridou2005

[vFI05] — Anankastic conditionals and related matters #

The "Harlem Sentence" — If you want to go to Harlem, you have to take the A train — and the puzzle: no straightforward Kratzerian analysis delivers its truth conditions. vF&I rule out three candidate analyses (if-clause restricts the modal base, modifies the ordering source à la [Sab01], or is restricted by a covert higher modal), then propose a Designated Goals account paired with [Slo70]'s have-to-vs-ought-to distinction.

This file contains:

Example data lives in Linglib/Data/Examples/vonFintelIatridou2005.json and is generated into the Examples section below by scripts/gen_examples.py vonFintelIatridou2005.

Analytical predicates #

Each candidate analysis is a predicate parameterized by the relevant propositions on a world type. Concrete vF&I scenarios (Hoboken, Conflicting Goals) instantiate these arguments with their own predicates and decide discharges the refutation. Bundling the propositions into a Scenario structure would hide the per-predicate decidability the refutations need behind a field projection; the explicit-argument form keeps each refutation mechanically verifiable. The circumstantial modal base is taken as universal (the worked vF&I scenarios do not exploit modal-base restriction).

Obvious analysis and the Hoboken Problem #

vF&I eq. (9): [have to](w)(f)(g)(q) = 1 iff ∀w' ∈ max_{g(w)}(∩f(w)) : q(w') = 1. vF&I eq. (10): [if φ](f) = λw. f(w) ∪ {⟦φ⟧}.

Combined, the "obvious analysis" of the Harlem Sentence asserts: in the best (per actual goals) worlds where you want to go to Harlem, you take the A train. In the Hoboken scenario the actual ordering source ranks worlds by satisfaction of want-Hoboken. Best want-Harlem worlds are then those that simultaneously achieve Hoboken — i.e., take the PATH train — so the obvious analysis predicts the sentence false (vF&I p. 5 intuition: true).

source
def VonFintelIatridou2005.obviousAnalysis {W : Type u_1} (wantHyp achieveAct candidate : W → Prop) :
Prop

The obvious analysis: the candidate is true at every want-Harlem world that maximizes actual-goal-achievement.

Equations
Instances For

    The Hoboken scenario. Four worlds: w0: A train, achieves Harlem; w1: PATH, achieves Hoboken; w2: PATH, achieves both Hoboken AND want-Harlem holds — the counterexample world; w3: A train, achieves Harlem.

    source
    @[reducible, inline]
    abbrev VonFintelIatridou2005.HobokenScenario.World :
    Type
    Equations
    Instances For
      source
      def VonFintelIatridou2005.HobokenScenario.wantHypothetical :
      World → Prop
      Equations
      Instances For
        source
        @[implicit_reducible]
        instance VonFintelIatridou2005.HobokenScenario.instDecidablePredWorldWantHypothetical :
        DecidablePred wantHypothetical
        Equations
        source
        def VonFintelIatridou2005.HobokenScenario.achieveActual :
        World → Prop
        Equations
        Instances For
          source
          @[implicit_reducible]
          instance VonFintelIatridou2005.HobokenScenario.instDecidablePredWorldAchieveActual :
          DecidablePred achieveActual
          Equations
          source
          def VonFintelIatridou2005.HobokenScenario.takeCandidate :
          World → Prop
          Equations
          Instances For
            source
            @[implicit_reducible]
            instance VonFintelIatridou2005.HobokenScenario.instDecidablePredWorldTakeCandidate :
            DecidablePred takeCandidate
            Equations
            source
            theorem VonFintelIatridou2005.hoboken_refutes_obvious :
            ¬obviousAnalysis HobokenScenario.wantHypothetical HobokenScenario.achieveActual HobokenScenario.takeCandidate

            The Hoboken scenario falsifies the obvious analysis: at w2 the candidate (A train) is false.

            Sæbø 2001's analysis and the Conflicting Goals refutation #

            [Sab01] adds the if-clause's proposition to the ordering source rather than the modal base: g⁺(w) := g(w) ∪ {⟦want-Harlem⟧}. The modal quantifies over best worlds in the modal base under g⁺. This survives the basic Hoboken setup but is non-compositional (want has to be zapped) and fails on Conflicting Goals scenarios (vF&I (13), (22)) where actual and hypothetical goals are jointly satisfiable yet conflicting in the concrete instance.

            source
            def VonFintelIatridou2005.saeboAnalysis {W : Type u_1} (achieveAct achieveHyp candidate : W → Prop) :
            Prop

            Sæbø's analysis: quantifies over worlds maximizing actual goal ∧ hypothetical goal jointly.

            Equations
            • VonFintelIatridou2005.saeboAnalysis achieveAct achieveHyp candidate = ∀ (w : W), (∀ (w' : W), achieveAct w' ∧ achieveHyp w' → achieveAct w ∧ achieveHyp w) → candidate w
            Instances For

              The Conflicting Goals scenario (vF&I (13)/(22)). Five worlds: w0: A, Harlem-only; w1: PATH, Hoboken-only; w2: A, both; w3: PATH, both — the counterexample world; w4: neither, neither.

              source
              @[reducible, inline]
              abbrev VonFintelIatridou2005.ConflictingGoalsScenario.World :
              Type
              Equations
              Instances For
                source
                def VonFintelIatridou2005.ConflictingGoalsScenario.achieveHypothetical :
                World → Prop
                Equations
                Instances For
                  source
                  @[implicit_reducible]
                  instance VonFintelIatridou2005.ConflictingGoalsScenario.instDecidablePredWorldAchieveHypothetical :
                  DecidablePred achieveHypothetical
                  Equations
                  source
                  def VonFintelIatridou2005.ConflictingGoalsScenario.achieveActual :
                  World → Prop
                  Equations
                  Instances For
                    source
                    @[implicit_reducible]
                    instance VonFintelIatridou2005.ConflictingGoalsScenario.instDecidablePredWorldAchieveActual :
                    DecidablePred achieveActual
                    Equations
                    source
                    def VonFintelIatridou2005.ConflictingGoalsScenario.takeCandidate :
                    World → Prop
                    Equations
                    Instances For
                      source
                      @[implicit_reducible]
                      instance VonFintelIatridou2005.ConflictingGoalsScenario.instDecidablePredWorldTakeCandidate :
                      DecidablePred takeCandidate
                      Equations
                      source
                      theorem VonFintelIatridou2005.conflictingGoals_refutes_saebo :
                      ¬saeboAnalysis ConflictingGoalsScenario.achieveActual ConflictingGoalsScenario.achieveHypothetical ConflictingGoalsScenario.takeCandidate

                      The Conflicting Goals scenario falsifies Sæbø's analysis: at w3 both goals are jointly achieved but the candidate (A train) is false.

                      Nested Modality #

                      vF&I §5 propose that the if-clause restricts an additional covert necessity modal scoping over the teleological modal: [ NEC if you want to go to Harlem ] [ have-to (you take the A train) ]. This survives the Hoboken Problem but fails on the Conflicting Goals scenario and on Huitink's van Nistelrooy (correlated-irrelevant). The shared failure motivates the Designated Goals move below. Not formalised here.

                      The Designated Goals proposal #

                      source
                      structure VonFintelIatridou2005.DesignatedGoal (W : Type u_1) :
                      Type u_1

                      [vFI05] §6 parameter for a teleological modal: a designated goal supplied by the to/if-clause, ancillary considerations ranking goal-achieving worlds, and a circumstantial modal base.

                      Instances For
                        source
                        def VonFintelIatridou2005.oughtTo {W : Type u_1} (dg : DesignatedGoal W) (q : W → Prop) (w : W) :
                        Prop

                        vF&I (24a): to p, ought-to q — q at every ancillary-best goal-achieving world.

                        Equations
                        Instances For
                          source
                          def VonFintelIatridou2005.haveTo {W : Type u_1} (dg : DesignatedGoal W) (q : W → Prop) (w : W) :
                          Prop

                          vF&I (24b): to p, have-to q — q at every goal-achieving world in the modal base. The exhaustification (no ranking) is the formal counterpart of [Slo70]'s "only candidate".

                          Equations
                          Instances For
                            source
                            theorem VonFintelIatridou2005.haveTo_implies_oughtTo_of_best_subset_accessible {W : Type u_1} (dg : DesignatedGoal W) (q : W → Prop) (w : W) (hHave : haveTo dg q w) (hBestSubset : ∀ w' ∈ Semantics.Modality.Kratzer.bestWorlds dg.modalBase (fun (v : W) => dg.ancillary v ++ [dg.goal]) w, w' ∈ Semantics.Modality.Kratzer.accessibleWorlds dg.modalBase w ∧ dg.goal w') :
                            oughtTo dg q w

                            [Slo70] / vF&I §6: have-to entails ought-to, under the structural assumption that every ancillary-best world is accessible and goal-achieving.

                            Cross-reference to [CM23] #

                            C&M's mustCM operator (Studies/ChungMascarenhas2024.lean) realises [Slo70]'s "only candidate" condition as an exhaustification clause on expected values: mustCM φ iff E[μ_R ∣ φ] > θ ∧ ∀ψ ∈ Alt(φ). E[μ_R ∣ ψ] ≤ θ. The first conjunct is strong permissibility (φ achieves the goal well enough); the second is the only-candidate condition. Under deontic/teleological R = R_D, this directly maps to vF&I's have-to: φ has to be the unique good-enough way of achieving the designated goal.

                            Handled cleanly by C&M:

                            Not dissolved by C&M: