Del Prete (2013): Imperfectivity and habituality in Italian

This file formalizes the plurality-based analysis of the Italian Imperfetto in [DP13]. A bare imperfective is habitual or progressive according to whether its reference situation is large or small, and on the habitual reading a singular indefinite object is understood as the same object across the repeated events, the same-object effect of (2). The imperfective feature spreads an event property over the forward expansion of the reference situation in a branching model of situations, (16): every branch of the expanded situation lies within the temporal trace of some event with the property. Verbs refer to plural events, [Kra08]'s lexical cumulativity hypothesis, and thematic roles are sum homomorphisms from events into the lattice of individuals of [Lin83] and [Kri98], so a plural event whose theme is a singular individual has that individual as the theme of each of its singular sub-events, the sameness principle SSP. The same-object effect is thereby an entailment of the truth conditions (24), and over a large reference situation the covering event must be plural, §5. A bare plural names the kind, [Car77a] and [Chi98], and a predication of a kind distributes its instances over the singular sub-events, (21), so bare plurals show a kind-level effect only, (30); the Q-adverb sempre forms a restricted universal over situations below the imperfective, (29), and the indefinite in its scope varies with the situation. The oddness of (2b) against (2a) is then [Mag09]'s principle (O), §7: habitually reading one philosophy book conflicts with common knowledge, habitually driving one sports car does not. Against the covert quantifier GEN of [KPC+95], §2, the obligatory wide scope of indefinites that the effect would demand gives the negated kind indefinite of (9b) the truth conditions (10b), strictly weaker than the intuitive (10'b), whatever the appropriate situations GEN quantifies over (genWide_of_genNarrow, not_genNarrow_of_genWide).

Implementation notes

Tense and the reference time adverbial, (15) and (18), fix the reference situation, which matters to the analysis only through its size, so the theorems are stated at the level of the aspectual phrase, (24e). The branches of a situation are its sub-situations lying within a single history, given by a predicate linear, and the forward expansion, taken from [Deo09] and which the chapter does not take to be a function, is a parameter fexp chosen per utterance. Verbs are event predicates with the agent conjunct folded in, the lexical cumulativity hypothesis is Mereology.AlgClosure of the singular events, and a plural event is Mereology.IsPlural, the iteration of the same volume's [BD13]. The kind of a noun is a parameter, the sum of its individuals, and a "kind coerced" indefinite ranges over a given set of sub-kinds, parts of the kind. Example numbers are those of the HAL preprint hal-00920848.

TODO

Footnote 28 argues that the sports car of (22) cannot vary across the branches of the expanded situation, since the reference situation itself lies within the trace of each covering event. The truth conditions (24g) choose a covering event per branch, and no axiom of the model identifies the parts of two such events at the reference situation, so the sameness proved in hab_soe is per covering event.

References

• [DP13]
• [Kra08]
• [Lin83]
• [Kri98]
• [Car77a]
• [Chi98]
• [Mag09]
• [KPC+95]
• [BD13]
• [Deo09]

def DelPrete2013.AtomicPart {α : Type u_4} [PartialOrder α] (x y : α) : Prop

x is an atomic part of y, the chapter's x AT y.

Equations

• DelPrete2013.AtomicPart x y = (Mereology.Atom x ∧ x ≤ y)

Throughout and the imperfective, §4.1

def DelPrete2013.Branch {S : Type u_1} [SemilatticeSup S] (linear : S → Prop) (b s : S) : Prop

A branch of a situation: a sub-situation lying within a single history.

Equations

• DelPrete2013.Branch linear b s = (linear b ∧ b ≤ s)

def DelPrete2013.THR {S : Type u_1} {E : Type u_2} [SemilatticeSup S] [SemilatticeSup E] (linear : S → Prop) (τ : SupHom E S) (P : E → Prop) (s : S) : Prop

(16a) THR: P holds throughout s when every branch of s lies within the trace of a P-event.

Equations

• DelPrete2013.THR linear τ P s = ∀ (b : S), DelPrete2013.Branch linear b s → ∃ (e : E), P e ∧ b ≤ τ e

def DelPrete2013.IMPF {S : Type u_1} {E : Type u_2} [SemilatticeSup S] [SemilatticeSup E] (linear : S → Prop) (τ : SupHom E S) (fexp : S → S) (P : E → Prop) (s : S) : Prop

(16b) IMPF: P holds throughout the forward expansion of the reference situation.

Equations

• DelPrete2013.IMPF linear τ fexp P s = DelPrete2013.THR linear τ P (fexp s)

def DelPrete2013.Large {S : Type u_1} {E : Type u_2} [SemilatticeSup S] [SemilatticeSup E] (linear : S → Prop) (τ : SupHom E S) (V₀ : E → Prop) (s : S) : Prop

A situation is large for V₀-events when no singular V₀-event's trace covers a branch of it, the size that forces a plural covering event, §5.

Equations

• DelPrete2013.Large linear τ V₀ s = ∀ (b : S), DelPrete2013.Branch linear b s → ∀ (e : E), V₀ e → ¬b ≤ τ e

theorem DelPrete2013.isPlural_of_large {S : Type u_1} {E : Type u_2} [SemilatticeSup S] [SemilatticeSup E] {linear : S → Prop} {τ : SupHom E S} {V₀ : E → Prop} (hV₀ : ∀ ⦃e : E⦄, V₀ e → Mereology.Atom e) {s : S} (hL : Large linear τ V₀ s) {b : S} (hb : Branch linear b s) {e : E} (he : Mereology.AlgClosure V₀ e) (hbe : b ≤ τ e) : Mereology.IsPlural V₀ e

HAB, §5: over a large situation, a covering event of a cumulative verb is plural.

theorem DelPrete2013.impf_of_le {S : Type u_1} {E : Type u_2} [SemilatticeSup S] [SemilatticeSup E] {linear : S → Prop} {τ : SupHom E S} {V₀ : E → Prop} {fexp : S → S} {s : S} {e : E} (he : V₀ e) (hs : fexp s ≤ τ e) : IMPF linear τ fexp (Mereology.AlgClosure V₀) s

PROG, §5: over a small reference situation, a single singular event whose trace covers the expanded situation verifies the same denotation.

Singular indefinites, bare plurals and Q-adverbs, §4.3

def DelPrete2013.indefinite {E : Type u_2} {I : Type u_3} [SemilatticeSup E] [SemilatticeSup I] (Th : SupHom E I) (N : I → Prop) (V : E → Prop) (e : E) : Prop

(24d): a verb with a singular indefinite object, λe. ∃x [N(x) ∧ V(e) ∧ Th(e) = x].

Equations

• DelPrete2013.indefinite Th N V e = ∃ (x : I), N x ∧ V e ∧ Th e = x

def DelPrete2013.distributes {E : Type u_2} {I : Type u_3} [SemilatticeSup E] [SemilatticeSup I] (P : E → I → Prop) (e : E) (k : I) : Prop

(21) Distribution to Sub-Events: a predication of a plural event and a kind distributes instances of the kind over the singular sub-events.

Equations

• DelPrete2013.distributes P e k = ∀ (e' : E), DelPrete2013.AtomicPart e' e → ∃ (x : I), DelPrete2013.AtomicPart x k ∧ P e' x

def DelPrete2013.barePlural {E : Type u_2} {I : Type u_3} [SemilatticeSup E] [SemilatticeSup I] (Th : SupHom E I) (V : E → Prop) (k : I) (e : E) : Prop

(30''a): a verb with a bare plural object names the kind k of the noun, and the predication distributes by (21).

Equations

• DelPrete2013.barePlural Th V k e = DelPrete2013.distributes (fun (e : E) (x : I) => V e ∧ Th e = x) e k

def DelPrete2013.kindIndefinite {E : Type u_2} {I : Type u_3} [SemilatticeSup E] [SemilatticeSup I] (Th : SupHom E I) (K : I → Prop) (V : E → Prop) (e : E) : Prop

(27a,b): a "kind coerced" singular indefinite quantifies over the sub-kinds K of the noun's kind, and the predication of the sub-kind distributes by (21).

Equations

• DelPrete2013.kindIndefinite Th K V e = ∃ (X : I), K X ∧ DelPrete2013.barePlural Th V X e

def DelPrete2013.sempre {S : Type u_1} {E : Type u_2} [SemilatticeSup E] (C : S → Prop) (R : E → S → Prop) (P : E → Prop) (e₀ : E) : Prop

(29''b) [sempre C]: for every situation with the contextual property C, an event with the property P in the contextual temporal relation R to it is part of the event described.

Equations

• DelPrete2013.sempre C R P e₀ = ∀ (s₁ : S), C s₁ → ∃ (e₁ : E), P e₁ ∧ R e₁ s₁ ∧ e₁ ≤ e₀

theorem DelPrete2013.ssp {E : Type u_2} {I : Type u_3} [SemilatticeSup E] [SemilatticeSup I] {Th : SupHom E I} (hTh : ∀ (e : E), Mereology.Atom e → ¬IsBot (Th e)) {x : I} (hx : Mereology.Atom x) {e e' : E} (h : Th e = x) (he' : AtomicPart e' e) : Th e' = x

(SSP) Sameness of the Singular Participant: a role mapping an event to a singular individual maps each of its singular sub-events to it, since roles are sum homomorphisms and so monotone.

theorem DelPrete2013.soe {E : Type u_2} {I : Type u_3} [SemilatticeSup E] [SemilatticeSup I] {Th : SupHom E I} (hTh : ∀ (e : E), Mereology.Atom e → ¬IsBot (Th e)) {N : I → Prop} (hN : ∀ ⦃x : I⦄, N x → Mereology.Atom x) {V : E → Prop} {e : E} (h : indefinite Th N V e) : ∃ (x : I), N x ∧ ∀ (e' : E), AtomicPart e' e → Th e' = x

The same-object effect, §5: an event of (24d) has one N-individual as the theme of each of its singular sub-events.

theorem DelPrete2013.barePlural_of_kindIndefinite {E : Type u_2} {I : Type u_3} [SemilatticeSup E] [SemilatticeSup I] {Th : SupHom E I} {K : I → Prop} {k : I} (hK : ∀ ⦃X : I⦄, K X → X ≤ k) {V : E → Prop} {e : E} (h : kindIndefinite Th K V e) : barePlural Th V k e

(9a) entails (13), §3: a kind coerced indefinite over sub-kinds of the kind entails the bare plural.

theorem DelPrete2013.not_kindIndefinite_of_barePlural : ∃ (E : Type) (I : Type) (x : SemilatticeSup E) (x_1 : SemilatticeSup I) (Th : SupHom E I) (K : I → Prop) (k : I) (V : E → Prop) (e : E), (∀ ⦃X : I⦄, K X → X ≤ k) ∧ barePlural Th V k e ∧ ¬kindIndefinite Th K V e

(13) does not entail (9a), footnote 12: Gianni smokes a Toscanello and a Mori, and no sub-kind of tuscan cigar is the kind he smokes.

theorem DelPrete2013.sempre_of_forall_not {S : Type u_1} {E : Type u_2} [SemilatticeSup E] {C : S → Prop} (hC : ∀ (s : S), ¬C s) (R : E → S → Prop) (P : E → Prop) (e₀ : E) : sempre C R P e₀

Footnote 32: with no C-situation, sempre requires no event at all.

theorem DelPrete2013.sempre_indefinite_no_soe : ∃ (S : Type) (E : Type) (I : Type) (x : SemilatticeSup E) (x_1 : SemilatticeSup I) (Th : SupHom E I) (C : S → Prop) (R : E → S → Prop) (N : I → Prop) (V : E → Prop) (e₀ : E), sempre C R (indefinite Th N V) e₀ ∧ ¬∃ (x_2 : I), ∀ (e' : E), AtomicPart e' e₀ → Th e' = x_2

(29) has no same-object effect, §6: with the indefinite in the scope of sempre, the books read on two occasions differ.

theorem DelPrete2013.barePlural_no_soe : ∃ (E : Type) (I : Type) (x : SemilatticeSup E) (x_1 : SemilatticeSup I) (Th : SupHom E I) (V : E → Prop) (k : I) (e : E), barePlural Th V k e ∧ ¬∃ (x_2 : I), ∀ (e' : E), AtomicPart e' e → Th e' = x_2

(30) has no same-object effect, §6: the bare plural distributes, and two singular readings have different books as themes.

The same-object effect and its oddness, §5 and §7

theorem DelPrete2013.hab_soe {S : Type u_1} {E : Type u_2} {I : Type u_3} [SemilatticeSup S] [SemilatticeSup E] [SemilatticeSup I] {linear : S → Prop} {τ : SupHom E S} {Th : SupHom E I} (hTh : ∀ (e : E), Mereology.Atom e → ¬IsBot (Th e)) {V₀ : E → Prop} (hV₀ : ∀ ⦃e : E⦄, V₀ e → Mereology.Atom e) {N : I → Prop} (hN : ∀ ⦃x : I⦄, N x → Mereology.Atom x) {fexp : S → S} {s : S} (hL : Large linear τ V₀ (fexp s)) (h : IMPF linear τ fexp (indefinite Th N (Mereology.AlgClosure V₀)) s) {b : S} (hb : Branch linear b (fexp s)) : ∃ (e : E), Mereology.IsPlural V₀ e ∧ b ≤ τ e ∧ ∃ (x : I), N x ∧ ∀ (e' : E), AtomicPart e' e → Th e' = x

(P1), §5: on the habitual reading, every branch of the large expanded situation is covered by a plural V₀-event, and one N-individual is the theme of each of its singular sub-events.

theorem DelPrete2013.not_impf_indefinite {S : Type u_1} {E : Type u_2} {I : Type u_3} [SemilatticeSup S] [SemilatticeSup E] [SemilatticeSup I] {linear : S → Prop} {τ : SupHom E S} {Th : SupHom E I} (hTh : ∀ (e : E), Mereology.Atom e → ¬IsBot (Th e)) {read₀ : E → Prop} (hV₀ : ∀ ⦃e : E⦄, read₀ e → Mereology.Atom e) {book : I → Prop} (hN : ∀ ⦃x : I⦄, book x → Mereology.Atom x) (hCK : ∀ (e : E), Mereology.IsPlural read₀ e → ∀ (x : I), book x → ∃ (e' : E), AtomicPart e' e ∧ Th e' ≠ x) {fexp : S → S} {s : S} (hL : Large linear τ read₀ (fexp s)) {b : S} (hb : Branch linear b (fexp s)) : ¬IMPF linear τ fexp (indefinite Th book (Mereology.AlgClosure read₀)) s

(2b) is odd on HAB by principle (O), §7: it is common knowledge that a habit of reading philosophy books involves different books, and the habitual truth conditions entail a plural reading event of one book throughout.

theorem DelPrete2013.impf_indefinite_witness : ∃ (S : Type) (E : Type) (I : Type) (x : SemilatticeSup S) (x_1 : SemilatticeSup E) (x_2 : SemilatticeSup I) (linear : S → Prop) (τ : SupHom E S) (Th : SupHom E I) (drive₀ : E → Prop) (car : I → Prop) (fexp : S → S) (s : S), (∀ ⦃e : E⦄, drive₀ e → Mereology.Atom e) ∧ (∀ ⦃x : I⦄, car x → Mereology.Atom x) ∧ (∀ (e : E), Mereology.Atom e → ¬IsBot (Th e)) ∧ Large linear τ drive₀ (fexp s) ∧ (∃ (b : S), Branch linear b (fexp s)) ∧ IMPF linear τ fexp (indefinite Th car (Mereology.AlgClosure drive₀)) s

(2a) is good on HAB, §7: a plural event of driving one sports car covers the large expanded situation, and no common knowledge excludes it.

Against the covert quantifier, §2

GEN quantifies over the appropriate situations of its restrictor, which a normality on situations selects.

def DelPrete2013.genWide {S : Type u_1} {I : Type u_3} (N : Genericity.Normality Unit S) (K : I → Prop) (φ : S → Prop) (P : I → S → Prop) : Prop

(10b): the negated kind indefinite of (9b) scoping over GEN, as assumption (α)1 demands: there is no sub-kind of tuscan cigar that Gianni smokes in every appropriate situation.

Equations

• DelPrete2013.genWide N K φ P = ¬∃ (X : I), K X ∧ () ∈ N.gen {s : S | φ s} {s : S | P X s}

def DelPrete2013.genNarrow {S : Type u_1} {I : Type u_3} (N : Genericity.Normality Unit S) (K : I → Prop) (φ : S → Prop) (P : I → S → Prop) : Prop

(10'b): the negation below GEN: in no appropriate situation does Gianni smoke a sub-kind of tuscan cigar.

Equations

• DelPrete2013.genNarrow N K φ P = (() ∈ N.gen {s : S | φ s} {s : S | ¬∃ (X : I), K X ∧ P X s})

theorem DelPrete2013.genWide_of_genNarrow {S : Type u_1} {I : Type u_3} {N : Genericity.Normality Unit S} {K : I → Prop} {φ : S → Prop} {P : I → S → Prop} (hφ : (N.normal () {s : S | φ s}).Nonempty) (h : genNarrow N K φ P) : genWide N K φ P

(10'b) is logically stronger than (10b), whatever the appropriate situations, provided there is one.

theorem DelPrete2013.not_genNarrow_of_genWide : ∃ (S : Type) (I : Type) (N : Genericity.Normality Unit S) (K : I → Prop) (φ : S → Prop) (P : I → S → Prop), (N.normal () {s : S | φ s}).Nonempty ∧ genWide N K φ P ∧ ¬genNarrow N K φ P

(10b) is too weak: where every situation is appropriate and Gianni smokes a tuscan cigar of one sub-kind or another in each, (10b) holds while (9b) is false, as (10'b) is.