von Fintel & Iatridou (2005): What to Do If You Want to Go to Harlem

This file formalizes [vFI05]'s analysis of anankastic conditionals, the Harlem sentence if you want to go to Harlem, you have to take the A train (1). Three analyses in [Kra91]'s framework fail. The obvious one, the if-clause restricting the modal base of a teleological have to ordered by the actual goals (11), founders on the Hoboken problem: when you actually want to go to Hoboken the best want-Harlem worlds take the PATH train, so the sentence is predicted false. [Sab01]'s analysis adds the hypothetical goal to the ordering source instead (14), and founders on conflicting goals: with Hoboken and Harlem inconsistent, the best worlds achieve either, so the sentence is again false (13). The nested analysis, a covert closeness modal restricted by the if-clause over the teleological one (15), (16), fails where the closest want-Harlem worlds keep the Hoboken goal (§5). The paper's proposal follows [Slo70]: a teleological modal takes a designated goal, which every world quantified over achieves, while the remaining goals are ancillary considerations that rank those worlds; have to quantifies over all goal-achieving accessible worlds and ought to over the best of them (24), so have to entails ought to and not conversely (haveTo, oughtTo). The designated goal overrides the actual goals, which dissolves the Hoboken and mayor problems (25), (26) and predicts the have to and ought to verdicts of Huitink's van Nistelrooy scenario (27). Necessary conditions come out trivially true under have to (34), and [Nis05]'s to go to Harlem, you ought to kiss Pedro Martinez (36) comes out true, against which the paper conjectures that the prejacent must be an essential part of a way of achieving the goal (42), IsEssentialPart.

Implementation notes

The obvious analysis is Conditional.Restrictor.conditionalNecessity, and the designated-goal modals are Kratzer necessity over the base restricted to the goal, with the ancillary ordering source for ought to and the empty one for have to. The scenarios are finite world types with the relevant propositions as predicates and the refutations decided. The condition (42) quantifies over arbitrary propositions, and so holds of any prejacent as soon as some accessible world lacks both the prejacent and the goal (isEssentialPart_of_exists); the paper leaves the status of the condition open. The paper's examples are the rows of Data.Examples.VonFintelIatridou2005.

References

• [vFI05]
• [Kra91]
• [Sab01]
• [Slo70]
• [Nis05]

The obvious analysis and the Hoboken problem (§3)

inductive VonFintelIatridou2005.Hoboken : Type

In the Hoboken scenario you take the A train or the PATH train, and hypothetically want to go to Harlem or not; the A train reaches Harlem, the PATH train Hoboken.

• wantA : Hoboken

  Wants Harlem, takes the A train.

• wantPath : Hoboken

  Wants Harlem, takes the PATH train.

• otherA : Hoboken

  Does not want Harlem, takes the A train.

• otherPath : Hoboken

  Does not want Harlem, takes the PATH train.

@[instance_reducible]

instance VonFintelIatridou2005.instDecidableEqHoboken : DecidableEq Hoboken

Equations

• VonFintelIatridou2005.instDecidableEqHoboken x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VonFintelIatridou2005.instFintypeHoboken : Fintype Hoboken

Equations

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

@[reducible, inline]

abbrev VonFintelIatridou2005.Hoboken.wantHarlem : Hoboken → Prop

Equations

• w.wantHarlem = (w = VonFintelIatridou2005.Hoboken.wantA ∨ w = VonFintelIatridou2005.Hoboken.wantPath)

@[reducible, inline]

abbrev VonFintelIatridou2005.Hoboken.takeA : Hoboken → Prop

Equations

• w.takeA = (w = VonFintelIatridou2005.Hoboken.wantA ∨ w = VonFintelIatridou2005.Hoboken.otherA)

@[reducible, inline]

abbrev VonFintelIatridou2005.Hoboken.goHoboken : Hoboken → Prop

Equations

• w.goHoboken = (w = VonFintelIatridou2005.Hoboken.wantPath ∨ w = VonFintelIatridou2005.Hoboken.otherPath)

