Boneh and Doron 2013: Hab and Gen in the expression of habituality

Boneh and Doron argue that habituality involves two covert operators. Gen is the familiar modalized universal. Hab is a modalized existential over sums of events: an iteration in every world of a gnomic modal base, with only an initiating event that indicates a disposition in the actual world. The English auxiliaries mark neither; would marks mood, a special case of Gen, and used to is the imperfective under a retrospective aspect, which places the reference interval before the perspective interval. The operators are built on Link's sum closure, Kratzer's modal base, Klein's imperfective and Pancheva's final-subinterval perfect (Aspect.perfect); Del Prete's Italian Same-Object Effect is the configuration of same_object_infelicity.

Main statements

• same_object_infelicity: an indefinite scoping over Hab makes an unrepeatable event recur.
• gen_admits_fresh_objects: Gen's universal lets the object vary.
• hab_without_actual_iteration: Hab holds with a single actual initiating event.
• retro_perfect_forces_point: the retrospective and the perfect share a reference interval only at a degenerate perspective.
• usedTo_of_persisting_state: used to does not bound the state.

References

• [BD13]
• [Lin83]
• [Kra81b]
• [Kle94]
• [KR93]
• [Pan03]
• [DP13]

Hab against Gen ((4)–(8), (13)–(15))

Gen needs an explicit restrictor; without one only Hab applies, and an indefinite can only scope over it, as in (8) ∃x [cigarette(x) ∧ Hab e smoke(e, Mary, x)]. The contrast between (4a) and (4b) is then a theorem: smoking is unrepeatable per cigarette, so the wide-scope form is contradictory while Gen's (5a) is satisfiable with a fresh cigarette per event.

Iteration, (14), a sum of P-events with at least two distinct proper P-parts on Link's closure, is Mereology.IsPlural.

theorem BonehDoron2013.same_object_infelicity {E : Type u_1} {C : Type u_2} [SemilatticeSup E] {smoke : E → C → Prop} {cig : C → Prop} (hOnce : ∀ (c : C) (e₁ e₂ : E), smoke e₁ c → smoke e₂ c → e₁ = e₂) : ¬∃ (c : C), cig c ∧ ∃ (e : E), Mereology.IsPlural (fun (x : E) => smoke x c) e

With the indefinite scoping over Hab, the same object recurs through the iteration, so the reading is contradictory when the predicate is unrepeatable per object, one smoking per cigarette, (4b), (8).

def BonehDoron2013.gen {W : Type u_1} {Z : Type u_2} {T : Type u_3} (P Q : Z → W → Prop) (τ : Z → Set T) (mb : Set T → Modality.Background W) (i : Set T) (w : W) : Prop

Gen holds at the interval i and world w when every Q-individual temporally included in i is a P-individual throughout the gnomic modal base of i at w, (21). It is GEN with every case normal and its modality in the matrix.

Equations

• BonehDoron2013.gen P Q τ mb i w = ((i, w) ∈ ⊤.gen {z : Z | τ z ⊆ i ∧ Q z w} {z : Z | Modality.simpleNecessity (mb i) (P z) w})

theorem BonehDoron2013.gen_admits_fresh_objects : ∃ (smoke : Bool → Bool → Prop), (∀ (c e₁ e₂ : Bool), smoke e₁ c → smoke e₂ c → e₁ = e₂) ∧ gen (fun (e : Bool) (x : Unit) => ∃ (c : Bool), smoke e c) (fun (x : Bool) (x_1 : Unit) => True) (fun (x : Bool) => ∅) (fun (x : Set Unit) => ⊥) Set.univ ()

Gen's universal lets the indefinite scope below it, so the unrepeatability premise is satisfiable with a fresh cigarette per event, (4a), (5a).

def BonehDoron2013.hab {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (P : E → W → Prop) (mb : Modality.Background W) (indicatesDisposition : W → Prop) (w : W) : Prop

Hab holds when an initiating event that indicates a disposition occurs in the actual world and an iteration occurs in every accessible world of the gnomic modal base, (13), (15). The paper leaves "indicating a disposition" unanalyzed, so it is a parameter, and the temporal anchoring τ(s) ⊆ τ(e) is dropped with the event times.

Equations

• BonehDoron2013.hab P mb indicatesDisposition w = (indicatesDisposition w ∧ ∀ w' ∈ mb.accessibleWorlds w, ∃ (e : E), Mereology.IsPlural (fun (x : E) => P x w') e)

