@cite{wellwood-2015}: Empirical Data

@cite{wellwood-2015}

Theory-neutral empirical data from @cite{wellwood-2015} on the distribution of much/many and dimensional restrictions in comparatives across nominal, verbal, and adjectival domains.

Data Sources

• §2.1: Nominal comparatives (mass vs count nouns)
• §2.2: Verbal comparatives (atelic vs telic VPs)
• §3.1–3.2: Adjectival comparatives (gradable vs non-gradable adjectives)
• §3.3: Morphosyntactic evidence (more = much + -er, @cite{bresnan-1973})
• §3.4: Dimensional restriction patterns
• §5: Number morphology and measurement (grammar shifts measurement)

inductive Phenomena.Comparison.Wellwood2015.LexCat : Type

Lexical categories relevant to Wellwood's cross-categorial analysis.

• massNoun : LexCat
• countNoun : LexCat
• atelicVP : LexCat
• telicVP : LexCat
• gradableAdj : LexCat
• nonGradableAdj : LexCat

instance Phenomena.Comparison.Wellwood2015.instDecidableEqLexCat : DecidableEq LexCat

Equations

• Phenomena.Comparison.Wellwood2015.instDecidableEqLexCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Comparison.Wellwood2015.instBEqLexCat : BEq LexCat

Equations

• Phenomena.Comparison.Wellwood2015.instBEqLexCat = { beq := Phenomena.Comparison.Wellwood2015.instBEqLexCat.beq }

def Phenomena.Comparison.Wellwood2015.instBEqLexCat.beq : LexCat → LexCat → Bool

Equations

• Phenomena.Comparison.Wellwood2015.instBEqLexCat.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Comparison.Wellwood2015.instReprLexCat : Repr LexCat

Equations

• Phenomena.Comparison.Wellwood2015.instReprLexCat = { reprPrec := Phenomena.Comparison.Wellwood2015.instReprLexCat.repr }

def Phenomena.Comparison.Wellwood2015.instReprLexCat.repr : LexCat → ℕ → Std.Format

Equations

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

structure Phenomena.Comparison.Wellwood2015.MuchFelicityDatum : Type

Observed felicity of much/more with different lexical categories.

Mass nouns and atelic VPs are felicitous with much and allow multiple measurement dimensions. Count nouns and telic VPs are anomalous. GAs are felicitous but lexically fix a single dimension. Non-GAs are anomalous (not comparable).

Examples from the paper:

• "Al bought more coffee than Bill did." ✓ (VOLUME or WEIGHT)
• "? Al has more idea than Bill does." ✗
• "Al ran more than Bill did." ✓ (DURATION or DISTANCE)
• "? Al graduated high school more than Bill did." ✗
• "Al's coffee is hotter than Bill's." ✓ (TEMPERATURE)
• "? This table is more wooden than that one." ✗

• category : LexCat
• felicitousWithMuch : Bool

  Is much/more felicitous with this category?

• multipleDimensions : Bool

  Does this category allow multiple measurement dimensions?

def Phenomena.Comparison.Wellwood2015.instDecidableEqMuchFelicityDatum.decEq (x✝ x✝¹ : MuchFelicityDatum) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Comparison.Wellwood2015.instDecidableEqMuchFelicityDatum : DecidableEq MuchFelicityDatum

Equations

• Phenomena.Comparison.Wellwood2015.instDecidableEqMuchFelicityDatum = Phenomena.Comparison.Wellwood2015.instDecidableEqMuchFelicityDatum.decEq

def Phenomena.Comparison.Wellwood2015.instBEqMuchFelicityDatum.beq : MuchFelicityDatum → MuchFelicityDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Comparison.Wellwood2015.instBEqMuchFelicityDatum.beq x✝¹ x✝ = false

instance Phenomena.Comparison.Wellwood2015.instBEqMuchFelicityDatum : BEq MuchFelicityDatum

Equations

• Phenomena.Comparison.Wellwood2015.instBEqMuchFelicityDatum = { beq := Phenomena.Comparison.Wellwood2015.instBEqMuchFelicityDatum.beq }

instance Phenomena.Comparison.Wellwood2015.instReprMuchFelicityDatum : Repr MuchFelicityDatum