@[reducible, inline]

abbrev VonFintelIatridou2005.Hoboken.goHarlem : Hoboken → Prop

Equations

• VonFintelIatridou2005.Hoboken.goHarlem = VonFintelIatridou2005.Hoboken.takeA

@[reducible, inline]

abbrev VonFintelIatridou2005.Hoboken.goals : Modality.Background Hoboken

The actual goal in every world is to go to Hoboken.

Equations

• x✝.goals = {VonFintelIatridou2005.Hoboken.goHoboken}

theorem VonFintelIatridou2005.Hoboken.not_obvious : ¬Conditional.Restrictor.conditionalNecessity ⊥ goals wantHarlem takeA wantA

On (11), the obvious analysis, the if-clause restricting the circumstantial base of a modal ordered by the actual goals, makes the Harlem sentence false, since the best want-Harlem world takes the PATH train.

Sæbø's analysis and conflicting goals (§4)

inductive VonFintelIatridou2005.Conflict : Type

The conflicting-goals scenario (13): this afternoon you take the A train to Harlem or the PATH train to Hoboken, not both.

• aTrain : Conflict
• pathTrain : Conflict

@[instance_reducible]

instance VonFintelIatridou2005.instDecidableEqConflict : DecidableEq Conflict

Equations

• VonFintelIatridou2005.instDecidableEqConflict x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VonFintelIatridou2005.instFintypeConflict : Fintype Conflict

Equations

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

@[reducible, inline]

abbrev VonFintelIatridou2005.Conflict.takeA : Conflict → Prop

Equations

• x✝.takeA = (x✝ = VonFintelIatridou2005.Conflict.aTrain)

@[reducible, inline]

abbrev VonFintelIatridou2005.Conflict.goHarlem : Conflict → Prop

Equations

• VonFintelIatridou2005.Conflict.goHarlem = VonFintelIatridou2005.Conflict.takeA

@[reducible, inline]

abbrev VonFintelIatridou2005.Conflict.goHoboken : Conflict → Prop

Equations

• x✝.goHoboken = (x✝ = VonFintelIatridou2005.Conflict.pathTrain)

@[reducible, inline]

abbrev VonFintelIatridou2005.Conflict.saebo : Modality.Background Conflict

Sæbø's ordering source (14) is the actual goal of going to Hoboken with the hypothetical goal of going to Harlem added.

Equations

• x✝.saebo = {VonFintelIatridou2005.Conflict.goHoboken, VonFintelIatridou2005.Conflict.goHarlem}

theorem VonFintelIatridou2005.Conflict.not_saebo : ¬Modality.necessity ⊥ saebo takeA aTrain

Sæbø's analysis makes the Harlem sentence false, since with the two goals inconsistent the best worlds achieve either, and not all take the A train.

Nested modality (§5)

inductive VonFintelIatridou2005.Nested : Type

In the scenario of §5 the closest world in which you want to go to Harlem is one in which you still want to go to Hoboken as well.

• actual : Nested

  The actual world: wants Hoboken, takes the PATH train.

• bothPath : Nested

  Wants both, takes the PATH train.

• bothA : Nested

  Wants both, takes the A train.

@[instance_reducible]

instance VonFintelIatridou2005.instDecidableEqNested : DecidableEq Nested

Equations

• VonFintelIatridou2005.instDecidableEqNested x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VonFintelIatridou2005.instFintypeNested : Fintype Nested

Equations

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

@[reducible, inline]

abbrev VonFintelIatridou2005.Nested.wantHarlem : Nested → Prop

Equations

• w.wantHarlem = (w = VonFintelIatridou2005.Nested.bothPath ∨ w = VonFintelIatridou2005.Nested.bothA)

@[reducible, inline]

abbrev VonFintelIatridou2005.Nested.takeA : Nested → Prop

Equations

• x✝.takeA = (x✝ = VonFintelIatridou2005.Nested.bothA)

@[reducible, inline]

abbrev VonFintelIatridou2005.Nested.goHoboken : Nested → Prop

