Kennedy 1999: Projecting the Adjective

@cite{kennedy-1999} @cite{bresnan-1973} @cite{bhatt-pancheva-2004} @cite{kennedy-2007} @cite{lechner-2004} @cite{rett-2020} @cite{schwarzschild-2008}

@cite{kennedy-1999} "Projecting the Adjective" (dissertation, UC Santa Cruz; published 1999, Garland). The foundational argument that gradable adjectives denote measure functions (Entity → Degree), with degree morphemes (-er, as, -est, too, enough) as functional heads of a DegP projection that bind the degree argument.

Core Contributions

1. Adjectives as measure functions: ⟦tall⟧ = λx. height(x), not λd.λx. height(x) ≥ d. The relational type ⟨d,⟨e,t⟩⟩ is derived by combining with degree morphology, not lexical.

2. Extent functions: pos-ext and neg-ext partition the scale into degrees an entity "has" and "lacks". Negative adjectives access the negative extent of the same scale as their positive counterpart.

3. Cross-polar anomaly: "Kim is as tall as Lee is short" is anomalous because the equative tries to compare a positive extent with a negative extent — structurally incompatible (proved always-false in Core.Scale.crossExtent_always_false).

4. Antonymy biconditional: "BK is longer than The Idiot iff The Idiot is shorter than BK" is DERIVED from extent complementarity, not stipulated as a lexical property (proved in Core.Scale.antonymy_biconditional).

5. DegP projection: Degree morphemes head their own syntactic phrase. This has been refined by @cite{heim-2001} (sentential operator approach) and subsequent work. The core insight — that degree binding is syntactic, not lexical — is consensus.

6. Comparative subdeletion: "The table is longer than it is wide" requires clausal standards and cross-dimensional commensurability.

What Is Current vs. Historical

The measure function denotation and extent functions (§ 1–4) are current consensus — they underlie all subsequent degree-semantic work including @cite{kennedy-2007} and @cite{schwarzschild-2008}.

The specific DegP syntax (§ 5) has been refined: @cite{heim-2001}'s sentential operator approach is now co-standard, and the two make different scope predictions. This study file records both the data and the 1999-era analysis.

Additional Data

This file also collects comparison construction data from @cite{bresnan-1973} (phrasal/clausal comparatives, morphological distribution), @cite{bhatt-pancheva-2004} and @cite{lechner-2004} (subcomparatives), and @cite{kennedy-2007} and @cite{rett-2020} (equative constructions).

structure Phenomena.Comparison.Studies.Kennedy1999.CrossPolarDatum : Type

A cross-polar anomaly judgment.

• sentence : String
• acceptable : Bool
• samePolarity : Bool

  Does this compare same-polarity or cross-polarity extents?

• isEquative : Bool

  Is this an equative ("as...as") or comparative ("-er...than")?

• note : String

def Phenomena.Comparison.Studies.Kennedy1999.instReprCrossPolarDatum.repr : CrossPolarDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Kennedy1999.instReprCrossPolarDatum : Repr CrossPolarDatum

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instReprCrossPolarDatum = { reprPrec := Phenomena.Comparison.Studies.Kennedy1999.instReprCrossPolarDatum.repr }

def Phenomena.Comparison.Studies.Kennedy1999.crossPolarData : List CrossPolarDatum

Cross-polar anomaly data from @cite{kennedy-1999}.

Equations

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

theorem Phenomena.Comparison.Studies.Kennedy1999.crossPolar_iff_unacceptable_equative (d : CrossPolarDatum) : d ∈ crossPolarData → d.isEquative = true → (d.acceptable = false ↔ d.samePolarity = false)

Among equatives, cross-polar = unacceptable. The comparative rescues cross-polar because -er compares degrees, not extents.

