[GJ04]: The English Resultative as a Family of Constructions

[GJ04]

Paper data and per-datum verifications for [GJ04]. The construction-theoretic primitives (ResultativeSubconstruction, SubeventDesc, the fusion machinery, the universal-quantifier theorems) live in Syntax/ConstructionGrammar/Resultatives.lean, which this file imports.

Key claims

1. The English resultative is not one construction but a family of four subconstructions organized along two dimensions: causative/noncausative × property/path RP
2. Every resultative has a dual subevent structure: a verbal subevent (from the verb) and a constructional subevent (CAUSE + BECOME/GO from the construction)
3. The verbal and constructional subevents are linked by typed semantic relations: MEANS, RESULT, INSTANCE, or CO-OCCURRENCE
4. Full Argument Realization (FAR): all obligatory arguments of both verb and construction must be syntactically realized; shared arguments fuse
5. Semantic Coherence: verb role rV and construction role rC may fuse only if rV is construable as an instance of rC
6. Aspectual constraint: resultatives are telic iff the RP denotes a bounded path/property
7. Temporal constraint: the constructional subevent cannot temporally precede the verbal subevent

File contents

This file holds:

• The paper's eight resultative entries (hammerFlat, kickIntoField, …) and the allEntries list — concrete data points the paper discusses.
• Per-datum verification theorems demonstrating the paper's data is consistent with the construction theory.
• A separate empirical-data layer (ResultativeType, ResultativeDatum, allExamples, aspectualContrasts) holding theory-neutral grammaticality judgments and aspectual contrasts drawn from §§2–8 of the paper.

Empirical data: resultative entries

def GoldbergJackendoff2004.hammerFlat : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.kickIntoField : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.freezeSolid : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.rollIntoField : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.drinkSick : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.laughSilly : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.swingShut : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.wipeClean : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def GoldbergJackendoff2004.allEntries : List ConstructionGrammar.Resultatives.ResultativeEntry

All resultative entries.

Equations

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

Per-datum verification theorems

theorem GoldbergJackendoff2004.hammerFlat_is_causativeProperty : hammerFlat.subconstruction = ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativeProperty

theorem GoldbergJackendoff2004.kickIntoField_is_causativePath : kickIntoField.subconstruction = ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativePath

theorem GoldbergJackendoff2004.freezeSolid_is_noncausativeProperty : freezeSolid.subconstruction = ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativeProperty

theorem GoldbergJackendoff2004.rollIntoField_is_noncausativePath : rollIntoField.subconstruction = ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativePath

theorem GoldbergJackendoff2004.hammerFlat_means : hammerFlat.subeventRelation = ConstructionGrammar.Resultatives.SubeventRelation.means

theorem GoldbergJackendoff2004.freezeSolid_means : freezeSolid.subeventRelation = ConstructionGrammar.Resultatives.SubeventRelation.means

theorem GoldbergJackendoff2004.drinkSick_means : drinkSick.subeventRelation = ConstructionGrammar.Resultatives.SubeventRelation.means

theorem GoldbergJackendoff2004.all_core_entries_use_means : (allEntries.all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.subeventRelation == ConstructionGrammar.Resultatives.SubeventRelation.means) = true

All four core subconstructions use MEANS (§3, summary 97a–d). RESULT is reserved for sound-emission and disappearance subconstructions.

theorem GoldbergJackendoff2004.causative_entries_have_cause : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.subconstruction.isCausative) allEntries).all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.dualSubevent.constructional.hasCause) = true

Causative entries have CAUSE in their derived constructional subevent.

theorem GoldbergJackendoff2004.noncausative_entries_no_cause : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => !e.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => !e.dualSubevent.constructional.hasCause) = true

Noncausative entries lack CAUSE in their derived constructional subevent.

theorem GoldbergJackendoff2004.all_constructional_have_become : (allEntries.all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.dualSubevent.constructional.hasBecome) = true

All derived constructional subevents have BECOME.

