The parameter of aspect

Formalises [Smi97]'s two-component theory: aspectual meaning factors into a situation type (VendlerClass) and a viewpoint (ViewpointType), freely combinable.

The four visibility properties Smith tabulates for viewpoints (§4.1) are not restated here as a stipulated lookup — they live in Semantics/Aspect/Basic.lean as Prop-valued predicates derived from the TT–TSit interval relation ViewpointType.ttTSitRelation. Smith's Table 1 then re-emerges as the four substrate iff theorems (showsInitialPoint_iff, etc.); this file only re-packages those into the row-wise groupings Smith uses prose-side.

Main declarations

• Smith1997.perfective_closed, imperfective_open, neutral_intermediate: the row-wise visibility groupings Smith presents in §4.1.
• Smith1997.AspectualInterpretation: situation-type × viewpoint pairs.
• Smith1997.AspectualSystem, english, french, mandarin, navajo: per-language viewpoint inventories ([Smi97] §4.2).
• Smith1997.ImperfectiveParadoxArises: the imperfective-paradox locus.
• Smith1997.PerfectiveEffect, Smith1997.perfectiveEffect: completion vs termination under perfective ([Smi97] §3, pp. 67–68).

Implementation notes

VendlerClass, Telicity, and the project's project-canonical VendlerClass.HasInternalStages live in Features/Aktionsart.lean. ViewpointType and its derived visibility predicates live in Semantics/Aspect/Basic.lean. Compositional rules (composeWithNP, overrideTelicity) live in Semantics/Aspect/Composition.lean.

References

• [Smi97] Smith, The Parameter of Aspect (2nd ed., 1997).

Visibility ([Smi97] §4.1 Table 1) — row-wise groupings

theorem Smith1997.perfective_closed : Semantics.Aspect.ViewpointType.perfective.ShowsInitialPoint ∧ Semantics.Aspect.ViewpointType.perfective.ShowsFinalPoint ∧ Semantics.Aspect.ViewpointType.perfective.IsClosed

Perfective makes both endpoints visible and presents the situation as closed ([Smi97] §4.1, Table 1).

theorem Smith1997.imperfective_open : ¬Semantics.Aspect.ViewpointType.imperfective.ShowsInitialPoint ∧ ¬Semantics.Aspect.ViewpointType.imperfective.ShowsFinalPoint ∧ ¬Semantics.Aspect.ViewpointType.imperfective.IsClosed

Imperfective makes neither endpoint visible and is not closed ([Smi97] §4.1, Table 1).

theorem Smith1997.neutral_intermediate : Semantics.Aspect.ViewpointType.neutral.ShowsInitialPoint ∧ ¬Semantics.Aspect.ViewpointType.neutral.ShowsFinalPoint ∧ ¬Semantics.Aspect.ViewpointType.neutral.IsClosed

Neutral is intermediate: initial point visible (like perfective), final point not asserted (like imperfective), not closed ([Smi97] §4.2.3, p. 80).

theorem Smith1997.neutral_no_preliminary_stages : ¬Semantics.Aspect.ViewpointType.neutral.FocusesPreliminaryStages ∧ Semantics.Aspect.ViewpointType.imperfective.FocusesPreliminaryStages

Only the imperfective focuses preliminary stages; neutral does not — the discriminator between neutral and imperfective ([Smi97] §4.2.3, p. 80, ex. 41).

theorem Smith1997.neutral_between_perf_imperf : (Semantics.Aspect.ViewpointType.neutral.ShowsInitialPoint ↔ Semantics.Aspect.ViewpointType.perfective.ShowsInitialPoint) ∧ (Semantics.Aspect.ViewpointType.neutral.ShowsFinalPoint ↔ Semantics.Aspect.ViewpointType.imperfective.ShowsFinalPoint)

Neutral's initial-point visibility matches perfective's (both hold), while its final-point visibility matches imperfective's (both fail).

Independence of situation type and viewpoint ([Smi97] §4.3)

structure Smith1997.AspectualInterpretation : Type

An aspectual interpretation: situation type × viewpoint. The two components are independent — every cell of the 5 × 5 product is well-formed.