Equations

• w.goHoboken = (w = VonFintelIatridou2005.Nested.actual ∨ w = VonFintelIatridou2005.Nested.bothPath)

@[reducible, inline]

abbrev VonFintelIatridou2005.Nested.goHarlem : Nested → Prop

Equations

• VonFintelIatridou2005.Nested.goHarlem = VonFintelIatridou2005.Nested.takeA

def VonFintelIatridou2005.Nested.goals : Modality.Background Nested

The goals of each world are Hoboken in the actual world and both in the others.

Equations

• VonFintelIatridou2005.Nested.actual.goals = {VonFintelIatridou2005.Nested.goHoboken}
• x✝.goals = {VonFintelIatridou2005.Nested.goHoboken, VonFintelIatridou2005.Nested.goHarlem}

@[reducible, inline]

abbrev VonFintelIatridou2005.Nested.closeness : Modality.Background Nested

The closeness ordering of the higher modal is agreement with the actual world on wanting Hoboken.

Equations

• x✝.closeness = {VonFintelIatridou2005.Nested.goHoboken}

theorem VonFintelIatridou2005.Nested.not_nested : ¬Conditional.Restrictor.conditionalNecessity ⊥ closeness wantHarlem (fun (w' : Nested) => Modality.necessity ⊥ goals takeA w') actual

On (16), the nested analysis, a closeness modal restricted by the if-clause over the teleological modal, makes the Harlem sentence false, since in the closest want-Harlem world the Hoboken goal survives and the PATH train is among the best worlds.

Designated goals (§6)

def VonFintelIatridou2005.haveTo {W : Type u_1} (f : Modality.Background W) (p q : W → Prop) (w : W) : Prop

To p, have to q (24b) holds when every accessible world achieving the designated goal p is a q-world.

Equations

• VonFintelIatridou2005.haveTo f p q w = Conditional.Restrictor.conditionalNecessity f ⊥ p q w

def VonFintelIatridou2005.oughtTo {W : Type u_1} (f g : Modality.Background W) (p q : W → Prop) (w : W) : Prop

To p, ought to q (24a) holds when every accessible world achieving the designated goal p that is best by the ancillary considerations g is a q-world.

Equations

• VonFintelIatridou2005.oughtTo f g p q w = Conditional.Restrictor.conditionalNecessity f g p q w

theorem VonFintelIatridou2005.haveTo_iff {W : Type u_1} {f : Modality.Background W} {p q : W → Prop} {w : W} : haveTo f p q w ↔ ∀ v ∈ f.accessibleWorlds w, p v → q v

theorem VonFintelIatridou2005.oughtTo_of_haveTo {W : Type u_1} {f g : Modality.Background W} {p q : W → Prop} {w : W} (h : haveTo f p q w) : oughtTo f g p q w

Sloman's insight is that have to entails ought to whatever the ancillary considerations.

theorem VonFintelIatridou2005.haveTo_of_imp {W : Type u_1} {f : Modality.Background W} {p q : W → Prop} {w : W} (h : ∀ (v : W), p v → q v) : haveTo f p q w

A necessary condition of the goal is trivially something you have to do (34).

theorem VonFintelIatridou2005.exists_oughtTo_not_haveTo : oughtTo ⊥ (fun (x : Bool) => {fun (x : Bool) => x = true}) (fun (x : Bool) => True) (fun (x : Bool) => x = true) true ∧ ¬haveTo ⊥ (fun (x : Bool) => True) (fun (x : Bool) => x = true) true

In Sloman's London example (23) the train is the best means without being the only one, so you ought to take the train, but you don't have to. World true goes by train, false by bus; both arrive by noon, and only the train is comfortable.

theorem VonFintelIatridou2005.Hoboken.haveTo_takeA : haveTo ⊥ goHarlem takeA wantA

By (25), with going to Harlem the designated goal the Hoboken problem does not arise; you have to take the A train whatever your actual goals.

inductive VonFintelIatridou2005.Ruud : Type

In Huitink's van Nistelrooy scenario (27) both the A and the C train reach Harlem, and Ruud rides the A train.

• aTrain : Ruud
• cTrain : Ruud

@[instance_reducible]

instance VonFintelIatridou2005.instDecidableEqRuud : DecidableEq Ruud

Equations

• VonFintelIatridou2005.instDecidableEqRuud x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VonFintelIatridou2005.instFintypeRuud : Fintype Ruud

Equations

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

@[reducible, inline]

abbrev VonFintelIatridou2005.Ruud.takeA : Ruud → Prop

Equations

• x✝.takeA = (x✝ = VonFintelIatridou2005.Ruud.aTrain)

@[reducible, inline]

abbrev VonFintelIatridou2005.Ruud.meetRuud : Ruud → Prop

Equations

• VonFintelIatridou2005.Ruud.meetRuud = VonFintelIatridou2005.Ruud.takeA

theorem VonFintelIatridou2005.Ruud.not_haveTo_and_oughtTo : ¬haveTo ⊥ (fun (x : Ruud) => True) takeA aTrain ∧ oughtTo ⊥ (fun (x : Ruud) => {meetRuud}) (fun (x : Ruud) => True) takeA aTrain

You do not have to take the A train, but given that you want to meet Ruud you ought to.

Kissing Pedro Martinez (§7.2)

inductive VonFintelIatridou2005.Pedro : Type

In Nissenbaum's scenario (36) the A and the C train reach Harlem, Pedro Martinez rides the C train, and you want to kiss him.

• aTrain : Pedro
• cTrainKiss : Pedro
• home : Pedro

@[instance_reducible]

instance VonFintelIatridou2005.instDecidableEqPedro : DecidableEq Pedro

Equations

• VonFintelIatridou2005.instDecidableEqPedro x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VonFintelIatridou2005.instFintypePedro : Fintype Pedro

Equations

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

@[reducible, inline]

abbrev VonFintelIatridou2005.Pedro.goHarlem : Pedro → Prop

Equations

• w.goHarlem = (w = VonFintelIatridou2005.Pedro.aTrain ∨ w = VonFintelIatridou2005.Pedro.cTrainKiss)

@[reducible, inline]

abbrev VonFintelIatridou2005.Pedro.kissPedro : Pedro → Prop

Equations

• x✝.kissPedro = (x✝ = VonFintelIatridou2005.Pedro.cTrainKiss)

theorem VonFintelIatridou2005.Pedro.oughtTo_kissPedro : oughtTo ⊥ (fun (x : Pedro) => {kissPedro}) goHarlem kissPedro aTrain

The designated-goal semantics predicts to go to Harlem, you ought to kiss Pedro Martinez true, contrary to fact.

def VonFintelIatridou2005.IsEssentialPart {W : Type u_1} (f : Modality.Background W) (p q : W → Prop) (w : W) : Prop

By (42), q is an essential part of a way of achieving p when some premises together with q entail p over the modal base while without q they do not.

Equations

• VonFintelIatridou2005.IsEssentialPart f p q w = ∃ (P : Set (W → Prop)), sInf (insert q (f w ∪ P)) ≤ p ∧ ¬sInf (f w ∪ P) ≤ p

theorem VonFintelIatridou2005.isEssentialPart_of_exists {W : Type u_1} {f : Modality.Background W} {p q : W → Prop} {w : W} (h : ∃ v ∈ f.accessibleWorlds w, ¬q v ∧ ¬p v) : IsEssentialPart f p q w

Over arbitrary premises the condition (42) is undiscriminating, since any prejacent is an essential part as soon as some accessible world lacks both the prejacent and the goal, the premise that either the goal holds or the prejacent fails doing the work.

theorem VonFintelIatridou2005.Pedro.isEssentialPart_kissPedro : IsEssentialPart ⊥ goHarlem kissPedro aTrain

In Nissenbaum's scenario, staying home neither kisses Pedro nor reaches Harlem, so kissing Pedro counts as essential by (42).