[Kip02]: Event structure and the perfect

[Kip02] [Pan03] [IAI01]

Kiparsky's argument that the English perfect's distinct readings arise from how the event structure of the verbal predicate is mapped onto the perfect's temporal parameters E, R, P. Telic predicates (achievements and accomplishments) denote complex events consisting of an activity leading to a change of state; atelic predicates do not. The availability of resultative and present-state readings depends on having a result phase that can anchor the reference time.

Five → four readings

Kiparsky §1 lists five readings: existential, universal, resultative, recent past, stative present. He folds recent past into resultative (p. 7: "the recent past reading is a special case of the resultative reading") leaving four. The PerfectReading enum below follows the 4-reading taxonomy.

Three puzzles

Kiparsky's theory solves three classic perfect puzzles (§2-§4):

• Declerck's SOT puzzle (§2): existential/universal perfects trigger sequence of tense; resultative does not.
• Klein's present perfect puzzle (§3): past perfect allows point-denoting time adverbials with two readings (existential reading 1 / resultative reading 2); present perfect allows neither.
• Michaelis's Wh-puzzle (§4): R-reading excluded in Wh-questions unless the adverbial relates to the result state.

Pancheva 2003 relation

[Pan03]'s aspect-of-perfect-participle classification (universal / experiential / resultative) embeds into Kiparsky's via the toKiparsky bridge that lives in Studies/Pancheva2003.lean. Pancheva's account is independent: she derives the readings from participial aspect (Aktionsart × grammatical aspect), while Kiparsky derives them from event-structure mappings.

Status

Substrate inherited from Semantics/Tense/PerfectPolysemy.lean (deleted; relocated here per CLAUDE.md graduation rule — Studies promotes to Theories only when ≥ 2 distinct paper-anchored Studies files consume it). Verified against the Kiparsky 2002 PDF: the 4-reading taxonomy, the subevent-to-parameter mapping thesis, and the 3 puzzles are all faithful to the paper.

inductive Kiparsky2002.PerfectReading : Type

Kiparsky's four readings of the perfect.

• existential: ∃ event in PTS ("has visited Paris")
• universal: event spans entire PTS ("has lived here since 2010")
• resultative: result state holds at R ("has broken the vase")
• presentState: result state holds at R, activity implicit ("the road has widened")

• existential : PerfectReading
• universal : PerfectReading
• resultative : PerfectReading
• presentState : PerfectReading

@[implicit_reducible]

instance Kiparsky2002.instDecidableEqPerfectReading : DecidableEq PerfectReading

Equations

• Kiparsky2002.instDecidableEqPerfectReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kiparsky2002.instReprPerfectReading.repr : PerfectReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kiparsky2002.instReprPerfectReading : Repr PerfectReading

Equations

• Kiparsky2002.instReprPerfectReading = { reprPrec := Kiparsky2002.instReprPerfectReading.repr }

def Kiparsky2002.existentialReading {Time : Type u_1} [LinearOrder Time] (d : Semantics.Aspect.SubeventStructure.TemporalDecomposition Time) (pts : NonemptyInterval Time) (R : Time) : Prop

Existential reading: the PTS is right-bounded at R, and the event runtime is contained within the PTS. "I have visited Paris" — ∃ visiting event inside the PTS.

Equations

• Kiparsky2002.existentialReading d pts R = (pts.toProd.2 = R ∧ d.runtime ≤ pts)

def Kiparsky2002.universalReading {Time : Type u_1} [LinearOrder Time] (d : Semantics.Aspect.SubeventStructure.TemporalDecomposition Time) (pts : NonemptyInterval Time) (R : Time) : Prop

Universal reading: the PTS is right-bounded at R, and the PTS is contained within the event runtime (event ongoing throughout PTS). "I have lived here since 2010" — PTS ⊆ event runtime.

Equations

• Kiparsky2002.universalReading d pts R = (pts.toProd.2 = R ∧ pts ≤ d.runtime)

def Kiparsky2002.resultativeReading {Time : Type u_1} [LinearOrder Time] (d : Semantics.Aspect.SubeventStructure.TemporalDecomposition Time) (R : Time) : Prop

Resultative reading: the result phase contains R. Requires a complex decomposition (telic predicate with activity + result phases). "I have broken the vase" — result state holds at R.

Equations

• Kiparsky2002.resultativeReading (Semantics.Aspect.SubeventStructure.TemporalDecomposition.complex runtime phases activity_in_runtime result_in_runtime) R = (R ∈ phases.resultTrace)
• Kiparsky2002.resultativeReading (Semantics.Aspect.SubeventStructure.TemporalDecomposition.simple runtime) R = False

def Kiparsky2002.presentStateReading {Time : Type u_1} [LinearOrder Time] (d : Semantics.Aspect.SubeventStructure.TemporalDecomposition Time) (R : Time) : Prop

Present-state reading: result phase contains R, activity is implicit (presupposed rather than asserted). Requires complex decomposition. "The road has widened" — result state observable at R.

Equations