Equations

• Phenomena.Comparison.Wellwood2015.instReprMuchFelicityDatum = { reprPrec := Phenomena.Comparison.Wellwood2015.instReprMuchFelicityDatum.repr }

def Phenomena.Comparison.Wellwood2015.instReprMuchFelicityDatum.repr : MuchFelicityDatum → ℕ → Std.Format

Equations

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

def Phenomena.Comparison.Wellwood2015.massNounDatum : MuchFelicityDatum

Equations

• Phenomena.Comparison.Wellwood2015.massNounDatum = { category := Phenomena.Comparison.Wellwood2015.LexCat.massNoun, felicitousWithMuch := true, multipleDimensions := true }

def Phenomena.Comparison.Wellwood2015.countNounDatum : MuchFelicityDatum

Equations

• Phenomena.Comparison.Wellwood2015.countNounDatum = { category := Phenomena.Comparison.Wellwood2015.LexCat.countNoun, felicitousWithMuch := false, multipleDimensions := false }

def Phenomena.Comparison.Wellwood2015.atelicVPDatum : MuchFelicityDatum

Equations

• Phenomena.Comparison.Wellwood2015.atelicVPDatum = { category := Phenomena.Comparison.Wellwood2015.LexCat.atelicVP, felicitousWithMuch := true, multipleDimensions := true }

def Phenomena.Comparison.Wellwood2015.telicVPDatum : MuchFelicityDatum

Equations

• Phenomena.Comparison.Wellwood2015.telicVPDatum = { category := Phenomena.Comparison.Wellwood2015.LexCat.telicVP, felicitousWithMuch := false, multipleDimensions := false }

def Phenomena.Comparison.Wellwood2015.gradableAdjDatum : MuchFelicityDatum

Equations

• Phenomena.Comparison.Wellwood2015.gradableAdjDatum = { category := Phenomena.Comparison.Wellwood2015.LexCat.gradableAdj, felicitousWithMuch := true, multipleDimensions := false }

def Phenomena.Comparison.Wellwood2015.nonGradableAdjDatum : MuchFelicityDatum

Equations

• Phenomena.Comparison.Wellwood2015.nonGradableAdjDatum = { category := Phenomena.Comparison.Wellwood2015.LexCat.nonGradableAdj, felicitousWithMuch := false, multipleDimensions := false }

structure Phenomena.Comparison.Wellwood2015.GrammarShiftDatum : Type

Number morphology and telicity shifts affect available dimensions (Wellwood §5, p. 91–93).

(104) a. "Al found more rock than Bill did." (WEIGHT, VOLUME, *NUMBER) b. "Al found more rocks than Bill did." (*WEIGHT, *VOLUME, NUMBER)

(105) a. "Al ran in the park more than Bill did." (DIST, DUR, NUMBER) b. "Al ran to the park more than Bill did." (*DIST, *DUR, NUMBER)

Shifting from mass → count (plural morpheme) or atelic → telic restricts measurement to NUMBER, blocking extensive dimensions.

• baseForm : String
• shiftedForm : String
• baseExtensive : Bool

  Base form allows extensive dimensions (WEIGHT, VOLUME, DURATION, etc.)?

• shiftedExtensive : Bool

  Shifted form allows extensive dimensions?

def Phenomena.Comparison.Wellwood2015.instReprGrammarShiftDatum.repr : GrammarShiftDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Wellwood2015.instReprGrammarShiftDatum : Repr GrammarShiftDatum

Equations

• Phenomena.Comparison.Wellwood2015.instReprGrammarShiftDatum = { reprPrec := Phenomena.Comparison.Wellwood2015.instReprGrammarShiftDatum.repr }

def Phenomena.Comparison.Wellwood2015.rockShift : GrammarShiftDatum

Ex. 104: mass → count via plural morpheme.

Equations

• Phenomena.Comparison.Wellwood2015.rockShift = { baseForm := "more rock", shiftedForm := "more rocks", baseExtensive := true, shiftedExtensive := false }

def Phenomena.Comparison.Wellwood2015.runShift : GrammarShiftDatum

Ex. 105: atelic → telic via directional PP.