theorem GoldbergJackendoff2004.noncausative_no_object_selection : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => !e.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => e.objectSelection == none) = true

Noncausative (intransitive) entries have no object selection.

theorem GoldbergJackendoff2004.causative_have_object_selection : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => e.objectSelection.isSome) = true

All causative entries specify an object selection mode.

theorem GoldbergJackendoff2004.bounded_entries_telic : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.rpBoundedness == ConstructionGrammar.Resultatives.Boundedness.bounded) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => (ConstructionGrammar.Resultatives.resultativeAspect e.rpBoundedness).telicity == Features.Telicity.telic) = true

All entries with bounded RP are telic.

Theorems migrated from Causation.Resultatives

These theorems quantify over allEntries (paper-specific data) and therefore belong with the paper, not in the Theory layer.

theorem GoldbergJackendoff2004.causative_resultative_has_cause : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.subconstruction.isCausative) allEntries).all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.dualSubevent.constructional.hasCause) = true

All causative entries in the data have CAUSE.

theorem GoldbergJackendoff2004.causative_means_have_cause : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => e.subconstruction.isCausative && e.subeventRelation == ConstructionGrammar.Resultatives.SubeventRelation.means) allEntries).all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.dualSubevent.constructional.hasCause) = true

MEANS-relation causative entries all have CAUSE.

theorem GoldbergJackendoff2004.activity_entries_become_accomplishments : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => e.bareVerbClass == Features.VendlerClass.activity && e.rpBoundedness == ConstructionGrammar.Resultatives.Boundedness.bounded) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => ConstructionGrammar.Resultatives.resultativeVendlerClass e.rpBoundedness == Features.VendlerClass.accomplishment) = true

Activity verbs in the data with bounded RPs become accomplishments.

theorem GoldbergJackendoff2004.all_have_become : (allEntries.all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.dualSubevent.constructional.hasBecome) = true

All resultative entries have BECOME.

Per-entry verb class participation

The construction-verb interaction across the four canonical Levin classes that [GJ04] discuss: manner verbs (hit = hammer/kick), change-of-state verbs (otherCoS = freeze), motion verbs (mannerOfMotion = roll/swing), and removing verbs (wipe).

theorem GoldbergJackendoff2004.all_entries_fused_cos : (allEntries.all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => e.fusedMC.changeOfState) = true

All entries acquire CoS from the construction, regardless of verb class.

theorem GoldbergJackendoff2004.all_entries_resultative_alternation : (allEntries.all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => ConstructionGrammar.predictedAlternationInConstruction e.verbMC e.subconstruction.toConstruction Semantics.Lexical.DiathesisAlternation.resultative) = true

All entries participate in the resultative alternation (none are instrument-spec).

theorem GoldbergJackendoff2004.causative_entries_causative_alternation : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => ConstructionGrammar.predictedAlternationInConstruction e.verbMC e.subconstruction.toConstruction Semantics.Lexical.DiathesisAlternation.causativeInchoative) = true

Causative entries all acquire the causative alternation.

theorem GoldbergJackendoff2004.noncausative_entries_no_new_causation : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => !e.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => decide (ConstructionGrammar.predictedAlternationInConstruction e.verbMC e.subconstruction.toConstruction Semantics.Lexical.DiathesisAlternation.causativeInchoative = e.verbMC.predictedAlternation Semantics.Lexical.DiathesisAlternation.causativeInchoative)) = true

Noncausative entries do NOT acquire the causative alternation (unless the verb already has causation — freeze/otherCoS does).

theorem GoldbergJackendoff2004.hammer_gains_cos_causation : hammerFlat.verbMC.changeOfState = false ∧ hammerFlat.verbMC.causation = false ∧ hammerFlat.fusedMC.changeOfState = true ∧ hammerFlat.fusedMC.causation = true

Hammer (hit-class): no CoS or causation alone → both added by causative construction.

theorem GoldbergJackendoff2004.freeze_already_has_cos : freezeSolid.verbMC.changeOfState = true ∧ freezeSolid.verbMC.causation = true ∧ freezeSolid.fusedMC = freezeSolid.verbMC

