Smith (1997): The Parameter of Aspect

This file formalizes the two-component theory of [Smi97]: aspectual meaning factors into a situation type (VendlerClass) and a viewpoint (ViewpointType), independent and freely combined. The visibility properties of chapter 4 are not stipulated per viewpoint: whether a viewpoint asserts the initial point or the final point of the situation, presents it as closed, or focuses an interval inside it are predicates over the substrate's relation between topic time and situation time, and the chapter's table of what each viewpoint makes visible is recovered as four theorems (showsInitialPoint_iff, showsFinalPoint_iff, presentsClosed_iff, focusesPreliminaryStages_iff). The perfective makes both endpoints visible and is closed, the imperfective makes neither visible and is open, and the neutral viewpoint of section 4.2.3 sits between them, including the initial point and at least one stage but never the preliminary stages that separate it from the imperfective (perfective_closed, imperfective_open, neutral_intermediate, neutral_no_preliminary_stages). Section 4.2 records the viewpoint inventories of the four languages of Part II and the three relations between the perfective and statives (Language.system); the perfective conveys completion for telic and termination for atelic situation types (perfectiveEffect, completion_iff_telic); and the imperfective paradox of section 4.3.2 is the invisibility of a telic situation's final point under a viewpoint that does not show it (CompletionInvisible).

Implementation notes

• The visibility predicates quantify over every linearly ordered time domain; the negative cases are witnessed on the integers.
• The per-language systems are the chapter's claims about which viewpoints a language grammaticizes, which viewpoint is dominant in an asymmetric system, and how its perfective treats statives. The compositional rules of section 3.3 are not formalized.

References

• [Smi97]
• [Kle94]

Visibility, section 4.1

def Smith1997.ShowsInitialPoint (v : Aspect.ViewpointType) : Prop

The viewpoint asserts the initial point of the situation.

Equations

• Smith1997.ShowsInitialPoint v = ∀ {T : Type} [inst : LinearOrder T] {tt tsit : NonemptyInterval T}, v.ttTSitRelation tt tsit → tsit.toProd.1 ∈ tt

def Smith1997.ShowsFinalPoint (v : Aspect.ViewpointType) : Prop

The viewpoint asserts the final point of the situation.

Equations

• Smith1997.ShowsFinalPoint v = ∀ {T : Type} [inst : LinearOrder T] {tt tsit : NonemptyInterval T}, v.ttTSitRelation tt tsit → tsit.toProd.2 ∈ tt

def Smith1997.PresentsClosed (v : Aspect.ViewpointType) : Prop

The viewpoint presents the situation as closed: the topic time reaches its final point.

Equations

• Smith1997.PresentsClosed v = ∀ {T : Type} [inst : LinearOrder T] {tt tsit : NonemptyInterval T}, v.ttTSitRelation tt tsit → tsit.toProd.2 ≤ tt.toProd.2

def Smith1997.FocusesPreliminaryStages (v : Aspect.ViewpointType) : Prop

The viewpoint focuses a topic time strictly inside the situation.

Equations

• Smith1997.FocusesPreliminaryStages v = ∀ {T : Type} [inst : LinearOrder T] {tt tsit : NonemptyInterval T}, v.ttTSitRelation tt tsit → tt < tsit

theorem Smith1997.showsInitialPoint_iff (v : Aspect.ViewpointType) : ShowsInitialPoint v ↔ v = Aspect.ViewpointType.perfective ∨ v = Aspect.ViewpointType.neutral

The initial point: the perfective and the neutral viewpoint assert it.

theorem Smith1997.showsFinalPoint_iff (v : Aspect.ViewpointType) : ShowsFinalPoint v ↔ v = Aspect.ViewpointType.perfective

The final point: only the perfective asserts it.

theorem Smith1997.presentsClosed_iff (v : Aspect.ViewpointType) : PresentsClosed v ↔ v = Aspect.ViewpointType.perfective ∨ v = Aspect.ViewpointType.perfect

Closure: the perfective and the perfect present the situation as closed.

