@cite{del-prete-2013} — Imperfectivity and Habituality in Italian

Fabio Del Prete, ch. 8 of Genericity (Mari, Beyssade, Del Prete eds.), OUP, Oxford Studies in Theoretical Linguistics 43.

Core Claim

The Italian Imperfetto (imperfective past) admits both habitual (HAB) and progressive (PROG) readings. The chapter's key empirical contribution is the Same-Object Effect (SOE): bare imperfectives with a singular indefinite in object position show an implication that the same object is involved across habitual events — e.g., "Gianni guidava un'auto sportiva" implies the same sports car each time. When this same-object reading is implausible (e.g., reading the same philosophy book repeatedly), HAB is blocked while PROG survives.

Chapter Sections Covered

• §8.1: Introduction — HAB/PROG readings, temporal anchoring (exx. 1–3)
• §8.2: GEN analysis and its inadequacy for SOEs (exx. 4–10)
• §8.3: Bare plural objects and 'kind-coerced' singular indefinites (exx. 11–14)
• §8.4: Semantic framework — PBT, LCH, IMPF (exx. 15–27) [concepts only]
• §8.5: SOE for bare imperfectives (exx. 22–27) [concepts only]
• §8.6: SOE, Q-adverbs, and bare plurals (exx. 28–30) [data]
• §8.7: Oddness explained via common knowledge (principle (O))
• §8.8: Conclusion

Argument Structure

Del Prete argues the standard covert-quantifier GEN analysis (§8.2) cannot account for the asymmetric distribution of SOEs across bare imperfectives and their adverbially-quantified/bare-plural counterparts, unless one makes stipulative assumptions about scope interactions between indefinites and GEN.

The proposed alternative (§8.4) is a non-quantificational, plurality-based analysis: HAB readings arise from event plurality under the Lexical Cumulativity Hypothesis (LCH; Kratzer 2008) combined with IMPF's forward-expansion of the reference time in a Partial Branching Time (PBT) model. The SOE is then derived as an entailment of the Sameness of Singular Participant principle (SSP), and the oddness of (2b) on HAB follows from the SOE conflicting with common knowledge (§8.7).

Connection to Existing Infrastructure

1. ViewpointAspectB (Tense/Aspect/Core.lean): imperfective/perfective distinction. The IMPF operator formalizes the same TT⊂TSit relation that Del Prete uses as the starting point for his f-exp analysis.

2. Fragments/Italian/Tense.lean: imperfetto TAMEEntry — the tense form that this chapter is about.

3. @cite{boneh-doron-2013} (BonehDoron2013.lean): Boneh & Doron's HAB/GEN distinction in ch. 6 of the same volume. Del Prete's analysis is explicitly built on their modal analysis of HAB (§8.4, eq. 41). Their English same-object data (exx. 6b, 7b) parallels Del Prete's Italian SOEs — formalized as sameObjectParallel in BonehDoron2013.

inductive Phenomena.Generics.Studies.DelPrete2013.ImperfettoReading : Type

The two readings available for the Italian Imperfetto.

@cite{del-prete-2013} §8.1: Imperfetto sentences "can have both habitual (HAB) and progressive (PROG) readings, in correlation with whether temporal anchoring is to a large or to a small reference time."

• hab : ImperfettoReading

  Habitual: "Gianni used to read the newspaper." Temporal anchoring to a large reference time.

• prog : ImperfettoReading

  Progressive: "Gianni was reading the newspaper." Temporal anchoring to a small reference time.

instance Phenomena.Generics.Studies.DelPrete2013.instDecidableEqImperfettoReading : DecidableEq ImperfettoReading

Equations

• Phenomena.Generics.Studies.DelPrete2013.instDecidableEqImperfettoReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Generics.Studies.DelPrete2013.instReprImperfettoReading.repr : ImperfettoReading → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.DelPrete2013.instReprImperfettoReading : Repr ImperfettoReading

Equations

• Phenomena.Generics.Studies.DelPrete2013.instReprImperfettoReading = { reprPrec := Phenomena.Generics.Studies.DelPrete2013.instReprImperfettoReading.repr }

