@cite{lakoff-1970} Grammaticality Judgments

@cite{lakoff-1970}

Pure empirical data from @cite{lakoff-1970} "Tense and Its Relation to Participants." No theoretical commitments — just the paper's acceptability judgments organized by phenomenon.

Key Minimal Pairs

• §1 False tense: synthetic forms (WAS, IS) can express non-temporal tense; periphrastic forms (USED TO) cannot.
• §2 SOT/novelty: present tense survives under past matrix when content is novel to hearer ("discovered that the boy HAS blue eyes").
• §4 Perfect/salience: present perfect requires current relevance (*"Shakespeare has quarreled with Bacon" vs "Shakespeare has written...").
• §5 Will-deletion: scheduled events allow present-for-future ("The meeting starts at 3"), but unscheduled events do not (*"It rains Thursday").

inductive Phenomena.TenseAspect.Studies.Lakoff1970.Data.Acceptability : Type

Acceptability judgment for a tense example.

• grammatical : Acceptability
• ungrammatical : Acceptability
• marginal : Acceptability

instance Phenomena.TenseAspect.Studies.Lakoff1970.Data.instDecidableEqAcceptability : DecidableEq Acceptability

Equations

• Phenomena.TenseAspect.Studies.Lakoff1970.Data.instDecidableEqAcceptability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.instReprAcceptability.repr : Acceptability → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.Lakoff1970.Data.instReprAcceptability : Repr Acceptability

Equations

• Phenomena.TenseAspect.Studies.Lakoff1970.Data.instReprAcceptability = { reprPrec := Phenomena.TenseAspect.Studies.Lakoff1970.Data.instReprAcceptability.repr }

instance Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqAcceptability : BEq Acceptability

Equations

• Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqAcceptability = { beq := Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqAcceptability.beq }

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqAcceptability.beq : Acceptability → Acceptability → Bool

Equations

• Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqAcceptability.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.TenseAspect.Studies.Lakoff1970.Data.TenseUseType : Type

Whether the tense use is "true" (temporal) or "false" (psychological).

• trueTense : TenseUseType
• falseTense : TenseUseType

instance Phenomena.TenseAspect.Studies.Lakoff1970.Data.instDecidableEqTenseUseType : DecidableEq TenseUseType

Equations

• Phenomena.TenseAspect.Studies.Lakoff1970.Data.instDecidableEqTenseUseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.TenseAspect.Studies.Lakoff1970.Data.instReprTenseUseType : Repr TenseUseType

Equations

• Phenomena.TenseAspect.Studies.Lakoff1970.Data.instReprTenseUseType = { reprPrec := Phenomena.TenseAspect.Studies.Lakoff1970.Data.instReprTenseUseType.repr }

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.instReprTenseUseType.repr : TenseUseType → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqTenseUseType : BEq TenseUseType

Equations

• Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqTenseUseType = { beq := Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqTenseUseType.beq }

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqTenseUseType.beq : TenseUseType → TenseUseType → Bool

Equations

• Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqTenseUseType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.TenseAspect.Studies.Lakoff1970.Data.TenseJudgment : Type

A grammaticality judgment from @cite{lakoff-1970}.

• exNumber : String

  Example number in the paper (e.g., "4a", "8a")

• sentence : String

  The sentence (abbreviated)

• tenseUse : TenseUseType

  True or false tense use

• formType : Core.Morphology.Tense.TenseFormType

  Synthetic or periphrastic form

• acceptability : Acceptability

  The paper's acceptability judgment

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.instReprTenseJudgment.repr : TenseJudgment → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.Lakoff1970.Data.instReprTenseJudgment : Repr TenseJudgment

Equations

• Phenomena.TenseAspect.Studies.Lakoff1970.Data.instReprTenseJudgment = { reprPrec := Phenomena.TenseAspect.Studies.Lakoff1970.Data.instReprTenseJudgment.repr }

instance Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqTenseJudgment : BEq TenseJudgment

Equations

• Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqTenseJudgment = { beq := Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqTenseJudgment.beq }

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqTenseJudgment.beq : TenseJudgment → TenseJudgment → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.Studies.Lakoff1970.Data.instBEqTenseJudgment.beq x✝¹ x✝ = false

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex4a : TenseJudgment

(4a) "The animal you saw WAS a chipmunk" — false past, synthetic, OK.

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex6a : TenseJudgment

(6a) "The animal you saw IS a chipmunk" — true present, synthetic, OK.

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex8a : TenseJudgment

(8a) *"The animal you saw USED TO BE a chipmunk" — false past, periphrastic, ungrammatical. The periphrastic form forces true-past reading, which conflicts with the present-time event.

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex9a : TenseJudgment

(9a) "The animal you saw USED TO BE a chipmunk" — true past, periphrastic, grammatical. It genuinely WAS a chipmunk before.

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex13a : TenseJudgment

(13a) "He discovered that the boy HAD blue eyes" — SOT past-under-past, OK.

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex13b : TenseJudgment