Equations

• Phenomena.Comparison.Wellwood2015.runShift = { baseForm := "ran in the park more", shiftedForm := "ran to the park more", baseExtensive := true, shiftedExtensive := false }

structure Phenomena.Comparison.Wellwood2015.CrossCategorialParallel : Type

The three CUM-like categories form a natural class (all measurable by much), and the three QUA-like categories form a natural class (none measurable by much):

CUM class: mass nouns, atelic VPs, gradable adjectives QUA class: count nouns, telic VPs, non-gradable adjectives

This parallel is Wellwood's central empirical claim (§2–3).

• massNoun_atelicVP_parallel : Bool

  Mass nouns and atelic VPs behave alike (both measurable)

• countNoun_telicVP_parallel : Bool

  Count nouns and telic VPs behave alike (both not measurable)

• gradableAdj_patterns_with_measurable : Bool

  Gradable adjectives pattern with the measurable class

• nonGradableAdj_patterns_with_nonmeasurable : Bool

  Non-gradable adjectives pattern with the non-measurable class

def Phenomena.Comparison.Wellwood2015.instDecidableEqCrossCategorialParallel.decEq (x✝ x✝¹ : CrossCategorialParallel) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Comparison.Wellwood2015.instDecidableEqCrossCategorialParallel : DecidableEq CrossCategorialParallel

Equations

• Phenomena.Comparison.Wellwood2015.instDecidableEqCrossCategorialParallel = Phenomena.Comparison.Wellwood2015.instDecidableEqCrossCategorialParallel.decEq

instance Phenomena.Comparison.Wellwood2015.instBEqCrossCategorialParallel : BEq CrossCategorialParallel

Equations

• Phenomena.Comparison.Wellwood2015.instBEqCrossCategorialParallel = { beq := Phenomena.Comparison.Wellwood2015.instBEqCrossCategorialParallel.beq }

def Phenomena.Comparison.Wellwood2015.instBEqCrossCategorialParallel.beq : CrossCategorialParallel → CrossCategorialParallel → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Comparison.Wellwood2015.instBEqCrossCategorialParallel.beq x✝¹ x✝ = false

instance Phenomena.Comparison.Wellwood2015.instReprCrossCategorialParallel : Repr CrossCategorialParallel

Equations

• Phenomena.Comparison.Wellwood2015.instReprCrossCategorialParallel = { reprPrec := Phenomena.Comparison.Wellwood2015.instReprCrossCategorialParallel.repr }

def Phenomena.Comparison.Wellwood2015.instReprCrossCategorialParallel.repr : CrossCategorialParallel → ℕ → Std.Format

Equations

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

def Phenomena.Comparison.Wellwood2015.crossCategorialData : CrossCategorialParallel

Equations

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

structure Phenomena.Comparison.Wellwood2015.MuchManyDistribution : Type

@cite{bresnan-1973}: more = much + -er (§3.3, p. 82–84).

(70) a. as much soup b. too much soup c. so much soup d. that much soup e. *more much soup

much occurs with CUM-like predicates (mass nouns, atelic VPs). many is a suppletive variant of much for count/QUA domains (@cite{wellwood-2014}, fn. 11).

• much_with_cum : Bool

  much occurs with CUM-like predicates

• many_with_qua : Bool

  many occurs with QUA-like predicates

def Phenomena.Comparison.Wellwood2015.instDecidableEqMuchManyDistribution.decEq (x✝ x✝¹ : MuchManyDistribution) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Comparison.Wellwood2015.instDecidableEqMuchManyDistribution : DecidableEq MuchManyDistribution

Equations

• Phenomena.Comparison.Wellwood2015.instDecidableEqMuchManyDistribution = Phenomena.Comparison.Wellwood2015.instDecidableEqMuchManyDistribution.decEq

def Phenomena.Comparison.Wellwood2015.instBEqMuchManyDistribution.beq : MuchManyDistribution → MuchManyDistribution → Bool

Equations