instance Phenomena.Generics.Studies.DelPrete2013.instBEqImperfettoReading : BEq ImperfettoReading

Equations

• Phenomena.Generics.Studies.DelPrete2013.instBEqImperfettoReading = { beq := Phenomena.Generics.Studies.DelPrete2013.instBEqImperfettoReading.beq }

def Phenomena.Generics.Studies.DelPrete2013.instBEqImperfettoReading.beq : ImperfettoReading → ImperfettoReading → Bool

Equations

• Phenomena.Generics.Studies.DelPrete2013.instBEqImperfettoReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.Generics.Studies.DelPrete2013.ObjectType : Type

The type of the object NP, which determines SOE behavior.

@cite{del-prete-2013} §8.1, §8.3, §8.5: The crucial variable is whether the object is a singular indefinite (triggers SOE), a bare plural (no SOE, analyzed as kind-denoting), or a definite (no SOE).

• definite : ObjectType

  Definite: "il giornale" (the newspaper)

• singularIndefinite : ObjectType

  Singular indefinite: "un'auto sportiva" (a sports car)

• barePlural : ObjectType

  Bare plural: "libri di filosofia" (philosophy books)

• none : ObjectType

  No object (intransitive or PP complement)

instance Phenomena.Generics.Studies.DelPrete2013.instDecidableEqObjectType : DecidableEq ObjectType

Equations

• Phenomena.Generics.Studies.DelPrete2013.instDecidableEqObjectType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Generics.Studies.DelPrete2013.instReprObjectType.repr : ObjectType → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.DelPrete2013.instReprObjectType : Repr ObjectType

Equations

• Phenomena.Generics.Studies.DelPrete2013.instReprObjectType = { reprPrec := Phenomena.Generics.Studies.DelPrete2013.instReprObjectType.repr }

def Phenomena.Generics.Studies.DelPrete2013.instBEqObjectType.beq : ObjectType → ObjectType → Bool

Equations

• Phenomena.Generics.Studies.DelPrete2013.instBEqObjectType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.Studies.DelPrete2013.instBEqObjectType : BEq ObjectType

Equations

• Phenomena.Generics.Studies.DelPrete2013.instBEqObjectType = { beq := Phenomena.Generics.Studies.DelPrete2013.instBEqObjectType.beq }

inductive Phenomena.Generics.Studies.DelPrete2013.SOEStatus : Type

Whether a sentence displays a Same-Object Effect on its HAB reading.

@cite{del-prete-2013} §8.1, §8.5: Singular indefinites in object position under Imperfetto trigger SOEs — the object must be the same across habitual events. When this is implausible, the HAB reading is blocked.

• plausible : SOEStatus

  SOE present and plausible (same object across events is natural).

• implausible : SOEStatus

  SOE present but implausible (same object across events is odd).

• kindLevel : SOEStatus

  Kind-level SOE: same kind of object, not same individual.

• absent : SOEStatus

  No SOE (bare plural, definite, or no object).

instance Phenomena.Generics.Studies.DelPrete2013.instDecidableEqSOEStatus : DecidableEq SOEStatus

Equations

• Phenomena.Generics.Studies.DelPrete2013.instDecidableEqSOEStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Generics.Studies.DelPrete2013.instReprSOEStatus : Repr SOEStatus

Equations

• Phenomena.Generics.Studies.DelPrete2013.instReprSOEStatus = { reprPrec := Phenomena.Generics.Studies.DelPrete2013.instReprSOEStatus.repr }

def Phenomena.Generics.Studies.DelPrete2013.instReprSOEStatus.repr : SOEStatus → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.DelPrete2013.instBEqSOEStatus : BEq SOEStatus

Equations

• Phenomena.Generics.Studies.DelPrete2013.instBEqSOEStatus = { beq := Phenomena.Generics.Studies.DelPrete2013.instBEqSOEStatus.beq }

def Phenomena.Generics.Studies.DelPrete2013.instBEqSOEStatus.beq : SOEStatus → SOEStatus → Bool

Equations