theorem BonehDoron2013.hab_without_actual_iteration : ∃ (P : Finset ℕ → Bool → Prop) (mb : Modality.Background Bool), hab P mb (fun (x : Bool) => x = false) false ∧ ¬∃ (e : Finset ℕ), Mereology.IsPlural (fun (x : Finset ℕ) => P x false) e

Hab is dispositional, holding on a single actual initiating event with the iteration only in the accessible worlds, (16)–(17), (42a–b).

used to: the imperfective under a retrospective ((18)–(19), (30)–(35))

The auxiliary is the retrospective over the imperfective. The imperfective (19a) is Klein's, IMPF, and the retrospective (19b) places the reference interval before the perspective interval, Kamp and Reyle's P, so used to is imperfective and retrospective by construction.

def BonehDoron2013.retro {W : Type u_1} {T : Type u_2} [LinearOrder T] (A : W → Set (NonemptyInterval T)) : W → Set (NonemptyInterval T)

The retrospective holds at a perspective interval when some reference interval satisfying the description lies wholly before it, (19b).

Equations

• BonehDoron2013.retro A w = {p : NonemptyInterval T | ∃ i ∈ A w, i.IsBefore p}

def BonehDoron2013.usedToOp {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) : W → Set (NonemptyInterval T)

Used to is the retrospective over the imperfective, (18).

Equations

• BonehDoron2013.usedToOp P = BonehDoron2013.retro (Aspect.IMPF P)

theorem BonehDoron2013.retro_perfect_forces_point {T : Type u_1} [LinearOrder T] {i p : NonemptyInterval T} (hb : i.IsBefore p) (hf : p.FinalSubinterval i) : p.IsPoint

One reference interval serves the retrospective and the perfect at once only for an instantaneous perspective, (32)–(34). The two form the Horn scale behind the retrospectivity implicature (31)–(33).