theorem Phenomena.Comparison.Studies.Kennedy1999.crossPolar_predicted {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (kim lee : Entity) : ¬Core.Scale.crossExtentInclusion μ kim lee

The cross-polar anomaly is predicted by extent function algebra: cross-extent inclusion is always false on any linear order. This is the formal content behind the unacceptability of "Kim is as tall as Lee is short".

theorem Phenomena.Comparison.Studies.Kennedy1999.samePolar_equative_welldefined {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Semantics.Degree.Comparative.equativeViaExtent μ a b ↔ μ a ≥ μ b

Same-polarity equatives are well-defined: "as tall as" checks that the standard's positive extent is included in the subject's. This reduces to μ(subject) ≥ μ(standard).

theorem Phenomena.Comparison.Studies.Kennedy1999.equative_extent_eq_literal {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Semantics.Degree.Comparative.equativeViaExtent μ a b ↔ Semantics.Degree.Equative.equativeLiteral μ a b

Bridge: the extent-based equative (equativeViaExtent, defined via posExt inclusion) and the direct equative (equativeLiteral, defined as μ(a) ≥ μ(b)) are equivalent. This connects Kennedy's algebraic formulation to the standard point-comparison semantics.

theorem Phenomena.Comparison.Studies.Kennedy1999.comparative_extent_bridge {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Semantics.Degree.Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.positive ↔ Core.Scale.posExt μ b ⊂ Core.Scale.posExt μ a

"A is taller than B" iff B's positive extent is strictly contained in A's. Bridges the consensus comparative to the algebraic posExt_ssubset_iff from Core.Scale.

theorem Phenomena.Comparison.Studies.Kennedy1999.antonymy_derived {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Semantics.Degree.Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.positive ↔ Core.Scale.negExt μ a ⊂ Core.Scale.negExt μ b

Central theorem of @cite{kennedy-1999} Ch. 3: antonymy equivalence is DERIVED from the complementarity of positive and negative extents, not stipulated as a lexical property.

"BK is longer than The Idiot" iff "The Idiot is shorter than BK"

Formally: posExt(b) ⊂ posExt(a) ↔ negExt(a) ⊂ negExt(b). The positive comparative and the negative comparative have the same truth conditions because positive and negative extents are complementary projections of the same scale point.

theorem Phenomena.Comparison.Studies.Kennedy1999.equative_antonymy_extent {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Semantics.Degree.Comparative.equativeViaExtent μ a b ↔ Core.Scale.negExt μ a ⊆ Core.Scale.negExt μ b

The antonymy biconditional also holds for equatives: "A is as tall as B" iff "B is as short as A" — extent inclusion in one polarity implies extent inclusion in the other.

structure Phenomena.Comparison.Studies.Kennedy1999.HistoricalDegP : Type

@cite{kennedy-1999}'s DegP projection: degree morphemes are functional heads taking AdjP as complement.

[DegP [Deg° -er, as, -est, too, enough] [AdjP tall]]

This specific syntactic structure was refined by @cite{heim-2001}, who treats -er as a sentential operator rather than a DegP head. Both agree that degree binding is syntactic.

Note: the degree head inventory matches Semantics.Degree.DegPType from Degree/Core.lean, which is the current consensus enumeration. This historical structure records Kennedy's specific proposal that these heads project a full DegP phrase.

• head : Semantics.Degree.DegPType
• adjective : String

def Phenomena.Comparison.Studies.Kennedy1999.instReprHistoricalDegP.repr : HistoricalDegP → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Kennedy1999.instReprHistoricalDegP : Repr HistoricalDegP

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instReprHistoricalDegP = { reprPrec := Phenomena.Comparison.Studies.Kennedy1999.instReprHistoricalDegP.repr }

def Phenomena.Comparison.Studies.Kennedy1999.exampleDegPs : List HistoricalDegP

Example DegP constructions from @cite{kennedy-1999}.

Equations

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

structure Phenomena.Comparison.Studies.Kennedy1999.MeasurePhraseDatum : Type

@cite{kennedy-1999} §3.1.8 observes that measure phrases are acceptable with positive adjectives but not negative ones:

(69) "My Cadillac is 8 feet long." ✓ (70) "#My Fiat is 5 feet short." ✗

Kennedy's explanation: measure phrases denote bounded extents. On scales with a minimum, positive extents are bounded (anchored at ⊥), but negative extents are not (they extend to ∞). So the ordering relation between a measure phrase (bounded extent) and a negative extent is undefined.

• sentence : String
• acceptable : Bool
• isPositiveAdj : Bool

def Phenomena.Comparison.Studies.Kennedy1999.instReprMeasurePhraseDatum.repr : MeasurePhraseDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Kennedy1999.instReprMeasurePhraseDatum : Repr MeasurePhraseDatum

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instReprMeasurePhraseDatum = { reprPrec := Phenomena.Comparison.Studies.Kennedy1999.instReprMeasurePhraseDatum.repr }

def Phenomena.Comparison.Studies.Kennedy1999.measurePhraseData : List MeasurePhraseDatum

Equations

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

theorem Phenomena.Comparison.Studies.Kennedy1999.measurePhrase_positive_only (d : MeasurePhraseDatum) : d ∈ measurePhraseData → (d.acceptable = true ↔ d.isPositiveAdj = true)

Measure phrases are acceptable with positive adjectives only.

structure Phenomena.Comparison.Studies.Kennedy1999.ComparativeJudgment : Type

An acceptability judgment for a comparative construction. @cite{bresnan-1973} @cite{kennedy-1999} @cite{lechner-2004}

• sentence : String

  The example sentence

• acceptable : Bool

  Whether the sentence is acceptable

• standardType : String

  Phrasal or clausal standard?

• note : String

  Notes on the reading or restriction

def Phenomena.Comparison.Studies.Kennedy1999.instReprComparativeJudgment.repr : ComparativeJudgment → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Kennedy1999.instReprComparativeJudgment : Repr ComparativeJudgment

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instReprComparativeJudgment = { reprPrec := Phenomena.Comparison.Studies.Kennedy1999.instReprComparativeJudgment.repr }

def Phenomena.Comparison.Studies.Kennedy1999.phrasalExamples : List ComparativeJudgment

Phrasal comparatives — DP complement of than.

Equations

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

def Phenomena.Comparison.Studies.Kennedy1999.clausalExamples : List ComparativeJudgment

Clausal comparatives — CP complement of than.

Equations

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

structure Phenomena.Comparison.Studies.Kennedy1999.MorphDistributionDatum : Type

Synthetic vs. analytic comparative distribution in English. The generalization: monosyllabic adjectives prefer synthetic (-er), polysyllabic prefer analytic (more), disyllabic varies.

• adjective : String
• syllables : ℕ
• syntheticOk : Bool
• analyticOk : Bool

def Phenomena.Comparison.Studies.Kennedy1999.instReprMorphDistributionDatum.repr : MorphDistributionDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Kennedy1999.instReprMorphDistributionDatum : Repr MorphDistributionDatum

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instReprMorphDistributionDatum = { reprPrec := Phenomena.Comparison.Studies.Kennedy1999.instReprMorphDistributionDatum.repr }

def Phenomena.Comparison.Studies.Kennedy1999.morphDistribution : List MorphDistributionDatum

Equations

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

structure Phenomena.Comparison.Studies.Kennedy1999.BareComparativeDatum : Type

Bare comparative data: the standard of comparison may be implicitly recovered from context.

"Kim is taller" — standard = contextually supplied comparison class. This connects to the evaluative/positive reading of bare gradable adjectives (Gradability/).

Note: "bare comparative" = comparative without an explicit standard. This is NOT "comparative deletion" in @cite{bresnan-1973}'s sense (= identity-based deletion of a clause constituent from the than-clause).

• sentence : String
• explicitStandard : Bool

  Is the standard explicitly present?

• readings : List String

  Available readings

def Phenomena.Comparison.Studies.Kennedy1999.instReprBareComparativeDatum.repr : BareComparativeDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Kennedy1999.instReprBareComparativeDatum : Repr BareComparativeDatum

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instReprBareComparativeDatum = { reprPrec := Phenomena.Comparison.Studies.Kennedy1999.instReprBareComparativeDatum.repr }

def Phenomena.Comparison.Studies.Kennedy1999.bareComparativeExamples : List BareComparativeDatum

Equations

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

structure Phenomena.Comparison.Studies.Kennedy1999.SubcomparativeDatum : Type

A subcomparative judgment. @cite{bhatt-pancheva-2004} @cite{kennedy-1999} @cite{lechner-2004} @cite{schwarzschild-2008}

• sentence : String
• acceptable : Bool
• matrixPredicate : String

  The matrix predicate (e.g., "long")

• embeddedPredicate : String

  The embedded predicate (e.g., "wide")

• commensurable : Bool

  Are the dimensions commensurable?

def Phenomena.Comparison.Studies.Kennedy1999.instReprSubcomparativeDatum.repr : SubcomparativeDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Kennedy1999.instReprSubcomparativeDatum : Repr SubcomparativeDatum

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instReprSubcomparativeDatum = { reprPrec := Phenomena.Comparison.Studies.Kennedy1999.instReprSubcomparativeDatum.repr }

def Phenomena.Comparison.Studies.Kennedy1999.subcomparativeExamples : List SubcomparativeDatum

Equations

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

structure Phenomena.Comparison.Studies.Kennedy1999.SubcomparativeTypologyDatum : Type

Cross-linguistic variation in subcomparative availability. @cite{bhatt-pancheva-2004}

• language : String
• available : Bool
• note : String

def Phenomena.Comparison.Studies.Kennedy1999.instReprSubcomparativeTypologyDatum.repr : SubcomparativeTypologyDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Kennedy1999.instReprSubcomparativeTypologyDatum : Repr SubcomparativeTypologyDatum

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instReprSubcomparativeTypologyDatum = { reprPrec := Phenomena.Comparison.Studies.Kennedy1999.instReprSubcomparativeTypologyDatum.repr }

def Phenomena.Comparison.Studies.Kennedy1999.subcomparativeTypology : List SubcomparativeTypologyDatum

Equations

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

structure Phenomena.Comparison.Studies.Kennedy1999.EquativeJudgment : Type

An equative judgment. @cite{kennedy-2007} @cite{rett-2020}

• sentence : String
• acceptable : Bool
• availableReadings : List String

  "at_least" or "exactly"

• note : String

def Phenomena.Comparison.Studies.Kennedy1999.instReprEquativeJudgment.repr : EquativeJudgment → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Kennedy1999.instReprEquativeJudgment : Repr EquativeJudgment

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instReprEquativeJudgment = { reprPrec := Phenomena.Comparison.Studies.Kennedy1999.instReprEquativeJudgment.repr }

def Phenomena.Comparison.Studies.Kennedy1999.equativeExamples : List EquativeJudgment

Equations

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

inductive Phenomena.Comparison.Studies.Kennedy1999.EquativeStrategy : Type

Equative encoding strategy. @cite{rett-2020}

• parameterMarker : EquativeStrategy
• reach : EquativeStrategy
• similative : EquativeStrategy
• exceed : EquativeStrategy

instance Phenomena.Comparison.Studies.Kennedy1999.instDecidableEqEquativeStrategy : DecidableEq EquativeStrategy

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instDecidableEqEquativeStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Comparison.Studies.Kennedy1999.instBEqEquativeStrategy : BEq EquativeStrategy

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instBEqEquativeStrategy = { beq := Phenomena.Comparison.Studies.Kennedy1999.instBEqEquativeStrategy.beq }

def Phenomena.Comparison.Studies.Kennedy1999.instBEqEquativeStrategy.beq : EquativeStrategy → EquativeStrategy → Bool

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instBEqEquativeStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Comparison.Studies.Kennedy1999.instReprEquativeStrategy.repr : EquativeStrategy → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Kennedy1999.instReprEquativeStrategy : Repr EquativeStrategy

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instReprEquativeStrategy = { reprPrec := Phenomena.Comparison.Studies.Kennedy1999.instReprEquativeStrategy.repr }

structure Phenomena.Comparison.Studies.Kennedy1999.EquativeTypologyDatum : Type

Cross-linguistic equative strategy datum.

• language : String
• strategy : EquativeStrategy
• exampleForm : String

instance Phenomena.Comparison.Studies.Kennedy1999.instReprEquativeTypologyDatum : Repr EquativeTypologyDatum

Equations

• Phenomena.Comparison.Studies.Kennedy1999.instReprEquativeTypologyDatum = { reprPrec := Phenomena.Comparison.Studies.Kennedy1999.instReprEquativeTypologyDatum.repr }

def Phenomena.Comparison.Studies.Kennedy1999.instReprEquativeTypologyDatum.repr : EquativeTypologyDatum → ℕ → Std.Format

Equations

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

def Phenomena.Comparison.Studies.Kennedy1999.equativeTypology : List EquativeTypologyDatum

Equations

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