• Phenomena.Comparison.Wellwood2015.instBEqMuchManyDistribution.beq { much_with_cum := a, many_with_qua := a_1 } { much_with_cum := b, many_with_qua := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Comparison.Wellwood2015.instBEqMuchManyDistribution.beq x✝¹ x✝ = false

instance Phenomena.Comparison.Wellwood2015.instBEqMuchManyDistribution : BEq MuchManyDistribution

Equations

• Phenomena.Comparison.Wellwood2015.instBEqMuchManyDistribution = { beq := Phenomena.Comparison.Wellwood2015.instBEqMuchManyDistribution.beq }

def Phenomena.Comparison.Wellwood2015.instReprMuchManyDistribution.repr : MuchManyDistribution → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Wellwood2015.instReprMuchManyDistribution : Repr MuchManyDistribution

Equations

• Phenomena.Comparison.Wellwood2015.instReprMuchManyDistribution = { reprPrec := Phenomena.Comparison.Wellwood2015.instReprMuchManyDistribution.repr }

def Phenomena.Comparison.Wellwood2015.muchManyData : MuchManyDistribution

Equations

• Phenomena.Comparison.Wellwood2015.muchManyData = { much_with_cum := true, many_with_qua := true }

inductive Phenomena.Comparison.Wellwood2015.MeasuredDomain : Type

What is actually measured in a comparative — the ontological domain whose mereological structure determines available dimensions.

Wellwood's key §3.4 insight: dimension type (intensive vs extensive) tracks the measured domain, not lexical category. GAs like hot and hard measure states (intensive), while GAs like full and heavy measure entities (extensive). Nouns like heat and firmness measure states (intensive), while coffee and plastic measure entities (extensive).

• entity : MeasuredDomain
• event : MeasuredDomain
• state : MeasuredDomain

instance Phenomena.Comparison.Wellwood2015.instDecidableEqMeasuredDomain : DecidableEq MeasuredDomain

Equations

• Phenomena.Comparison.Wellwood2015.instDecidableEqMeasuredDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Comparison.Wellwood2015.instBEqMeasuredDomain : BEq MeasuredDomain

Equations

• Phenomena.Comparison.Wellwood2015.instBEqMeasuredDomain = { beq := Phenomena.Comparison.Wellwood2015.instBEqMeasuredDomain.beq }

def Phenomena.Comparison.Wellwood2015.instBEqMeasuredDomain.beq : MeasuredDomain → MeasuredDomain → Bool

Equations

• Phenomena.Comparison.Wellwood2015.instBEqMeasuredDomain.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Comparison.Wellwood2015.instReprMeasuredDomain : Repr MeasuredDomain

Equations

• Phenomena.Comparison.Wellwood2015.instReprMeasuredDomain = { reprPrec := Phenomena.Comparison.Wellwood2015.instReprMeasuredDomain.repr }

def Phenomena.Comparison.Wellwood2015.instReprMeasuredDomain.repr : MeasuredDomain → ℕ → Std.Format

Equations

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

structure Phenomena.Comparison.Wellwood2015.DimensionReversalDatum : Type

Dimension reversal datum: a comparative form paired with its lexical category, available dimension, and what's actually measured.

The key empirical claim (§3.4, p. 85–87): changing the expression changes the measured domain, and available dimensions follow from the measured domain, not from the syntactic category.

• (82): GA hotter/harder — measures states → intensive
• (83): Noun more coffee/more plastic — measures entities → extensive
• (84): GA fuller/heavier — measures entities → extensive (reversal!)
• (85): Noun more heat/more firmness — measures states → intensive (reversal!)
• (86–89): Verbal/adverbal parallels

• form : String
• category : LexCat
• dimensionName : String
• measuredDomain : MeasuredDomain
• intensive : Bool

  Is the dimension intensive (state-measuring) rather than extensive?

def Phenomena.Comparison.Wellwood2015.instReprDimensionReversalDatum.repr : DimensionReversalDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Wellwood2015.instReprDimensionReversalDatum : Repr DimensionReversalDatum

Equations

• Phenomena.Comparison.Wellwood2015.instReprDimensionReversalDatum = { reprPrec := Phenomena.Comparison.Wellwood2015.instReprDimensionReversalDatum.repr }

def Phenomena.Comparison.Wellwood2015.hotterDatum : DimensionReversalDatum

(82a): "This coffee is hotter than that coffee is." — TEMPERATURE, *VOLUME. GA measuring states → intensive.

Equations

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

def Phenomena.Comparison.Wellwood2015.harderDatum : DimensionReversalDatum

(82b): "This plastic is harder than that plastic is." — HARDNESS, *WEIGHT. GA measuring states → intensive.

Equations

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

def Phenomena.Comparison.Wellwood2015.moreCoffeeDatum : DimensionReversalDatum

(83a): "Al has more coffee than Bill does." — *TEMPERATURE, VOLUME. Mass noun measuring entities → extensive.

Equations

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

def Phenomena.Comparison.Wellwood2015.morePlasticDatum : DimensionReversalDatum

(83b): "Al has more plastic than Bill does." — *HARDNESS, WEIGHT. Mass noun measuring entities → extensive.

Equations

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

def Phenomena.Comparison.Wellwood2015.fullerDatum : DimensionReversalDatum

(84a): "This glass is fuller than that glass is." — *TEMPERATURE, VOLUME. GA measuring entities (via container contents) → extensive. Reversal: GA but extensive, because measured domain is entity.

Equations

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

def Phenomena.Comparison.Wellwood2015.heavierDatum : DimensionReversalDatum

(84b): "This plastic is heavier than that plastic is." — *HARDNESS, WEIGHT. GA measuring entities → extensive. Reversal: GA but extensive, because measured domain is entity.

Equations

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

def Phenomena.Comparison.Wellwood2015.moreHeatDatum : DimensionReversalDatum

(85a): "This rock has more heat than that one does." — TEMPERATURE, *VOLUME. Mass noun measuring states → intensive. Reversal: noun but intensive, because measured domain is state.

Equations

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

def Phenomena.Comparison.Wellwood2015.moreFirmnessDatum : DimensionReversalDatum

(85b): "This mattress has more firmness than that one does." — HARDNESS, *WEIGHT. Mass noun measuring states → intensive. Reversal: noun but intensive, because measured domain is state.

Equations

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

def Phenomena.Comparison.Wellwood2015.spedUpMoreDatum : DimensionReversalDatum

(89a): "Al sped up more than Peter did." — SPEED, *DISTANCE. Atelic VP measuring states (speed) → intensive. Reversal: verb but intensive, because measured domain is state.

Equations

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

def Phenomena.Comparison.Wellwood2015.droveMoreDatum : DimensionReversalDatum

(87a): "Al drove more than Peter did." — *SPEED, DISTANCE. Atelic VP measuring events → extensive.

Equations

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

def Phenomena.Comparison.Wellwood2015.dimensionReversalData : List DimensionReversalDatum

All dimension reversal data from §3.4.

Equations

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

structure Phenomena.Comparison.Wellwood2015.StateModificationDatum : Type

State modification datum: an adjective with a modifier that applies to the state argument, illustrating that states (like events) support predicate modification via conjunction (§3.2, p. 81; §3.5, p. 88).

"happy in the morning" = ∃s. happy(s) ∧ Holder(x, s) ∧ in-the-morning(s)

This parallels Davidson's event modification: states are eventualities of sort .state, so EventModifier applies to them.

• adjective : String
• modifier : String
• form : String

  Full modified form

instance Phenomena.Comparison.Wellwood2015.instReprStateModificationDatum : Repr StateModificationDatum

Equations

• Phenomena.Comparison.Wellwood2015.instReprStateModificationDatum = { reprPrec := Phenomena.Comparison.Wellwood2015.instReprStateModificationDatum.repr }

def Phenomena.Comparison.Wellwood2015.instReprStateModificationDatum.repr : StateModificationDatum → ℕ → Std.Format

Equations

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

def Phenomena.Comparison.Wellwood2015.happyMorningDatum : StateModificationDatum

"happy in the morning" — temporal modifier on a state (§3.5).

Equations

• Phenomena.Comparison.Wellwood2015.happyMorningDatum = { adjective := "happy", modifier := "in the morning", form := "happy in the morning" }

def Phenomena.Comparison.Wellwood2015.patientPlaygroundDatum : StateModificationDatum

"patient with Mary on the playground" — multiple modifiers on a state (§3.5).

Equations

• Phenomena.Comparison.Wellwood2015.patientPlaygroundDatum = { adjective := "patient", modifier := "with Mary on the playground", form := "patient with Mary on the playground" }

def Phenomena.Comparison.Wellwood2015.lexCatToStatus : LexCat → Semantics.Lexical.Measurement.MereologicalStatus

Map LexCat to MereologicalStatus using the theory's bridges.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Comparison.Wellwood2015.lexCatToStatus Phenomena.Comparison.Wellwood2015.LexCat.gradableAdj = Semantics.Lexical.Measurement.gradableToStatus
• Phenomena.Comparison.Wellwood2015.lexCatToStatus Phenomena.Comparison.Wellwood2015.LexCat.nonGradableAdj = Semantics.Lexical.Measurement.nonGradableToStatus

def Phenomena.Comparison.Wellwood2015.statusPredictsFelicitous : Semantics.Lexical.Measurement.MereologicalStatus → Bool

The theory predicts: cumulative → felicitous with much.

Equations

• Phenomena.Comparison.Wellwood2015.statusPredictsFelicitous Semantics.Lexical.Measurement.MereologicalStatus.cumulative = true
• Phenomena.Comparison.Wellwood2015.statusPredictsFelicitous Semantics.Lexical.Measurement.MereologicalStatus.quantized = false

theorem Phenomena.Comparison.Wellwood2015.massNoun_felicity : statusPredictsFelicitous (lexCatToStatus LexCat.massNoun) = massNounDatum.felicitousWithMuch

theorem Phenomena.Comparison.Wellwood2015.countNoun_felicity : statusPredictsFelicitous (lexCatToStatus LexCat.countNoun) = countNounDatum.felicitousWithMuch

theorem Phenomena.Comparison.Wellwood2015.atelicVP_felicity : statusPredictsFelicitous (lexCatToStatus LexCat.atelicVP) = atelicVPDatum.felicitousWithMuch

theorem Phenomena.Comparison.Wellwood2015.telicVP_felicity : statusPredictsFelicitous (lexCatToStatus LexCat.telicVP) = telicVPDatum.felicitousWithMuch

theorem Phenomena.Comparison.Wellwood2015.gradableAdj_felicity : statusPredictsFelicitous (lexCatToStatus LexCat.gradableAdj) = gradableAdjDatum.felicitousWithMuch

theorem Phenomena.Comparison.Wellwood2015.nonGradableAdj_felicity : statusPredictsFelicitous (lexCatToStatus LexCat.nonGradableAdj) = nonGradableAdjDatum.felicitousWithMuch

theorem Phenomena.Comparison.Wellwood2015.massNoun_atelicVP_same_status : lexCatToStatus LexCat.massNoun = lexCatToStatus LexCat.atelicVP

theorem Phenomena.Comparison.Wellwood2015.countNoun_telicVP_same_status : lexCatToStatus LexCat.countNoun = lexCatToStatus LexCat.telicVP

theorem Phenomena.Comparison.Wellwood2015.gradableAdj_patterns_with_cum : lexCatToStatus LexCat.gradableAdj = lexCatToStatus LexCat.massNoun

theorem Phenomena.Comparison.Wellwood2015.nonGradableAdj_patterns_with_qua : lexCatToStatus LexCat.nonGradableAdj = lexCatToStatus LexCat.countNoun

theorem Phenomena.Comparison.Wellwood2015.run_shift_via_telicize : have p := Semantics.Tense.Aspect.LexicalAspect.activityProfile; Semantics.Lexical.Measurement.telicityToStatus p.telicity = Semantics.Lexical.Measurement.MereologicalStatus.cumulative ∧ Semantics.Lexical.Measurement.telicityToStatus p.telicize.telicity = Semantics.Lexical.Measurement.MereologicalStatus.quantized

theorem Phenomena.Comparison.Wellwood2015.build_shift_via_atelicize : have p := Semantics.Tense.Aspect.LexicalAspect.accomplishmentProfile; Semantics.Lexical.Measurement.telicityToStatus p.telicity = Semantics.Lexical.Measurement.MereologicalStatus.quantized ∧ Semantics.Lexical.Measurement.telicityToStatus p.atelicize.telicity = Semantics.Lexical.Measurement.MereologicalStatus.cumulative

theorem Phenomena.Comparison.Wellwood2015.rock_shift_status : lexCatToStatus LexCat.massNoun = Semantics.Lexical.Measurement.MereologicalStatus.cumulative ∧ lexCatToStatus LexCat.countNoun = Semantics.Lexical.Measurement.MereologicalStatus.quantized

theorem Phenomena.Comparison.Wellwood2015.massNoun_open_scale : (lexCatToStatus LexCat.massNoun).toBoundedness = Core.Scale.Boundedness.open_

theorem Phenomena.Comparison.Wellwood2015.countNoun_closed_scale : (lexCatToStatus LexCat.countNoun).toBoundedness = Core.Scale.Boundedness.closed

theorem Phenomena.Comparison.Wellwood2015.atelicVP_open_scale : (lexCatToStatus LexCat.atelicVP).toBoundedness = Core.Scale.Boundedness.open_

theorem Phenomena.Comparison.Wellwood2015.telicVP_closed_scale : (lexCatToStatus LexCat.telicVP).toBoundedness = Core.Scale.Boundedness.closed

def Phenomena.Comparison.Wellwood2015.measuredDomainRestricted : MeasuredDomain → Bool

Equations

• Phenomena.Comparison.Wellwood2015.measuredDomainRestricted Phenomena.Comparison.Wellwood2015.MeasuredDomain.state = true
• Phenomena.Comparison.Wellwood2015.measuredDomainRestricted Phenomena.Comparison.Wellwood2015.MeasuredDomain.entity = false
• Phenomena.Comparison.Wellwood2015.measuredDomainRestricted Phenomena.Comparison.Wellwood2015.MeasuredDomain.event = false

theorem Phenomena.Comparison.Wellwood2015.hotter_restricted : measuredDomainRestricted hotterDatum.measuredDomain = hotterDatum.intensive

theorem Phenomena.Comparison.Wellwood2015.harder_restricted : measuredDomainRestricted harderDatum.measuredDomain = harderDatum.intensive

theorem Phenomena.Comparison.Wellwood2015.moreCoffee_not_restricted : measuredDomainRestricted moreCoffeeDatum.measuredDomain = moreCoffeeDatum.intensive

theorem Phenomena.Comparison.Wellwood2015.morePlastic_not_restricted : measuredDomainRestricted morePlasticDatum.measuredDomain = morePlasticDatum.intensive

theorem Phenomena.Comparison.Wellwood2015.fuller_not_restricted : measuredDomainRestricted fullerDatum.measuredDomain = fullerDatum.intensive

theorem Phenomena.Comparison.Wellwood2015.heavier_not_restricted : measuredDomainRestricted heavierDatum.measuredDomain = heavierDatum.intensive

theorem Phenomena.Comparison.Wellwood2015.moreHeat_restricted : measuredDomainRestricted moreHeatDatum.measuredDomain = moreHeatDatum.intensive

theorem Phenomena.Comparison.Wellwood2015.moreFirmness_restricted : measuredDomainRestricted moreFirmnessDatum.measuredDomain = moreFirmnessDatum.intensive

theorem Phenomena.Comparison.Wellwood2015.spedUpMore_restricted : measuredDomainRestricted spedUpMoreDatum.measuredDomain = spedUpMoreDatum.intensive

theorem Phenomena.Comparison.Wellwood2015.droveMore_not_restricted : measuredDomainRestricted droveMoreDatum.measuredDomain = droveMoreDatum.intensive

theorem Phenomena.Comparison.Wellwood2015.state_mod_pm_bridge {Entity : Type u_1} {Time : Type u_2} [LE Time] (P : Semantics.Events.EvPred Time) (frame : Semantics.Events.ThematicRoles.ThematicFrame Entity Time) (x : Entity) (M : Semantics.Events.ThematicRoles.EventModifier Time) : Semantics.Events.ThematicRoles.modifiedStativeLogicalForm P frame x M ↔ Semantics.Events.ThematicRoles.stativeLogicalForm (Semantics.Events.ThematicRoles.modify P M) frame x