theorem BonehDoron2013.usedTo_of_persisting_state {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {e : E} (hP : P w e) {i p : NonemptyInterval T} (hie : i < Event.τ e) (hip : i.IsBefore p) : p ∈ usedToOp P w

Retrospectivity of the state is cancellable, as in … used to go to. Still do. (30), since the imperfective (19a) bounds only the reference interval, so a state whose run time properly contains a reference interval before the perspective satisfies used to however far it runs.

The three forms and Table (41)

inductive BonehDoron2013.HabitualForm : Type

A HabitualForm is one of the English past-habituality forms of (1).

• simpleForm : HabitualForm
• usedTo : HabitualForm
• would : HabitualForm

@[instance_reducible]

instance BonehDoron2013.instDecidableEqHabitualForm : DecidableEq HabitualForm

Equations

• BonehDoron2013.instDecidableEqHabitualForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BonehDoron2013.instReprHabitualForm.repr : HabitualForm → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BonehDoron2013.instReprHabitualForm : Repr HabitualForm

Equations

• BonehDoron2013.instReprHabitualForm = { reprPrec := BonehDoron2013.instReprHabitualForm.repr }

inductive BonehDoron2013.PerspectiveType : Type

A perspective is internal or retrospective, the second dimension of Table (41).

• internal : PerspectiveType
• retrospective : PerspectiveType

@[instance_reducible]

instance BonehDoron2013.instDecidableEqPerspectiveType : DecidableEq PerspectiveType

Equations

• BonehDoron2013.instDecidableEqPerspectiveType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BonehDoron2013.instReprPerspectiveType : Repr PerspectiveType

Equations

• BonehDoron2013.instReprPerspectiveType = { reprPrec := BonehDoron2013.instReprPerspectiveType.repr }

def BonehDoron2013.instReprPerspectiveType.repr : PerspectiveType → ℕ → Std.Format

Equations

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

def BonehDoron2013.admitsViewpoint : HabitualForm → Aspect.Perfectivity → Prop

admitsViewpoint f v says that the form f admits the viewpoint v, the viewpoint column of Table (41). The simple form takes either viewpoint, (26)–(27), and the periphrastic forms only the imperfective.

Equations

• BonehDoron2013.admitsViewpoint BonehDoron2013.HabitualForm.simpleForm x✝ = True
• BonehDoron2013.admitsViewpoint x✝ Aspect.Perfectivity.imperfective = True
• BonehDoron2013.admitsViewpoint x✝ Aspect.Perfectivity.perfective = False

def BonehDoron2013.admitsPerspective : HabitualForm → PerspectiveType → Prop

admitsPerspective f p says that the form f admits the perspective p, the perspective column of Table (41). Used to is retrospective, would internal and the simple form either, (35)–(40).

Equations

• BonehDoron2013.admitsPerspective BonehDoron2013.HabitualForm.simpleForm x✝ = True
• BonehDoron2013.admitsPerspective BonehDoron2013.HabitualForm.usedTo BonehDoron2013.PerspectiveType.retrospective = True
• BonehDoron2013.admitsPerspective BonehDoron2013.HabitualForm.usedTo BonehDoron2013.PerspectiveType.internal = False
• BonehDoron2013.admitsPerspective BonehDoron2013.HabitualForm.would BonehDoron2013.PerspectiveType.internal = True
• BonehDoron2013.admitsPerspective BonehDoron2013.HabitualForm.would BonehDoron2013.PerspectiveType.retrospective = False

The chapter's judgments

structure BonehDoron2013.EnglishDatum : Type

An EnglishDatum records an English judgment from the chapter.

• sentence : String
• form : HabitualForm
• felicitous : Bool
• exNumber : String

def BonehDoron2013.instReprEnglishDatum.repr : EnglishDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BonehDoron2013.instReprEnglishDatum : Repr EnglishDatum

Equations

• BonehDoron2013.instReprEnglishDatum = { reprPrec := BonehDoron2013.instReprEnglishDatum.repr }

def BonehDoron2013.maryCigaretteAfterDinner : EnglishDatum

Mary smokes a cigarette after dinner, (4a), is felicitous, since after dinner supplies Gen's restrictor and the indefinite scopes below it, as in (5a).

Equations

• BonehDoron2013.maryCigaretteAfterDinner = { sentence := "Mary smokes a cigarette after dinner", form := BonehDoron2013.HabitualForm.simpleForm, felicitous := true, exNumber := "(4a)" }

def BonehDoron2013.maryCigarette : EnglishDatum

Mary smokes a cigarette, (4b), is infelicitous, since with no explicit restrictor only Hab applies and the indefinite scopes over it, (8).

Equations

• BonehDoron2013.maryCigarette = { sentence := "#Mary smokes a cigarette", form := BonehDoron2013.HabitualForm.simpleForm, felicitous := false, exNumber := "(4b)" }

def BonehDoron2013.flowerGrows : EnglishDatum

A flower grows out behind the old shed, (6b), survives on its plausible same-object reading, one flower growing out repeatedly.

Equations

• BonehDoron2013.flowerGrows = { sentence := "A flower grows out behind the old shed", form := BonehDoron2013.HabitualForm.simpleForm, felicitous := true, exNumber := "(6b)" }

def BonehDoron2013.maxKilledRabbit : EnglishDatum

Max killed a rabbit repeatedly, (7b), is infelicitous, since the indefinite scopes over the adverbial's quantifier and the same rabbit would be killed repeatedly.

Equations

• BonehDoron2013.maxKilledRabbit = { sentence := "#Max killed a rabbit repeatedly", form := BonehDoron2013.HabitualForm.simpleForm, felicitous := false, exNumber := "(7b)" }

def BonehDoron2013.wouldDressNoContext : EnglishDatum

In the good old days, people would dress elegantly, (2c), is infelicitous, since would requires its restricting episodes to be explicit or presupposed and nothing supplies them.

Equations

• BonehDoron2013.wouldDressNoContext = { sentence := "#In the good old days, people would dress elegantly", form := BonehDoron2013.HabitualForm.would, felicitous := false, exNumber := "(2c)" }

def BonehDoron2013.wouldDressWithContext : EnglishDatum

With a purpose clause, (2d), the restriction is supplied.

Equations

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

def BonehDoron2013.sheWentByBus : EnglishDatum

She went to work by bus, (42a), is true on a single actual episode, read episodically or with Hab.

Equations

• BonehDoron2013.sheWentByBus = { sentence := "She went to work by bus", form := BonehDoron2013.HabitualForm.simpleForm, felicitous := true, exNumber := "(42a)" }

def BonehDoron2013.sheWouldGoByBus : EnglishDatum

She would go to work by bus, (42b), is true on a single episode, since would is Gen, about the accessible worlds rather than an actual iteration.

Equations

• BonehDoron2013.sheWouldGoByBus = { sentence := "She would go to work by bus", form := BonehDoron2013.HabitualForm.would, felicitous := true, exNumber := "(42b)" }

def BonehDoron2013.sheUsedToGoByBus : EnglishDatum

She used to go to work by bus, (42c), is false on a single episode. The chapter derives the actualization requirement from the aspect. The retrospective's extended reference interval characterizes a period, and only actualized episodes can characterize one.

Equations

• BonehDoron2013.sheUsedToGoByBus = { sentence := "She used to go to work by bus", form := BonehDoron2013.HabitualForm.usedTo, felicitous := false, exNumber := "(42c)" }

def BonehDoron2013.usedToStand : EnglishDatum

The London Bridge used to stand on the Thames, (48a), is felicitous, since used to is an aspectual operator selecting states, individual-level ones included.

Equations

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

def BonehDoron2013.wouldStand : EnglishDatum

The London Bridge would stand on the Thames, (48b), is ungrammatical, since habitual would is Gen, an individual-level predicate is incompatible with an episodic restrictor, and a definite subject supplies no nominal one.

Equations

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

def BonehDoron2013.wouldKnowLatin : EnglishDatum

In a French teacher would know Latin, (3a), (47a), the indefinite singular provides Gen's restrictor, of objects rather than events, so would tolerates the individual-level predicate.

Equations

• BonehDoron2013.wouldKnowLatin = { sentence := "a French teacher would know Latin", form := BonehDoron2013.HabitualForm.would, felicitous := true, exNumber := "(3a)/(47a)" }

def BonehDoron2013.usedToKnowLatin : EnglishDatum

A French teacher used to know Latin, (3b), (47b), is ungrammatical, since used to is aspectual rather than quantificational. The indefinite singular finds no operator below Gen, and Gen over the whole clause, (50b), gives the wrong truth conditions. A bare plural instead denotes the kind and combines directly, (50a).

Equations

• BonehDoron2013.usedToKnowLatin = { sentence := "*a French teacher used to know Latin", form := BonehDoron2013.HabitualForm.usedTo, felicitous := false, exNumber := "(3b)/(47b)" }

theorem BonehDoron2013.restrictor_contrast : maryCigaretteAfterDinner.felicitous = true ∧ maryCigarette.felicitous = false

Gen with a restrictor is felicitous and Hab with a wide-scope indefinite is not, (4).

theorem BonehDoron2013.sameObjectParallel : flowerGrows.felicitous = true ∧ maxKilledRabbit.felicitous = false

The same-object reading decides felicity, plausible for the flower and absurd for the rabbit, (6b), (7b).

theorem BonehDoron2013.actualization_contrast : sheWentByBus.felicitous = true ∧ sheWouldGoByBus.felicitous = true ∧ sheUsedToGoByBus.felicitous = false

One actual episode verifies the simple form and would but not used to, (42).

theorem BonehDoron2013.individual_level_contrast : usedToStand.felicitous = true ∧ wouldStand.felicitous = false

Used to selects individual-level states, and habitual would cannot restrict Gen with them, (48).

theorem BonehDoron2013.would_vs_usedTo_puzzle : wouldKnowLatin.felicitous = true ∧ usedToKnowLatin.felicitous = false

The indefinite singular restricts Gen under would but has no host under aspectual used to, (3), (47).