Freeze (otherCoS): already has CoS + causation → construction doesn't change profile.

theorem GoldbergJackendoff2004.roll_gains_cos_only : rollIntoField.verbMC.changeOfState = false ∧ rollIntoField.fusedMC.changeOfState = true ∧ rollIntoField.fusedMC.causation = false

Roll (manner-of-motion): gains CoS from construction; no causation (noncausative).

theorem GoldbergJackendoff2004.laugh_gains_cos_causation : laughSilly.verbMC.changeOfState = false ∧ laughSilly.verbMC.causation = false ∧ laughSilly.fusedMC.changeOfState = true ∧ laughSilly.fusedMC.causation = true

Laugh (performance): pure manner verb — construction adds CoS + causation.

theorem GoldbergJackendoff2004.wipe_already_has_everything : wipeClean.verbMC.changeOfState = true ∧ wipeClean.verbMC.causation = true ∧ wipeClean.fusedMC = wipeClean.verbMC

Wipe (wipe-class): already has full profile — construction is redundant.

Empirical data: grammaticality judgments

Theory-neutral grammaticality judgments and aspectual contrasts drawn from §§2–8 of the paper. These provide the shared data layer that other studies (Dendikken, Tay, Levin) connect to their own analyses.

inductive GoldbergJackendoff2004.ResultativeType : Type

What type of resultative is exemplified.

Extends the paper's 2×2 matrix (§2) with fake reflexives (§5) and anticausative property resultatives ([Lev26]).

• causativeProperty : ResultativeType
• causativePath : ResultativeType
• noncausativeProperty : ResultativeType
• noncausativePath : ResultativeType
• fakeReflexive : ResultativeType
• anticausativeProperty : ResultativeType

  Anticausative: verb doesn't alternate alone; construction licenses it ([Lev26]). Distinct from noncausativeProperty (e.g., freeze solid) where the verb independently shows the causative alternation.

@[implicit_reducible]

instance GoldbergJackendoff2004.instReprResultativeType : Repr ResultativeType

Equations

• GoldbergJackendoff2004.instReprResultativeType = { reprPrec := GoldbergJackendoff2004.instReprResultativeType.repr }

def GoldbergJackendoff2004.instReprResultativeType.repr : ResultativeType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GoldbergJackendoff2004.instDecidableEqResultativeType : DecidableEq ResultativeType

Equations

• GoldbergJackendoff2004.instDecidableEqResultativeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure GoldbergJackendoff2004.ResultativeDatum : Type

A single resultative example with judgment data.

• exId : String

  Example identifier

• sentence : String

  The sentence

• judgment : Features.Acceptability

  Acceptability judgment

• resType : ResultativeType

  Which resultative subtype

• phenomenon : String

  What phenomenon this illustrates

@[implicit_reducible]

instance GoldbergJackendoff2004.instReprResultativeDatum : Repr ResultativeDatum

Equations

• GoldbergJackendoff2004.instReprResultativeDatum = { reprPrec := GoldbergJackendoff2004.instReprResultativeDatum.repr }

def GoldbergJackendoff2004.instReprResultativeDatum.repr : ResultativeDatum → ℕ → Std.Format

Equations

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

def GoldbergJackendoff2004.instBEqResultativeDatum.beq : ResultativeDatum → ResultativeDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• GoldbergJackendoff2004.instBEqResultativeDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance GoldbergJackendoff2004.instBEqResultativeDatum : BEq ResultativeDatum

Equations

• GoldbergJackendoff2004.instBEqResultativeDatum = { beq := GoldbergJackendoff2004.instBEqResultativeDatum.beq }

Causative property resultatives (§2, ex. 5a, 7a)

def GoldbergJackendoff2004.hammer_flat : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.wipe_clean : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.paint_red : ResultativeDatum

Equations

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

Causative path resultatives (§2, ex. 5b)