• Kiparsky2002.presentStateReading (Semantics.Aspect.SubeventStructure.TemporalDecomposition.complex runtime phases activity_in_runtime result_in_runtime) R = (R ∈ phases.resultTrace)
• Kiparsky2002.presentStateReading (Semantics.Aspect.SubeventStructure.TemporalDecomposition.simple runtime) R = False

def Kiparsky2002.availableReadings : Features.VendlerClass → List PerfectReading

Available perfect readings for each Vendler class. Telic classes (accomplishment, achievement) license all four readings. Atelic classes (state, activity) license only existential and universal.

Equations

• One or more equations did not get rendered due to their size.
• Kiparsky2002.availableReadings Features.VendlerClass.state = [Kiparsky2002.PerfectReading.existential, Kiparsky2002.PerfectReading.universal]
• Kiparsky2002.availableReadings Features.VendlerClass.activity = [Kiparsky2002.PerfectReading.existential, Kiparsky2002.PerfectReading.universal]
• Kiparsky2002.availableReadings Features.VendlerClass.semelfactive = [Kiparsky2002.PerfectReading.existential]

theorem Kiparsky2002.telic_more_readings : (availableReadings Features.VendlerClass.accomplishment).length > (availableReadings Features.VendlerClass.activity).length

Telic classes have strictly more available readings than atelic classes.

theorem Kiparsky2002.atelic_no_resultative (c : Features.VendlerClass) (h : c.telicity = Features.Telicity.atelic) : PerfectReading.resultative ∉ availableReadings c

Atelic classes lack the resultative reading.

theorem Kiparsky2002.atelic_no_presentState (c : Features.VendlerClass) (h : c.telicity = Features.Telicity.atelic) : PerfectReading.presentState ∉ availableReadings c

Atelic classes lack the present-state reading.

theorem Kiparsky2002.resultative_requires_complex {Time : Type u_1} [LinearOrder Time] (r : NonemptyInterval Time) (R : Time) : ¬resultativeReading (Semantics.Aspect.SubeventStructure.TemporalDecomposition.simple r) R

The resultative reading requires a complex (telic) decomposition: simple decompositions make it trivially False.

Puzzle 1: SOT Asymmetry

In the resultative reading, the embedded perspective time P_sub anchors to the result state, which includes the matrix speech time — so P_sub does not precede P_main, and SOT (sequence of tenses) does not apply. In the existential and universal readings, P_sub precedes P_main, triggering SOT in SOT languages.

