Perfect Polysemy

@cite{iatridou-anagnostopoulou-izvorski-2001} @cite{kiparsky-2002} @cite{pancheva-2003}

Kiparsky's "Event Structure and the Perfect" argues that the English perfect's multiple readings (existential, universal, resultative, present-state) arise from how the Perfect Time Span (PTS) interacts with the subevent structure of the predicate. Telic predicates (accomplishments, achievements) have internal activity + result phases; atelic predicates (states, activities) do not. The availability of resultative and present-state readings depends on having a result phase that can anchor the reference time.

Architecture

This module integrates:

• TemporalDecomposition (subevent phases for telic predicates)
• ViewpointAspect.PerfectType (@cite{pancheva-2003} classification)
• ReichenbachFrame with perspectiveTime (Kiparsky's P)
• Tense/Basic (tense applies R relative to P)

Sections

1. PerfectReading: Kiparsky's four readings
2. Subevent-to-parameter mappings: each reading as a predicate
3. Reading availability from VendlerClass: telicity gates resultative
4. Pancheva bridge: Pancheva's types embed into Kiparsky's
5. Kiparsky's three puzzles: SOT asymmetry, present perfect puzzle, wh-puzzle
6. Compositional derivation: existential = PERF(PRFV), universal = PERF(UNBOUNDED)

inductive Semantics.Tense.PerfectPolysemy.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

instance Semantics.Tense.PerfectPolysemy.instDecidableEqPerfectReading : DecidableEq PerfectReading

Equations

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

instance Semantics.Tense.PerfectPolysemy.instReprPerfectReading : Repr PerfectReading

Equations

• Semantics.Tense.PerfectPolysemy.instReprPerfectReading = { reprPrec := Semantics.Tense.PerfectPolysemy.instReprPerfectReading.repr }

def Semantics.Tense.PerfectPolysemy.instReprPerfectReading.repr : PerfectReading → ℕ → Std.Format

Equations

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

instance Semantics.Tense.PerfectPolysemy.instBEqPerfectReading : BEq PerfectReading

Equations

• Semantics.Tense.PerfectPolysemy.instBEqPerfectReading = { beq := Semantics.Tense.PerfectPolysemy.instBEqPerfectReading.beq }

def Semantics.Tense.PerfectPolysemy.instBEqPerfectReading.beq : PerfectReading → PerfectReading → Bool

Equations

• Semantics.Tense.PerfectPolysemy.instBEqPerfectReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Tense.PerfectPolysemy.existentialReading {Time : Type u_1} [LinearOrder Time] (d : Events.TemporalDecomposition Time) (pts : Core.Time.Interval 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

• Semantics.Tense.PerfectPolysemy.existentialReading d pts R = (pts.finish = R ∧ d.runtime.subinterval pts)

def Semantics.Tense.PerfectPolysemy.universalReading {Time : Type u_1} [LinearOrder Time] (d : Events.TemporalDecomposition Time) (pts : Core.Time.Interval 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

• Semantics.Tense.PerfectPolysemy.universalReading d pts R = (pts.finish = R ∧ pts.subinterval d.runtime)

def Semantics.Tense.PerfectPolysemy.resultativeReading {Time : Type u_1} [LinearOrder Time] (d : Events.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

• Semantics.Tense.PerfectPolysemy.resultativeReading (Semantics.Events.TemporalDecomposition.complex runtime phases activity_in_runtime result_in_runtime) R = phases.resultTrace.contains R
• Semantics.Tense.PerfectPolysemy.resultativeReading (Semantics.Events.TemporalDecomposition.simple runtime) R = False

def Semantics.Tense.PerfectPolysemy.presentStateReading {Time : Type u_1} [LinearOrder Time] (d : Events.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

• Semantics.Tense.PerfectPolysemy.presentStateReading (Semantics.Events.TemporalDecomposition.complex runtime phases activity_in_runtime result_in_runtime) R = phases.resultTrace.contains R
• Semantics.Tense.PerfectPolysemy.presentStateReading (Semantics.Events.TemporalDecomposition.simple runtime) R = False

def Semantics.Tense.PerfectPolysemy.availableReadings : Aspect.LexicalAspect.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.

theorem Semantics.Tense.PerfectPolysemy.telic_more_readings : (availableReadings Aspect.LexicalAspect.VendlerClass.accomplishment).length > (availableReadings Aspect.LexicalAspect.VendlerClass.activity).length

Telic classes have strictly more available readings than atelic classes.

theorem Semantics.Tense.PerfectPolysemy.atelic_no_resultative (c : Aspect.LexicalAspect.VendlerClass) (h : c.telicity = Aspect.LexicalAspect.Telicity.atelic) : PerfectReading.resultative ∉ availableReadings c

Atelic classes lack the resultative reading.

theorem Semantics.Tense.PerfectPolysemy.atelic_no_presentState (c : Aspect.LexicalAspect.VendlerClass) (h : c.telicity = Aspect.LexicalAspect.Telicity.atelic) : PerfectReading.presentState ∉ availableReadings c

Atelic classes lack the present-state reading.

theorem Semantics.Tense.PerfectPolysemy.resultative_requires_complex {Time : Type u_1} [LinearOrder Time] (r : Core.Time.Interval Time) (R : Time) : ¬resultativeReading (Events.TemporalDecomposition.simple r) R

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

def Semantics.Tense.PerfectPolysemy.toKiparsky : Aspect.Core.PerfectType → PerfectReading

Map @cite{pancheva-2003}'s perfect types to Kiparsky's readings.

• experiential → existential
• universal → universal
• resultative → resultative

Equations

• Semantics.Tense.PerfectPolysemy.toKiparsky Semantics.Tense.Aspect.Core.PerfectType.experiential = Semantics.Tense.PerfectPolysemy.PerfectReading.existential
• Semantics.Tense.PerfectPolysemy.toKiparsky Semantics.Tense.Aspect.Core.PerfectType.universal = Semantics.Tense.PerfectPolysemy.PerfectReading.universal
• Semantics.Tense.PerfectPolysemy.toKiparsky Semantics.Tense.Aspect.Core.PerfectType.resultative = Semantics.Tense.PerfectPolysemy.PerfectReading.resultative

theorem Semantics.Tense.PerfectPolysemy.pancheva_injective : Function.Injective toKiparsky

Pancheva's classification embeds into Kiparsky's: every Pancheva type maps to a distinct Kiparsky reading.

theorem Semantics.Tense.PerfectPolysemy.pancheva_subset_kiparsky (pt : Aspect.Core.PerfectType) : toKiparsky pt ∈ [PerfectReading.existential, PerfectReading.universal, PerfectReading.resultative, PerfectReading.presentState]

Pancheva's types are a proper subset of Kiparsky's: Kiparsky adds the present-state reading which Pancheva does not distinguish.

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 Semantics.Tense.PerfectPolysemy.resultative_no_sot_shift {Time : Type u_1} [LinearOrder Time] (f : Core.Reichenbach.ReichenbachFrame Time) (d : Events.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 Semantics.Tense.PerfectPolysemy.present_perfect_puzzle {Time : Type u_1} [LinearOrder Time] (f : Core.Reichenbach.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 Semantics.Tense.PerfectPolysemy.past_perfect_allows_adverbs {Time : Type u_1} [LinearOrder Time] (f : Core.Reichenbach.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 (Core.Presupposition) and question semantics (Semantics.Questions).

structure Semantics.Tense.PerfectPolysemy.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 Semantics.Tense.PerfectPolysemy.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 Semantics.Tense.PerfectPolysemy.existential_eq_perf_prfv {Time : Type u_1} [LinearOrder Time] (d : Events.TemporalDecomposition Time) (R : Time) : (∃ (pts : Core.Time.Interval Time), existentialReading d pts R) ↔ Aspect.Core.PERF (Aspect.Core.PRFV (Events.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 Semantics.Tense.PerfectPolysemy.universal_eq_perf_unbounded {Time : Type u_1} [LinearOrder Time] (d : Events.TemporalDecomposition Time) (R : Time) : (∃ (pts : Core.Time.Interval Time), universalReading d pts R) ↔ Aspect.Core.PERF (Aspect.Core.UNBOUNDED (Events.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 Semantics.Tense.PerfectPolysemy.resultative_from_result_contains {Time : Type u_1} [LinearOrder Time] (rt : Core.Time.Interval Time) (phases : Events.SubeventPhases Time) (h_act : phases.activityTrace.subinterval rt) (h_res : phases.resultTrace.subinterval rt) (R : Time) (h_R_in_result : phases.resultTrace.contains R) : resultativeReading (Events.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 Semantics.Tense.PerfectPolysemy.existential_available_for_all_classes (c : Aspect.LexicalAspect.VendlerClass) : PerfectReading.existential ∈ availableReadings c ∧ PerfectReading.universal ∈ availableReadings c

The existential reading is available for all Vendler classes (it uses only the full runtime, not the subevent structure). The universal reading is similarly available for all classes. These correspond to the atelic-compatible readings.

def Semantics.Tense.PerfectPolysemy.msAvailableReadings : Events.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. @cite{moens-steedman-1988}

Equations

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

theorem Semantics.Tense.PerfectPolysemy.resultative_requires_consState (c : Events.MoensSteedmanClass) (h : c.toProfile.hasConsequentState = false) : PerfectReading.resultative ∉ msAvailableReadings c

The resultative reading requires a consequent state (@cite{moens-steedman-1988}). Points (telic but without consequent state) cannot anchor a result.

theorem Semantics.Tense.PerfectPolysemy.ms_refines_vendler_readings (c : Events.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 Semantics.Tense.PerfectPolysemy.point_fewer_readings_than_achievement : (msAvailableReadings Events.MoensSteedmanClass.point).length < (availableReadings Aspect.LexicalAspect.VendlerClass.achievement).length

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