theorem Smith1997.focusesPreliminaryStages_iff (v : Aspect.ViewpointType) : FocusesPreliminaryStages v ↔ v = Aspect.ViewpointType.imperfective

Preliminary stages: only the imperfective places the topic time strictly inside the situation.

theorem Smith1997.perfective_closed : ShowsInitialPoint Aspect.ViewpointType.perfective ∧ ShowsFinalPoint Aspect.ViewpointType.perfective ∧ PresentsClosed Aspect.ViewpointType.perfective

The perfective makes both endpoints visible and presents the situation as closed, section 4.2.1.

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

The imperfective makes neither endpoint visible and is open, section 4.2.2.

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

The neutral viewpoint is intermediate, section 4.2.3: the initial point visible as under the perfective, the final point unasserted as under the imperfective, and open.

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

Only the imperfective focuses preliminary stages, the discriminator between the neutral viewpoint and the imperfective, section 4.2.3, (41).

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

The neutral viewpoint sides with the perfective on the initial point and with the imperfective on the final point.

The independence of the components, section 4.3

structure Smith1997.AspectualInterpretation : Type

An aspectual interpretation: a situation type and a viewpoint, chosen independently.

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

@[instance_reducible]

instance Smith1997.instDecidableEqAspectualInterpretation : DecidableEq AspectualInterpretation

Equations

• Smith1997.instDecidableEqAspectualInterpretation = Smith1997.instDecidableEqAspectualInterpretation.decEq

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

Equations

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

def Smith1997.CompletionInvisible (ai : AspectualInterpretation) : Prop

The imperfective paradox, section 4.3.2: the situation type is visible whatever the viewpoint, so a telic situation's natural endpoint is known though not asserted under a viewpoint that does not show the final point.

Equations

• Smith1997.CompletionInvisible ai = (ai.situationType.telicity = Aspect.Telicity.telic ∧ ¬Smith1997.ShowsFinalPoint ai.viewpoint)

theorem Smith1997.completionInvisible_iff (ai : AspectualInterpretation) : CompletionInvisible ai ↔ ai.situationType.telicity = Aspect.Telicity.telic ∧ ai.viewpoint ≠ Aspect.ViewpointType.perfective

Completion is invisible exactly for telic situation types under a non-perfective viewpoint.

theorem Smith1997.walking_to_school : CompletionInvisible { situationType := Aspect.VendlerClass.accomplishment, viewpoint := Aspect.ViewpointType.imperfective }

We were walking to school, (47): an accomplishment under the imperfective.

The perfective's final point, section 4.2.1

The perfective presents its situation as closed, and the closed situation is completed or terminated according to its situation type, (10) and (11).

inductive Smith1997.PerfectiveEffect : Type

What the perfective conveys of the final point: completion for a telic situation type, termination for an atelic one, and nothing under another viewpoint.

• completion : PerfectiveEffect
• termination : PerfectiveEffect
• noEffect : PerfectiveEffect

@[instance_reducible]

instance Smith1997.instDecidableEqPerfectiveEffect : DecidableEq PerfectiveEffect

Equations

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

def Smith1997.perfectiveEffect (ai : AspectualInterpretation) : PerfectiveEffect

The perfective effect of an aspectual interpretation.

Equations

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

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

Under the perfective, completion is conveyed exactly by the telic situation types.

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

The imperfective conveys neither completion nor termination.

The aspectual systems of Part II, section 4.2

inductive Smith1997.PerfectiveStative : Type

The relation between the perfective and statives, section 4.2.1: the perfective includes the changes into and out of a state and closes it (French); it presents states open or closed (English); or it does not apply to statives (Russian, Chinese, Navajo).

• closed : PerfectiveStative
• openOrClosed : PerfectiveStative
• excluded : PerfectiveStative

@[instance_reducible]

instance Smith1997.instDecidableEqPerfectiveStative : DecidableEq PerfectiveStative

Equations

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

inductive Smith1997.Interaction : Type