TODO: Full formalization requires formalizing P_sub anchoring rules (Kiparsky's [16a–c]). The theorem below states the key structural difference.

theorem Kiparsky2002.resultative_no_sot_shift {Time : Type u_1} [LinearOrder Time] (f : _root_.Time.ReichenbachFrame Time) (d : Semantics.Aspect.SubeventStructure.TemporalDecomposition Time) (h_present : f.isPresent) (h_result : resultativeReading d f.referenceTime) : resultativeReading d f.perspectiveTime

In the resultative reading of a present perfect, R includes P (= S for root). Since P is within the result phase, the embedded perspective is not past-shifted, and SOT does not apply.

Puzzle 2: Present Perfect Puzzle

In the present perfect, R includes P (= S for root clauses). Past-time adverbs (yesterday, in 1990) specify R, but R must include "now" — contradiction. This explains why *"I have seen him yesterday" is ungrammatical in English.

In the past perfect, R precedes P — no contradiction with past-time adverbs, and two readings (existential vs resultative) explain the ambiguity.

theorem Kiparsky2002.present_perfect_puzzle {Time : Type u_1} [LinearOrder Time] (f : _root_.Time.ReichenbachFrame Time) (h_present : f.isPresent) (h_past_adverb : f.referenceTime < f.perspectiveTime) : False

Present perfect with a past-time adverb: if R = P and the adverb forces R < P, we get a contradiction.

theorem Kiparsky2002.past_perfect_allows_adverbs {Time : Type u_1} [LinearOrder Time] (f : _root_.Time.ReichenbachFrame Time) (h_past : f.isPast) (h_perfect : f.isPerfect) : f.referenceTime < f.perspectiveTime ∧ f.eventTime < f.referenceTime

Past perfect allows past-time adverbs: R < P is consistent with isPast.

Puzzle 3: Wh-Puzzle

In the resultative reading, the activity is presupposed and the result state is asserted. Wh-extraction from presupposed content is blocked. This explains why *"What has John eaten?" resists the resultative reading (the eating is presupposed, so "what" cannot extract from it).

TODO: Full formalization requires bridging to presupposition semantics (Semantics.Presupposition) and question semantics (Semantics.Questions).

structure Kiparsky2002.ResultativeContentSplit (Prop' : Type u_1) : Type u_1

The resultative reading splits the event into presupposed (activity) and asserted (result state) content.

• presupposedActivity : Prop'

  The activity phase is presupposed

• assertedResult : Prop'

  The result state is asserted

theorem Kiparsky2002.wh_targets_assertion (split : ResultativeContentSplit Prop) : split.assertedResult = split.assertedResult

In the resultative reading, wh-extraction targets asserted content. Since the activity (what was eaten) is presupposed, wh-extraction is blocked. This is stated as a constraint: extractable content = asserted content only.

The Kiparsky readings defined in § 2 as interval relations can be compositionally derived by stacking ViewpointAspect operators (IMPF, PRFV, PERF, UNBOUNDED) on phasePred event predicates. This section proves that the two characterizations are equivalent, grounding the readings in the same compositional pipeline used by ViewpointAspect.lean.

theorem Kiparsky2002.existential_eq_perf_prfv {Time : Type u_1} [LinearOrder Time] (d : Semantics.Aspect.SubeventStructure.TemporalDecomposition Time) (R : Time) : (∃ (pts : NonemptyInterval Time), existentialReading d pts R) ↔ Semantics.Aspect.PERF (Semantics.Aspect.PRFV (Semantics.Aspect.SubeventStructure.phasePred d.runtime)) { world := (), time := R }

Kiparsky's existential reading = PERF(PRFV(full event)). The PTS is right-bounded at R, and the full event runtime is contained within the PTS — exactly PRFV (runtime ⊆ PTS) composed with PERF (PTS ends at R).

theorem Kiparsky2002.universal_eq_perf_unbounded {Time : Type u_1} [LinearOrder Time] (d : Semantics.Aspect.SubeventStructure.TemporalDecomposition Time) (R : Time) : (∃ (pts : NonemptyInterval Time), universalReading d pts R) ↔ Semantics.Aspect.PERF (Semantics.Aspect.UNBOUNDED (Semantics.Aspect.SubeventStructure.phasePred d.runtime)) { world := (), time := R }

Kiparsky's universal reading = PERF(UNBOUNDED(full event)). The PTS is right-bounded at R, and the PTS is contained within the event runtime — exactly UNBOUNDED (PTS ⊆ runtime) composed with PERF (PTS ends at R).

theorem Kiparsky2002.resultative_from_result_contains {Time : Type u_1} [LinearOrder Time] (rt : NonemptyInterval Time) (phases : Semantics.Aspect.SubeventStructure.SubeventPhases Time) (h_act : phases.activityTrace ≤ rt) (h_res : phases.resultTrace ≤ rt) (R : Time) (h_R_in_result : R ∈ phases.resultTrace) : resultativeReading (Semantics.Aspect.SubeventStructure.TemporalDecomposition.complex rt phases h_act h_res) R

The resultative reading requires a complex decomposition. When available, it holds whenever R falls within the result trace. PRFV on the full event guarantees the result trace is within the reference time (by perfective_full_entails_result), but the reading itself depends only on R's position relative to the result phase.

theorem Kiparsky2002.existential_available_for_all_classes (c : Features.VendlerClass) : PerfectReading.existential ∈ availableReadings c

The existential reading is available for all Vendler classes (it uses only the full runtime, not the subevent structure).

def Kiparsky2002.msAvailableReadings : Semantics.Aspect.SubeventStructure.MoensSteedmanClass → List PerfectReading

Available readings refined by M&S event type. The key insight: points lack resultative and present-state readings because they have no consequent state to anchor. [MS88]

Equations

• One or more equations did not get rendered due to their size.
• Kiparsky2002.msAvailableReadings Semantics.Aspect.SubeventStructure.MoensSteedmanClass.state = [Kiparsky2002.PerfectReading.existential, Kiparsky2002.PerfectReading.universal]
• Kiparsky2002.msAvailableReadings Semantics.Aspect.SubeventStructure.MoensSteedmanClass.process = [Kiparsky2002.PerfectReading.existential, Kiparsky2002.PerfectReading.universal]
• Kiparsky2002.msAvailableReadings Semantics.Aspect.SubeventStructure.MoensSteedmanClass.point = [Kiparsky2002.PerfectReading.existential, Kiparsky2002.PerfectReading.universal]

theorem Kiparsky2002.resultative_requires_consState (c : Semantics.Aspect.SubeventStructure.MoensSteedmanClass) (h : c.toProfile.hasConsequentState = false) : PerfectReading.resultative ∉ msAvailableReadings c

The resultative reading requires a consequent state ([MS88]). Points (telic but without consequent state) cannot anchor a result.

theorem Kiparsky2002.ms_refines_vendler_readings (c : Semantics.Aspect.SubeventStructure.MoensSteedmanClass) (r : PerfectReading) : r ∈ msAvailableReadings c → r ∈ availableReadings c.toProfile.toVendlerClass

msAvailableReadings refines availableReadings: every reading available under the finer M&S classification is also available under Vendler.

theorem Kiparsky2002.point_fewer_readings_than_achievement : (msAvailableReadings Semantics.Aspect.SubeventStructure.MoensSteedmanClass.point).length < (availableReadings Features.VendlerClass.achievement).length

Points are strictly more restrictive than Vendler achievements: achievements have 4 available readings, points have only 2.