• Phenomena.Generics.Studies.DelPrete2013.instBEqSOEStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Generics.Studies.DelPrete2013.ItalianDatum : Type

An Italian imperfective datum from @cite{del-prete-2013}.

• italian : String
• gloss : String
• aspect : Semantics.Tense.Aspect.Core.ViewpointAspectB
• objectType : ObjectType
• habOK : Bool
• progOK : Bool
• soe : SOEStatus
• exNumber : String

instance Phenomena.Generics.Studies.DelPrete2013.instReprItalianDatum : Repr ItalianDatum

Equations

• Phenomena.Generics.Studies.DelPrete2013.instReprItalianDatum = { reprPrec := Phenomena.Generics.Studies.DelPrete2013.instReprItalianDatum.repr }

def Phenomena.Generics.Studies.DelPrete2013.instReprItalianDatum.repr : ItalianDatum → ℕ → Std.Format

Equations

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

def Phenomena.Generics.Studies.DelPrete2013.gianniLeggeva : ItalianDatum

Ex. (1): "Gianni leggeva il giornale" — definite object, no SOE issue. Both HAB and PROG are fine.

Equations

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

def Phenomena.Generics.Studies.DelPrete2013.gianniGuidava : ItalianDatum

Ex. (2a): "Gianni guidava un'auto sportiva" — singular indefinite, SOE plausible (one can habitually drive the same sports car). Both HAB and PROG are fine.

Equations

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

def Phenomena.Generics.Studies.DelPrete2013.gianniLeggevaFilosofia : ItalianDatum