The interaction of viewpoint and situation type, section 4.2: an asymmetric system in which one viewpoint is limited and the dominant one is available to every situation type, a system in which every viewpoint is available to every situation type, or one in which statives lie outside the viewpoint system.

• asymmetric (dominant : Aspect.ViewpointType) : Interaction
• symmetric : Interaction
• nonStativeOnly : Interaction

def Smith1997.instDecidableEqInteraction.decEq (x✝ x✝¹ : Interaction) : Decidable (x✝ = x✝¹)

Equations

• Smith1997.instDecidableEqInteraction.decEq (Smith1997.Interaction.asymmetric a) (Smith1997.Interaction.asymmetric b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Smith1997.instDecidableEqInteraction.decEq (Smith1997.Interaction.asymmetric dominant) Smith1997.Interaction.symmetric = isFalse ⋯
• Smith1997.instDecidableEqInteraction.decEq (Smith1997.Interaction.asymmetric dominant) Smith1997.Interaction.nonStativeOnly = isFalse ⋯
• Smith1997.instDecidableEqInteraction.decEq Smith1997.Interaction.symmetric (Smith1997.Interaction.asymmetric dominant) = isFalse ⋯
• Smith1997.instDecidableEqInteraction.decEq Smith1997.Interaction.symmetric Smith1997.Interaction.symmetric = isTrue ⋯
• Smith1997.instDecidableEqInteraction.decEq Smith1997.Interaction.symmetric Smith1997.Interaction.nonStativeOnly = isFalse Smith1997.instDecidableEqInteraction.decEq._proof_7
• Smith1997.instDecidableEqInteraction.decEq Smith1997.Interaction.nonStativeOnly (Smith1997.Interaction.asymmetric dominant) = isFalse ⋯
• Smith1997.instDecidableEqInteraction.decEq Smith1997.Interaction.nonStativeOnly Smith1997.Interaction.symmetric = isFalse Smith1997.instDecidableEqInteraction.decEq._proof_9
• Smith1997.instDecidableEqInteraction.decEq Smith1997.Interaction.nonStativeOnly Smith1997.Interaction.nonStativeOnly = isTrue ⋯

@[instance_reducible]

instance Smith1997.instDecidableEqInteraction : DecidableEq Interaction

Equations

• Smith1997.instDecidableEqInteraction = Smith1997.instDecidableEqInteraction.decEq

structure Smith1997.AspectualSystem : Type

A language's aspectual system: its viewpoints, their interaction with situation type, and the treatment of statives by the perfective.

• viewpoints : List Aspect.ViewpointType
• interaction : Interaction
• perfectiveStative : PerfectiveStative

@[instance_reducible]

instance Smith1997.instDecidableEqAspectualSystem : DecidableEq AspectualSystem

Equations

• Smith1997.instDecidableEqAspectualSystem = Smith1997.instDecidableEqAspectualSystem.decEq

def Smith1997.instDecidableEqAspectualSystem.decEq (x✝ x✝¹ : AspectualSystem) : Decidable (x✝ = x✝¹)

Equations

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

inductive Smith1997.Language : Type

The four languages of Part II.

• english : Language
• french : Language
• mandarin : Language
• navajo : Language

@[instance_reducible]

instance Smith1997.instDecidableEqLanguage : DecidableEq Language

Equations

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

def Smith1997.Language.system : Language → AspectualSystem

The systems of section 4.2: English has the perfective and the progressive, the perfective dominant, and presents states open or closed; French has the perfective, the imperfective and the neutral viewpoint of its Futur, every viewpoint available to every situation type, and its perfective closes states; Mandarin has perfectives, imperfectives and the neutral viewpoint of a sentence without a viewpoint morpheme, and Navajo the perfective, the imperfective and the neutral viewpoint of its Usitative and Iterative, both keeping statives outside the viewpoint system.

Equations

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

theorem Smith1997.excluded_iff_nonStativeOnly (l : Language) : l.system.perfectiveStative = PerfectiveStative.excluded ↔ l.system.interaction = Interaction.nonStativeOnly

A language whose perfective does not apply to statives keeps them outside its viewpoint system, and conversely.