• situationType : Features.VendlerClass
• viewpoint : Semantics.Aspect.ViewpointType

def Smith1997.instDecidableEqAspectualInterpretation.decEq (x✝ x✝¹ : AspectualInterpretation) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Smith1997.instDecidableEqAspectualInterpretation : DecidableEq AspectualInterpretation

Equations

• Smith1997.instDecidableEqAspectualInterpretation = Smith1997.instDecidableEqAspectualInterpretation.decEq

def Smith1997.instReprAspectualInterpretation.repr : AspectualInterpretation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Smith1997.instReprAspectualInterpretation : Repr AspectualInterpretation

Equations

• Smith1997.instReprAspectualInterpretation = { reprPrec := Smith1997.instReprAspectualInterpretation.repr }

def Smith1997.allSituationTypes : List Features.VendlerClass

Enumeration of all 5 Vendler classes.

Equations

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

def Smith1997.allViewpoints : List Semantics.Aspect.ViewpointType

Enumeration of all 5 viewpoint types.

Equations

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

def Smith1997.allInterpretations : List AspectualInterpretation

All 5 × 5 = 25 aspectual interpretations.

Equations

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

theorem Smith1997.allInterpretations_length : allInterpretations.length = 25

theorem Smith1997.allInterpretations_nodup : allInterpretations.Nodup

Cross-linguistic viewpoint inventories ([Smi97] §4.2)

inductive Smith1997.PerfStativeParam : Type

How the perfective interacts with statives ([Smi97] pp. 69–70): three cross-linguistic patterns.

• closed : PerfStativeParam

  Perfective covers statives with a closed interpretation (French "Marie a vécu à Paris" asserts the situation is over).

• open : PerfStativeParam

  Perfective appears with statives, allowing both open and closed readings (English "Jennifer knew Turkish").

• excluded : PerfStativeParam

  Perfective does not apply to statives (Russian, Chinese, Navajo).

@[implicit_reducible]

instance Smith1997.instDecidableEqPerfStativeParam : DecidableEq PerfStativeParam

Equations

• Smith1997.instDecidableEqPerfStativeParam x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Smith1997.instReprPerfStativeParam.repr : PerfStativeParam → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Smith1997.instReprPerfStativeParam : Repr PerfStativeParam

Equations

• Smith1997.instReprPerfStativeParam = { reprPrec := Smith1997.instReprPerfStativeParam.repr }

structure Smith1997.AspectualSystem : Type

A language's aspectual system: which viewpoints are available, which is the default, and how the perfective interacts with statives.

• language : String

  Language name.

• viewpoints : List Semantics.Aspect.ViewpointType

  Available viewpoint types in this language.

• defaultViewpoint : Semantics.Aspect.ViewpointType

  Default viewpoint for aspectually vague sentences.

• perfStativeParam : PerfStativeParam

  How the perfective interacts with statives.

def Smith1997.instReprAspectualSystem.repr : AspectualSystem → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Smith1997.instReprAspectualSystem : Repr AspectualSystem

Equations

• Smith1997.instReprAspectualSystem = { reprPrec := Smith1997.instReprAspectualSystem.repr }

def Smith1997.english : AspectualSystem

English: perfective + imperfective (progressive); no neutral ([Smi97] p. 70).

Equations

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

def Smith1997.french : AspectualSystem

French: perfective + imperfective + neutral (Futur); perfective covers statives with closed reading ([Smi97] p. 70).

Equations

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

def Smith1997.mandarin : AspectualSystem

Mandarin: perfective (-le) + imperfective (zai, -zhe) + neutral (bare); perfective excludes statives.

Equations

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

def Smith1997.navajo : AspectualSystem

Navajo: perfective + imperfective + neutral (Usitative/Iterative); perfective excludes statives.

Equations

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

theorem Smith1997.universal_core (sys : AspectualSystem) : sys ∈ [english, french, mandarin, navajo] → Semantics.Aspect.ViewpointType.perfective ∈ sys.viewpoints ∧ Semantics.Aspect.ViewpointType.imperfective ∈ sys.viewpoints

