inductive Phenomena.TenseAspect.Diagnostics.DiagnosticResult : Type

Result of applying a diagnostic test.

• Accept: Test is felicitous (grammatical, acceptable)
• Reject: Test is infelicitous (ungrammatical, unacceptable)
• Marginal: Test is degraded but not completely out
• Coerced: Test is acceptable but requires meaning shift

• accept : DiagnosticResult
• reject : DiagnosticResult
• marginal : DiagnosticResult
• coerced : DiagnosticResult

instance Phenomena.TenseAspect.Diagnostics.instDecidableEqDiagnosticResult : DecidableEq DiagnosticResult

Equations

• Phenomena.TenseAspect.Diagnostics.instDecidableEqDiagnosticResult x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.TenseAspect.Diagnostics.instReprDiagnosticResult : Repr DiagnosticResult

Equations

• Phenomena.TenseAspect.Diagnostics.instReprDiagnosticResult = { reprPrec := Phenomena.TenseAspect.Diagnostics.instReprDiagnosticResult.repr }

def Phenomena.TenseAspect.Diagnostics.instReprDiagnosticResult.repr : DiagnosticResult → ℕ → Std.Format

Equations

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

def Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticResult.beq : DiagnosticResult → DiagnosticResult → Bool

Equations

• Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticResult.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticResult : BEq DiagnosticResult

Equations

• Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticResult = { beq := Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticResult.beq }

def Phenomena.TenseAspect.Diagnostics.DiagnosticResult.fromBool : Bool → DiagnosticResult

Convert Bool prediction to DiagnosticResult.

Equations

• Phenomena.TenseAspect.Diagnostics.DiagnosticResult.fromBool true = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept
• Phenomena.TenseAspect.Diagnostics.DiagnosticResult.fromBool false = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.reject

def Phenomena.TenseAspect.Diagnostics.forXPrediction : Semantics.Tense.Aspect.LexicalAspect.VendlerClass → DiagnosticResult

Prediction for "for X" adverbial compatibility.

"For X" measures the duration of an atelic (unbounded) eventuality:

• "ran for an hour" ✓
• "knew French for ten years" ✓
• *"arrived for an hour" ✗
• ?"built the house for a year" — coerces to repetitive

States and activities accept "for X" straightforwardly. Achievements reject "for X" (no duration to measure). Accomplishments can accept "for X" but with coercion to activity/repetition.

Equations

• Phenomena.TenseAspect.Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept
• Phenomena.TenseAspect.Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept
• Phenomena.TenseAspect.Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.reject
• Phenomena.TenseAspect.Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.coerced

theorem Phenomena.TenseAspect.Diagnostics.forX_identifies_atelic (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) : forXPrediction c = DiagnosticResult.accept ↔ c.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic

The "for X" test identifies atelic predicates.

States and activities pass; achievements fail; accomplishments require coercion.

def Phenomena.TenseAspect.Diagnostics.inXPrediction : Semantics.Tense.Aspect.LexicalAspect.VendlerClass → DiagnosticResult

Prediction for "in X" adverbial compatibility.

"In X" measures time to reach a culmination point:

• *"ran in an hour" ✗ (no endpoint to reach)
• "arrived in an hour" ✓ (punctual, endpoint reached)
• "built the house in a year" ✓ (durative, endpoint reached)
• *"knew French in ten years" ✗ (no endpoint, state)

Only telic predicates have a culmination point to measure.

Equations

• Phenomena.TenseAspect.Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.reject
• Phenomena.TenseAspect.Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.reject
• Phenomena.TenseAspect.Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept
• Phenomena.TenseAspect.Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept

theorem Phenomena.TenseAspect.Diagnostics.inX_identifies_telic (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) : inXPrediction c = DiagnosticResult.accept ↔ c.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.telic

The "in X" test identifies telic predicates.

Achievements and accomplishments pass; states and activities fail.

def Phenomena.TenseAspect.Diagnostics.progressivePrediction : Semantics.Tense.Aspect.LexicalAspect.VendlerClass → DiagnosticResult

Prediction for progressive compatibility.

The progressive requires ongoing, dynamic eventualities:

• "John is running" ✓ (activity — paradigmatic)
• "John is building a house" ✓ (accomplishment — in progress)
• *"John is knowing French" ✗ (state — no stages)
• ?"John is arriving" — marginal (achievement, requires interpretation)

States generally reject the progressive (no stages, no development). Achievements take the progressive marginally (slow-motion, preliminary).

Equations

• Phenomena.TenseAspect.Diagnostics.progressivePrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.reject
• Phenomena.TenseAspect.Diagnostics.progressivePrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept
• Phenomena.TenseAspect.Diagnostics.progressivePrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.marginal
• Phenomena.TenseAspect.Diagnostics.progressivePrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept

theorem Phenomena.TenseAspect.Diagnostics.progressive_accepts_durative_dynamic (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) : progressivePrediction c = DiagnosticResult.accept ↔ c.duration = Semantics.Tense.Aspect.LexicalAspect.Duration.durative ∧ c.dynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic

The progressive test distinguishes dynamic and durative predicates.

Activities and accomplishments clearly accept; states reject; achievements are marginal.

def Phenomena.TenseAspect.Diagnostics.stopVingPrediction : Semantics.Tense.Aspect.LexicalAspect.VendlerClass → DiagnosticResult