def GoldbergJackendoff2004.kick_into_field : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.push_off_table : ResultativeDatum

Equations

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

Noncausative property resultatives (§2, ex. 6a)

def GoldbergJackendoff2004.freeze_solid : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.swing_shut : ResultativeDatum

Equations

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

Noncausative path resultatives (§2, ex. 6b)

def GoldbergJackendoff2004.roll_into_field : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.slide_off_table : ResultativeDatum

Equations

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

Fake reflexive resultatives (§5, ex. 9)

def GoldbergJackendoff2004.laugh_silly : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.drink_sick : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.run_ragged : ResultativeDatum

Equations

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

Aspectual contrasts (§4, Principle 27)

structure GoldbergJackendoff2004.AspectualContrast : Type

An aspectual contrast pair.

• sentence : String

  Sentence with temporal adverbial

• judgment : Features.Acceptability

  Acceptability

• adverbialType : String

  Which adverbial type

• description : String

  Description

def GoldbergJackendoff2004.instReprAspectualContrast.repr : AspectualContrast → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GoldbergJackendoff2004.instReprAspectualContrast : Repr AspectualContrast

Equations

• GoldbergJackendoff2004.instReprAspectualContrast = { reprPrec := GoldbergJackendoff2004.instReprAspectualContrast.repr }

@[implicit_reducible]

instance GoldbergJackendoff2004.instBEqAspectualContrast : BEq AspectualContrast

Equations

• GoldbergJackendoff2004.instBEqAspectualContrast = { beq := GoldbergJackendoff2004.instBEqAspectualContrast.beq }

def GoldbergJackendoff2004.instBEqAspectualContrast.beq : AspectualContrast → AspectualContrast → Bool

Equations

• One or more equations did not get rendered due to their size.
• GoldbergJackendoff2004.instBEqAspectualContrast.beq x✝¹ x✝ = false

def GoldbergJackendoff2004.hammer_flat_in : AspectualContrast

Equations

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

def GoldbergJackendoff2004.hammer_flat_for : AspectualContrast

Equations

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

def GoldbergJackendoff2004.hammer_bare_for : AspectualContrast

Equations

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

def GoldbergJackendoff2004.hammer_bare_in : AspectualContrast

Equations

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

Unacceptable resultatives (§6, semantic coherence violations)

def GoldbergJackendoff2004.eat_full : ResultativeDatum

Equations

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

def GoldbergJackendoff2004.sleep_flat : ResultativeDatum

Equations

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

Aggregate data

def GoldbergJackendoff2004.allExamples : List ResultativeDatum

Equations

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

def GoldbergJackendoff2004.aspectualContrasts : List AspectualContrast

Equations

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

Empirical verification

theorem GoldbergJackendoff2004.has_all_resultative_types : (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.causativeProperty) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.causativePath) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.noncausativeProperty) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.noncausativePath) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.fakeReflexive) = true

All four resultative types are attested in the data.

theorem GoldbergJackendoff2004.has_both_judgments : (allExamples.any fun (x : ResultativeDatum) => x.judgment == Features.Acceptability.ok) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.judgment == Features.Acceptability.unacceptable) = true

Both grammatical and ungrammatical examples are represented.

theorem GoldbergJackendoff2004.aspectual_both_adverbials : (aspectualContrasts.any fun (x : AspectualContrast) => x.adverbialType == "in-adverbial") = true ∧ (aspectualContrasts.any fun (x : AspectualContrast) => x.adverbialType == "for-adverbial") = true

The aspectual contrast data includes both in- and for-adverbials.

theorem GoldbergJackendoff2004.telic_adverbial_pattern : (hammer_flat_in.judgment == Features.Acceptability.ok) = true ∧ (hammer_flat_for.judgment == Features.Acceptability.unacceptable) = true

Telic resultatives accept in-adverbials and reject for-adverbials.

theorem GoldbergJackendoff2004.atelic_adverbial_pattern : (hammer_bare_for.judgment == Features.Acceptability.ok) = true

Atelic bare activities accept for-adverbials.