All four sampled languages have at least perfective and imperfective.

theorem Smith1997.neutral_in_lvm_languages : Semantics.Aspect.ViewpointType.neutral ∈ french.viewpoints ∧ Semantics.Aspect.ViewpointType.neutral ∈ mandarin.viewpoints ∧ Semantics.Aspect.ViewpointType.neutral ∈ navajo.viewpoints

The neutral viewpoint appears in LVM (low-verbal-morphology) languages.

theorem Smith1997.english_no_neutral : Semantics.Aspect.ViewpointType.neutral ∉ english.viewpoints

English lacks the neutral viewpoint.

theorem Smith1997.three_perf_stative_patterns : english.perfStativeParam = PerfStativeParam.open ∧ french.perfStativeParam = PerfStativeParam.closed ∧ mandarin.perfStativeParam = PerfStativeParam.excluded ∧ navajo.perfStativeParam = PerfStativeParam.excluded

The three perfective–stative patterns are all attested across the sample.

WALS typology bridge

theorem Smith1997.smith_languages_have_wals_aspect : English.tenseAspectProfile.aspect = Morphology.TenseAspect.AspectMarking.grammatical ∧ French.tenseAspectProfile.aspect = Morphology.TenseAspect.AspectMarking.grammatical ∧ Mandarin.tenseAspectProfile.aspect = Morphology.TenseAspect.AspectMarking.grammatical

Smith's sample languages all have grammaticalised aspect in WALS Ch. 65. Consistent with each having both .perfective and .imperfective.

theorem Smith1997.french_neutral_has_inflectional_future : Semantics.Aspect.ViewpointType.neutral ∈ french.viewpoints ∧ French.tenseAspectProfile.future = Morphology.TenseAspect.FutureMarking.inflectional

French has the neutral viewpoint (the Futur), and WALS records French as having an inflectional future — consistent across the two encodings.

Imperfective paradox

def Smith1997.ImperfectiveParadoxArises (ai : AspectualInterpretation) : Prop

The imperfective paradox: imperfective + telic does not entail the perfective completion ("Mary was building a house" ⊭ "Mary built a house"). The paradox does not arise for atelic situations because their subinterval property makes IMPF entail PRFV.

Equations

• Smith1997.ImperfectiveParadoxArises ai = (ai.viewpoint = Semantics.Aspect.ViewpointType.imperfective ∧ ai.situationType.telicity = Features.Telicity.telic)

@[implicit_reducible]

instance Smith1997.instDecidablePredAspectualInterpretationImperfectiveParadoxArises : DecidablePred ImperfectiveParadoxArises

Equations

• Smith1997.instDecidablePredAspectualInterpretationImperfectiveParadoxArises x✝ = Smith1997.instDecidablePredAspectualInterpretationImperfectiveParadoxArises._aux_1 x✝

theorem Smith1997.paradox_impf_accomplishment : ImperfectiveParadoxArises { situationType := Features.VendlerClass.accomplishment, viewpoint := Semantics.Aspect.ViewpointType.imperfective }

theorem Smith1997.not_paradox_impf_activity : ¬ImperfectiveParadoxArises { situationType := Features.VendlerClass.activity, viewpoint := Semantics.Aspect.ViewpointType.imperfective }

theorem Smith1997.not_paradox_perfective (c : Features.VendlerClass) : ¬ImperfectiveParadoxArises { situationType := c, viewpoint := Semantics.Aspect.ViewpointType.perfective }

Perfective effect: completion vs termination ([Smi97] pp. 67–68)

inductive Smith1997.PerfectiveEffect : Type

Whether the perfective conveys completion (telic) or termination (atelic), or has no effect (non-perfective viewpoints).

• completion : PerfectiveEffect

  Natural endpoint reached.

• termination : PerfectiveEffect

  Event stopped without reaching a natural endpoint.

• noEffect : PerfectiveEffect

  Not perfective; no completion/termination asserted.

@[implicit_reducible]

instance Smith1997.instDecidableEqPerfectiveEffect : DecidableEq PerfectiveEffect