Ex. (2b): "Gianni leggeva un libro di filosofia" — singular indefinite, SOE implausible (reading the same philosophy book repeatedly is odd). HAB is blocked (#); only PROG survives.

Equations

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

def Phenomena.Generics.Studies.DelPrete2013.gianniFumavaSigaro : ItalianDatum

Ex. (3): "Gianni fumava un sigaro toscano (il Toscanello)" — singular indefinite, but SOE is at the kind level (a kind of Tuscan cigar, not an individual cigar). HAB is fine because the kind-level SOE is plausible.

This is a key data point: SOEs can be satisfied at the kind level when the indefinite is coerced to a kind-reading.

Equations

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

def Phenomena.Generics.Studies.DelPrete2013.gianniViaggia : ItalianDatum

Ex. (4a): "Gianni viaggia in treno" — bare habitual (present tense, no object). Both HAB and PROG available (here we record the generic habitual reading). No SOE issue (intransitive).

Equations

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

def Phenomena.Generics.Studies.DelPrete2013.gianniLeggevaLibri : ItalianDatum

Ex. (11): "Gianni leggeva libri di filosofia" — bare plural object, no SOE. HAB is fine; PROG is marginal (#). Key contrast with (2b): bare plural rescues HAB.

Equations

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

def Phenomena.Generics.Studies.DelPrete2013.gianniLeggeva_sempre : ItalianDatum

Ex. (8)/(29): "Gianni leggeva sempre un libro di filosofia" — same predicate as (2b) but with Q-adverb sempre 'always'. HAB is now fine (✓). The Q-adverb provides a tripartite quantificational structure at LF (§8.6), so the singular indefinite scopes below the Q-adverb and no SOE arises.

This is the key contrast with (2b): adding sempre rescues HAB for the same sentence frame.

Equations

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

def Phenomena.Generics.Studies.DelPrete2013.italianData : List ItalianDatum

Equations

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

theorem Phenomena.Generics.Studies.DelPrete2013.all_imperfective : (italianData.all fun (d : ItalianDatum) => d.aspect == Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective) = true

All examples are imperfective (the chapter studies the Imperfetto).

theorem Phenomena.Generics.Studies.DelPrete2013.soe_blocks_hab : (gianniGuidava.soe == SOEStatus.plausible) = true ∧ gianniGuidava.habOK = true ∧ (gianniLeggevaFilosofia.soe == SOEStatus.implausible) = true ∧ gianniLeggevaFilosofia.habOK = false

The SOE contrast: when SOE is implausible, HAB is blocked. (2a) with plausible SOE → HAB ✓; (2b) with implausible SOE → HAB ✗.

theorem Phenomena.Generics.Studies.DelPrete2013.bare_plural_rescues_hab : gianniLeggevaFilosofia.habOK = false ∧ gianniLeggevaLibri.habOK = true

The bare plural rescue: (2b) sing. indef. blocks HAB, but (11) bare plural with same predicate allows HAB.

theorem Phenomena.Generics.Studies.DelPrete2013.qadverb_rescues_hab : gianniLeggevaFilosofia.habOK = false ∧ gianniLeggeva_sempre.habOK = true

The Q-adverb rescue (§8.6): "sempre" rescues HAB for the same sentence frame where bare Imperfetto blocks it. (2b) without Q-adverb: HAB ✗; (29) with sempre: HAB ✓.

theorem Phenomena.Generics.Studies.DelPrete2013.hab_prog_complementarity : gianniLeggevaFilosofia.habOK = false ∧ gianniLeggevaFilosofia.progOK = true ∧ gianniLeggevaLibri.habOK = true ∧ gianniLeggevaLibri.progOK = false

The HAB/PROG complementarity for the SOE contrast: sing. indef. with implausible SOE: HAB ✗, PROG ✓ bare plural: HAB ✓, PROG ✗

theorem Phenomena.Generics.Studies.DelPrete2013.definite_object_both_readings : gianniLeggeva.habOK = true ∧ gianniLeggeva.progOK = true ∧ (gianniLeggeva.soe == SOEStatus.absent) = true ∧ (gianniLeggeva.objectType == ObjectType.definite) = true

Definite object: both readings available, no SOE.

theorem Phenomena.Generics.Studies.DelPrete2013.kind_level_soe_permits_hab : (gianniFumavaSigaro.soe == SOEStatus.kindLevel) = true ∧ gianniFumavaSigaro.habOK = true ∧ (gianniFumavaSigaro.objectType == ObjectType.singularIndefinite) = true

Kind-level SOE: singular indefinite with kind coercion permits HAB because the SOE is satisfied at the kind level.

theorem Phenomena.Generics.Studies.DelPrete2013.bare_indef_triggers_soe : (gianniGuidava.objectType == ObjectType.singularIndefinite) = true ∧ (gianniGuidava.soe != SOEStatus.absent) = true ∧ (gianniLeggevaFilosofia.objectType == ObjectType.singularIndefinite) = true ∧ (gianniLeggevaFilosofia.soe != SOEStatus.absent) = true ∧ (gianniFumavaSigaro.objectType == ObjectType.singularIndefinite) = true ∧ (gianniFumavaSigaro.soe != SOEStatus.absent) = true ∧ (gianniLeggeva.objectType == ObjectType.definite) = true ∧ (gianniLeggeva.soe == SOEStatus.absent) = true ∧ (gianniLeggevaLibri.objectType == ObjectType.barePlural) = true ∧ (gianniLeggevaLibri.soe == SOEStatus.absent) = true

In bare imperfectives (without Q-adverbs), singular indefinites trigger SOEs while other object types do not. The Q-adverb case (8)/(29) is excluded: a singular indefinite under sempre scopes below the Q-adverb, so no SOE arises.

structure Phenomena.Generics.Studies.DelPrete2013.GENScopeAssumption : Type

The two problematic scope assumptions that the GEN analysis must make to explain the SOE data.

@cite{del-prete-2013} §8.2, discussion around exx. (7)–(8): the GEN approach requires: (α1) Singular indefinites obligatorily scope above GEN (α2) Singular indefinites can scope below overt Q-adverbs

The problem is that GEN is supposed to be a phonologically silent version of sempre 'always', and should have the same syntactic properties — making (α1) and (α2) contradictory.

• label : String
• assumption : String
• problematic : Bool

def Phenomena.Generics.Studies.DelPrete2013.instReprGENScopeAssumption.repr : GENScopeAssumption → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.DelPrete2013.instReprGENScopeAssumption : Repr GENScopeAssumption

Equations

• Phenomena.Generics.Studies.DelPrete2013.instReprGENScopeAssumption = { reprPrec := Phenomena.Generics.Studies.DelPrete2013.instReprGENScopeAssumption.repr }

def Phenomena.Generics.Studies.DelPrete2013.alpha1 : GENScopeAssumption

Equations

• Phenomena.Generics.Studies.DelPrete2013.alpha1 = { label := "α1", assumption := "Singular indefinites obligatorily scope above GEN", problematic := true }

def Phenomena.Generics.Studies.DelPrete2013.alpha2 : GENScopeAssumption

Equations

• Phenomena.Generics.Studies.DelPrete2013.alpha2 = { label := "α2", assumption := "Singular indefinites can scope below overt Q-adverbs", problematic := true }

theorem Phenomena.Generics.Studies.DelPrete2013.gen_scope_assumptions_contradictory : alpha1.problematic = true ∧ alpha2.problematic = true

Both assumptions are needed but create a contradictory picture: GEN is supposed to be a covert sempre but doesn't behave like one with respect to scope of indefinites.

inductive Phenomena.Generics.Studies.DelPrete2013.TheoreticalConcept : Type

Key theoretical concepts from Del Prete's non-quantificational analysis (§8.4).

These are enumerated here for reference; full formalization would require substantial new infrastructure (PBT models, event structures with plural events, etc.).

• partialBranchingTime : TheoreticalConcept

  Partial Branching Time (PBT): A model based on Kratzerian situations where every situation has a unique past but many possible futures. Histories are maximal chains of situations.

• forwardExpansion : TheoreticalConcept

  Forward expansion (f-exp): The operation that expands a situation s forward in time, producing branches that represent expected continuations of s. Central to the lexical entry of IMPF.

• throughoutOperator : TheoreticalConcept

  THR (Throughout): A topological operator that 'spreads out' a temporal property P over a situation s and its branches. IMPF is defined as: ⟦IMPF⟧ = λs.λP. THR(P, f-exp(s)).

• lexicalCumulativity : TheoreticalConcept

  Lexical Cumulativity Hypothesis (LCH): Verbs can inherently refer to plural events (Kratzer 2008). This enables the non-quantificational analysis: plurality of events comes from the verb itself, not from a quantifier over situations.

• samenessOfSingularParticipant : TheoreticalConcept

  Sameness of Singular Participant (SSP): If a plural event e has a singular individual x as theme, then every atomic subevent of e has x as theme. This derives the SOE as an entailment.

• distributionToSubevents : TheoreticalConcept

  Distribution to Subevents: For kind-denoting themes, singular instances of the kind are distributed over atomic subevents of the plural event. This explains why bare plurals lack SOEs.

instance Phenomena.Generics.Studies.DelPrete2013.instDecidableEqTheoreticalConcept : DecidableEq TheoreticalConcept

Equations

• Phenomena.Generics.Studies.DelPrete2013.instDecidableEqTheoreticalConcept x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Generics.Studies.DelPrete2013.instReprTheoreticalConcept : Repr TheoreticalConcept

Equations

• Phenomena.Generics.Studies.DelPrete2013.instReprTheoreticalConcept = { reprPrec := Phenomena.Generics.Studies.DelPrete2013.instReprTheoreticalConcept.repr }

def Phenomena.Generics.Studies.DelPrete2013.instReprTheoreticalConcept.repr : TheoreticalConcept → ℕ → Std.Format

Equations

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

def Phenomena.Generics.Studies.DelPrete2013.instBEqTheoreticalConcept.beq : TheoreticalConcept → TheoreticalConcept → Bool

Equations

• Phenomena.Generics.Studies.DelPrete2013.instBEqTheoreticalConcept.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.Studies.DelPrete2013.instBEqTheoreticalConcept : BEq TheoreticalConcept

Equations

• Phenomena.Generics.Studies.DelPrete2013.instBEqTheoreticalConcept = { beq := Phenomena.Generics.Studies.DelPrete2013.instBEqTheoreticalConcept.beq }

structure Phenomena.Generics.Studies.DelPrete2013.OddnessPrinciple : Type

Principle (O) from §8.7: "If a sentence S has implications that conflict with common knowledge, then S is perceived as odd."

This pragmatic principle explains the asymmetric HAB availability:

• (2a) "Gianni drove a sports car" — SOE (same car) is compatible with common knowledge (people do habitually drive one car). → HAB ✓

• (2b) "Gianni read a philosophy book" — SOE (same book) conflicts with common knowledge (people don't repeatedly read the same philosophy book). → HAB perceived as odd (#).

The SOE itself is a semantic entailment of the analysis (via SSP); the oddness arises from a pragmatic conflict with common knowledge. This two-step explanation (semantic SOE + pragmatic filter) is the chapter's main result.

• sentence : String
• soeImplication : String
• conflictsWithCK : Bool
• perceivedAsOdd : Bool

def Phenomena.Generics.Studies.DelPrete2013.instReprOddnessPrinciple.repr : OddnessPrinciple → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.DelPrete2013.instReprOddnessPrinciple : Repr OddnessPrinciple

Equations

• Phenomena.Generics.Studies.DelPrete2013.instReprOddnessPrinciple = { reprPrec := Phenomena.Generics.Studies.DelPrete2013.instReprOddnessPrinciple.repr }

def Phenomena.Generics.Studies.DelPrete2013.guidava_oddness : OddnessPrinciple

Equations

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

def Phenomena.Generics.Studies.DelPrete2013.leggeva_filosofia_oddness : OddnessPrinciple

Equations

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

theorem Phenomena.Generics.Studies.DelPrete2013.oddness_from_ck_conflict : guidava_oddness.conflictsWithCK = false ∧ guidava_oddness.perceivedAsOdd = false ∧ leggeva_filosofia_oddness.conflictsWithCK = true ∧ leggeva_filosofia_oddness.perceivedAsOdd = true

The oddness follows from common-knowledge conflict: no CK conflict → not odd; CK conflict → odd.

theorem Phenomena.Generics.Studies.DelPrete2013.twostep_soe_oddness : (gianniLeggevaFilosofia.soe == SOEStatus.implausible) = true ∧ leggeva_filosofia_oddness.conflictsWithCK = true ∧ gianniLeggevaFilosofia.habOK = false

The two-step explanation: SOE is semantic (entailed by analysis), oddness is pragmatic (CK conflict). Matches soe_blocks_hab.

def Phenomena.Generics.Studies.DelPrete2013.permitsHabitualReading : Semantics.Tense.Aspect.Core.ViewpointAspectB → Bool

Whether a given viewpoint aspect permits habitual readings.

Background observation: imperfective permits HAB; perfective does not. @cite{del-prete-2013} takes this as given — the chapter's contribution is analyzing HOW the Imperfetto gives rise to HAB readings via IMPF's forward expansion and event plurality.

Equations

• Phenomena.Generics.Studies.DelPrete2013.permitsHabitualReading Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective = true
• Phenomena.Generics.Studies.DelPrete2013.permitsHabitualReading Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective = false

theorem Phenomena.Generics.Studies.DelPrete2013.imperfective_permits_habitual : permitsHabitualReading Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective = true ∧ permitsHabitualReading Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective = false

Imperfective permits habituals; perfective does not.

theorem Phenomena.Generics.Studies.DelPrete2013.aspect_permits_hab_for_all : (italianData.all fun (d : ItalianDatum) => permitsHabitualReading d.aspect) = true

All examples use imperfective aspect and the aspect permits HAB.

theorem Phenomena.Generics.Studies.DelPrete2013.soe_is_crosslinguistic : gianniGuidava.habOK = true ∧ gianniLeggevaFilosofia.habOK = false

The SOE phenomenon is cross-linguistic: English shows the same pattern. @cite{boneh-doron-2013} exx. (6b), (7b) in the same volume give the English counterparts:

• "A flower grew out of the tree trunk" (plausible SOE → ✓)
• "#Max killed a rabbit (repeatedly)" (implausible SOE → ✗)

This parallel is formalized in BonehDoron2013.sameObjectParallel.