Prediction for "stop V-ing" compatibility.

"Stop V-ing" presupposes an ongoing activity that ceases:

• "John stopped running" ✓ (activity)
• "John stopped building the house" ✓ (accomplishment, activity in progress)
• ?"John stopped knowing French" — marginal (states don't "stop")
• ?"John stopped recognizing her" — requires iterative reading

This test identifies predicates with internal duration/stages.

Equations

• Phenomena.TenseAspect.Diagnostics.stopVingPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.marginal
• Phenomena.TenseAspect.Diagnostics.stopVingPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept
• Phenomena.TenseAspect.Diagnostics.stopVingPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.coerced
• Phenomena.TenseAspect.Diagnostics.stopVingPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept

def Phenomena.TenseAspect.Diagnostics.imperativePrediction : Semantics.Tense.Aspect.LexicalAspect.VendlerClass → DiagnosticResult

Prediction for imperative compatibility.

Imperatives require agentive control:

• "Run!" ✓ (activity)
• "Build a house!" ✓ (accomplishment)
• *"Know French!" ✗ (state, not controllable)
• ?"Recognize her!" — marginal (achievement, not directly controllable)

Equations

• Phenomena.TenseAspect.Diagnostics.imperativePrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.reject
• Phenomena.TenseAspect.Diagnostics.imperativePrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept
• Phenomena.TenseAspect.Diagnostics.imperativePrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.marginal
• Phenomena.TenseAspect.Diagnostics.imperativePrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept

structure Phenomena.TenseAspect.Diagnostics.DiagnosticBattery : Type

Result of running all diagnostic tests on a Vendler class.

• forX : DiagnosticResult
• inX : DiagnosticResult
• progressive : DiagnosticResult
• stopVing : DiagnosticResult
• imperative : DiagnosticResult

def Phenomena.TenseAspect.Diagnostics.instReprDiagnosticBattery.repr : DiagnosticBattery → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Diagnostics.instReprDiagnosticBattery : Repr DiagnosticBattery

Equations

• Phenomena.TenseAspect.Diagnostics.instReprDiagnosticBattery = { reprPrec := Phenomena.TenseAspect.Diagnostics.instReprDiagnosticBattery.repr }

instance Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticBattery : BEq DiagnosticBattery

Equations

• Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticBattery = { beq := Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticBattery.beq }

def Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticBattery.beq : DiagnosticBattery → DiagnosticBattery → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticBattery.beq x✝¹ x✝ = false

def Phenomena.TenseAspect.Diagnostics.runDiagnostics (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) : DiagnosticBattery

Run all diagnostics for a Vendler class.

Equations

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

def Phenomena.TenseAspect.Diagnostics.stateDiagnostics : DiagnosticBattery

Expected diagnostic battery for states.

Equations

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

def Phenomena.TenseAspect.Diagnostics.activityDiagnostics : DiagnosticBattery

Expected diagnostic battery for activities.

Equations

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

def Phenomena.TenseAspect.Diagnostics.achievementDiagnostics : DiagnosticBattery

Expected diagnostic battery for achievements.

Equations

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

def Phenomena.TenseAspect.Diagnostics.accomplishmentDiagnostics : DiagnosticBattery

Expected diagnostic battery for accomplishments.

Equations

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

theorem Phenomena.TenseAspect.Diagnostics.diagnostics_correct (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) : runDiagnostics c = match c with | Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state => stateDiagnostics | Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity => activityDiagnostics | Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement => achievementDiagnostics | Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment => accomplishmentDiagnostics

Running diagnostics on each class gives the expected battery.

structure Phenomena.TenseAspect.Diagnostics.VerbAspectData : Type

Attested aspectual data for sample verbs.

• verbLemma : String

  Verb lemma

• vendlerClass : Semantics.Tense.Aspect.LexicalAspect.VendlerClass

  Assigned Vendler class

• forXExample : String

  Example sentence for "for X"

• forXJudgment : DiagnosticResult

  Judgment for "for X"

def Phenomena.TenseAspect.Diagnostics.instReprVerbAspectData.repr : VerbAspectData → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Diagnostics.instReprVerbAspectData : Repr VerbAspectData

Equations

• Phenomena.TenseAspect.Diagnostics.instReprVerbAspectData = { reprPrec := Phenomena.TenseAspect.Diagnostics.instReprVerbAspectData.repr }

def Phenomena.TenseAspect.Diagnostics.runData : VerbAspectData

"run" — activity

Equations

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

def Phenomena.TenseAspect.Diagnostics.knowData : VerbAspectData

"know" — state

Equations

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

def Phenomena.TenseAspect.Diagnostics.buildData : VerbAspectData

"build" — accomplishment

Equations

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

def Phenomena.TenseAspect.Diagnostics.arriveData : VerbAspectData

"arrive" — achievement

Equations

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

def Phenomena.TenseAspect.Diagnostics.recognizeData : VerbAspectData

"recognize" — achievement

Equations

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

def Phenomena.TenseAspect.Diagnostics.loveData : VerbAspectData

"love" — state

Equations

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

def Phenomena.TenseAspect.Diagnostics.writeData : VerbAspectData

"write" — accomplishment (with bounded object)

Equations

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

def Phenomena.TenseAspect.Diagnostics.allVerbData : List VerbAspectData

All sample verb data

Equations

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