Equations

• Smith1997.instDecidableEqPerfectiveEffect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Smith1997.instReprPerfectiveEffect : Repr PerfectiveEffect

Equations

• Smith1997.instReprPerfectiveEffect = { reprPrec := Smith1997.instReprPerfectiveEffect.repr }

def Smith1997.instReprPerfectiveEffect.repr : PerfectiveEffect → ℕ → Std.Format

Equations

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

def Smith1997.perfectiveEffect (ai : AspectualInterpretation) : PerfectiveEffect

The perfective effect of an aspectual interpretation: perfective + telic → completion; perfective + atelic → termination; non-perfective viewpoints → no effect.

Equations

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

theorem Smith1997.perf_accomplishment_completes : perfectiveEffect { situationType := Features.VendlerClass.accomplishment, viewpoint := Semantics.Aspect.ViewpointType.perfective } = PerfectiveEffect.completion

theorem Smith1997.perf_activity_terminates : perfectiveEffect { situationType := Features.VendlerClass.activity, viewpoint := Semantics.Aspect.ViewpointType.perfective } = PerfectiveEffect.termination

theorem Smith1997.perf_achievement_completes : perfectiveEffect { situationType := Features.VendlerClass.achievement, viewpoint := Semantics.Aspect.ViewpointType.perfective } = PerfectiveEffect.completion

theorem Smith1997.impf_no_completion_termination (c : Features.VendlerClass) : perfectiveEffect { situationType := c, viewpoint := Semantics.Aspect.ViewpointType.imperfective } = PerfectiveEffect.noEffect

theorem Smith1997.completion_iff_telic (c : Features.VendlerClass) : perfectiveEffect { situationType := c, viewpoint := Semantics.Aspect.ViewpointType.perfective } = PerfectiveEffect.completion ↔ c.telicity = Features.Telicity.telic

Progressive requires internal stages

theorem Smith1997.progressive_requires_HasInternalStages (c : Features.VendlerClass) : Features.progressivePrediction c = Features.DiagnosticResult.accept ↔ c.HasInternalStages

The progressive accepts exactly the dynamic-durative classes — i.e. those with internal stages ([Smi97] Ch. 4). Smith's claim factored through the substrate's VendlerClass.HasInternalStages.

Compositional rule verification ([Smi97] §3.2.5, §3.3)

theorem Smith1997.external_override_is_final (v : Features.AspectualProfile) (np : MassCount) (ext : Features.Telicity) : (Semantics.Aspect.Composition.overrideTelicity (Semantics.Aspect.Composition.composeWithNP v np) ext).telicity = ext

Smith's external override (§3.2.5) is final — it absorbs all prior compositional steps.

theorem Smith1997.krifka_smith_agreement : (Semantics.Aspect.Composition.composeWithNP Features.accomplishmentProfile MassCount.count).telicity = Features.Telicity.telic ∧ (Semantics.Aspect.Composition.composeWithNP Features.accomplishmentProfile MassCount.mass).telicity = Features.Telicity.atelic

Smith and [Kri89] agree on count/mass NP composition: telic+count stays telic, telic+mass atelicises.

theorem Smith1997.semelfactive_coercion_three_ways : Features.semelfactiveProfile.duratize.toVendlerClass = Features.VendlerClass.activity ∧ (Semantics.Aspect.Composition.overrideDuration Features.semelfactiveProfile Features.Duration.durative).toVendlerClass = Features.VendlerClass.activity ∧ Features.forXPrediction Features.VendlerClass.semelfactive = Features.DiagnosticResult.coerced

Semelfactive duration-coercion gives an activity by three independent routes: profile-level duratize, feature-level overrideDuration, and diagnostic-level coercion.

Bridge to [Kri89]

theorem Smith1997.telic_iff_toMereoTag_qua (c : Features.VendlerClass) : c.telicity = Features.Telicity.telic ↔ c.telicity.toMereoTag = Core.Order.MereoTag.qua

Smith's telicity matches Krifka's mereological quantization: a Vendler class is telic iff its telicity tag is the quantized MereoTag.qua.