(13b) "He discovered that the boy HAS blue eyes" — novel-info present survives under past matrix, grammatical when content is new to hearer.

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex22a : TenseJudgment

(22a) "Shakespeare has written 37 plays" — salient (enduring relevance), OK.

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex22b : TenseJudgment

(22b) *"Shakespeare has quarreled with Bacon" — not salient (no current relevance), ungrammatical with present perfect.

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex27a : TenseJudgment

(27a) "John will die" — overt future, grammatical (control).

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex27b : TenseJudgment

(27b) "John dies tomorrow" — will-deletion with scheduled/salient event, OK.

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex25b : TenseJudgment

(25b) *"It rains Thursday" — will-deletion without salience/schedule, ungrammatical. Weather events are not scheduled.

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.allJudgments : List TenseJudgment

All judgments from the paper.

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.falseTenseJudgments : List TenseJudgment

False-tense judgments only.

Equations

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

def Phenomena.TenseAspect.Studies.Lakoff1970.Data.periphrasticJudgments : List TenseJudgment

Periphrastic judgments only.

Equations

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

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.total_count : allJudgments.length = 11

There are 11 total judgments.

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.false_tense_count : falseTenseJudgments.length = 4

There are 4 false-tense judgments.

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.periphrastic_count : periphrasticJudgments.length = 2

There are 2 periphrastic judgments.

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.false_periphrastic_ungrammatical : (List.filter (fun (x : TenseJudgment) => x.formType == Core.Morphology.Tense.TenseFormType.periphrastic) falseTenseJudgments).length = 1

The only ungrammatical false-tense-with-periphrastic example is ex8a.

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex4a_formType : ex4a.formType = Fragments.English.Tense.simplePastPerspective.formType

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex8a_formType : ex8a.formType = Fragments.English.Tense.usedTo.formType

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.ex9a_formType : ex9a.formType = Fragments.English.Tense.usedTo.formType

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.synthetic_allows_false_tense : Semantics.Tense.ParticipantPerspective.falseTenseRequiresSynthetic Semantics.Tense.ParticipantPerspective.TenseUse.falseTense Core.Morphology.Tense.TenseFormType.synthetic = true

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.periphrastic_blocks_false_tense : Semantics.Tense.ParticipantPerspective.falseTenseRequiresSynthetic Semantics.Tense.ParticipantPerspective.TenseUse.falseTense Core.Morphology.Tense.TenseFormType.periphrastic = false

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.true_tense_any_form : Semantics.Tense.ParticipantPerspective.falseTenseRequiresSynthetic Semantics.Tense.ParticipantPerspective.TenseUse.trueTense Core.Morphology.Tense.TenseFormType.periphrastic = true

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.usedTo_entry_blocks_false : Fragments.English.Tense.usedTo.allowsFalseTense = false

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.simplePast_entry_allows_false : Fragments.English.Tense.simplePastPerspective.allowsFalseTense = true

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.false_past_is_temporally_present (f : Semantics.Tense.ParticipantPerspective.TensePerspective ℤ) (h : Semantics.Tense.ParticipantPerspective.falsePast f) : f.eventTime = f.speechTime

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.false_past_classified_correctly (f : Semantics.Tense.ParticipantPerspective.TensePerspective ℤ) (h : Semantics.Tense.ParticipantPerspective.falsePast f) : Semantics.Tense.ParticipantPerspective.classifyUse Core.Tense.GramTense.past f = Semantics.Tense.ParticipantPerspective.TenseUse.falseTense

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.novel_info_licenses_present (f : Semantics.Tense.ParticipantPerspective.TensePerspective ℤ) (h : Semantics.Tense.ParticipantPerspective.novelInfoPresent f) : f.hearerNovelty = true ∧ f.eventTime = f.speechTime

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.perfect_salience_required (f : Semantics.Tense.ParticipantPerspective.TensePerspective ℤ) (h : Semantics.Tense.ParticipantPerspective.perfectRequiresSalience f) : f.speakerSalience = true

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.will_deletion_requires_future_and_salience (f : Semantics.Tense.ParticipantPerspective.TensePerspective ℤ) (h : Semantics.Tense.ParticipantPerspective.willDeletion f) : f.speechTime < f.eventTime ∧ f.speakerSalience = true

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.grammatical_false_tense_all_synthetic : ((List.filter (fun (j : TenseJudgment) => j.acceptability == Acceptability.grammatical) falseTenseJudgments).all fun (j : TenseJudgment) => j.formType == Core.Morphology.Tense.TenseFormType.synthetic) = true

theorem Phenomena.TenseAspect.Studies.Lakoff1970.Data.false_periphrastic_is_ungrammatical : (ex8a.tenseUse == TenseUseType.falseTense && ex8a.formType == Core.Morphology.Tense.TenseFormType.periphrastic && ex8a.acceptability == Acceptability.ungrammatical) = true