Kennedy 1999: Projecting the Adjective

Study file for [Ken99], the dissertation arguing that gradable adjectives denote measure functions (⟦tall⟧ = λx. height(x)) whose relational ⟨d,⟨e,t⟩⟩ type is derived by degree morphology, and that positive and negative extents of the same scale (POSδ and NEGδ, eqs (30)–(31)) derive antonymy and cross-polar anomaly rather than stipulating them. The extent algebra is formalised in Semantics/Degree/Basic.lean: extents are Set.Iic (μ x) / Set.Ioi (μ x), comparison is extent inclusion (Degree.comparative_iff_Iic_ssubset), the antonymy biconditional (54) is Degree.antonymy_biconditional, and cross-polar anomaly (§3.1.7) is Degree.not_crossExtentInclusion. The embedding of measure functions into [Kle80]'s rival degree-free delineation semantics is in Semantics/Degree/Hom.lean (Degree.delineation_strictly_more_general).

The judgment data live in Data/Examples/Kennedy1999.json: the cross-polar and incommensurability comparatives of §3.1.3–§3.1.7 (including the ficus quadruple (61)–(64) showing the anomaly generalizes beyond antonym pairs) and the measure-phrase restriction of §3.1.8–§3.1.9. Kennedy's account defines comparison exactly when the compared extents are of the same sort on a shared scale; comparison_defined_iff and measurePhrase_positive_iff check the predicted judgment patterns row by row.

Cross-polar anomaly (§3.1.3–§3.1.7)

def Kennedy1999.samePolarity (e : Data.Examples.LinguisticExample) : Prop

The two compared adjectives have the same scale polarity.

Equations

• Kennedy1999.samePolarity e = (e.feature? "matrix_polarity" = e.feature? "standard_polarity")

@[instance_reducible]

instance Kennedy1999.instDecidableSamePolarity (e : Data.Examples.LinguisticExample) : Decidable (samePolarity e)

Equations

• Kennedy1999.instDecidableSamePolarity e = Kennedy1999.instDecidableSamePolarity._aux_1 e

def Kennedy1999.sharedScale (e : Data.Examples.LinguisticExample) : Prop

The two compared adjectives project onto a shared scale.

Equations

• Kennedy1999.sharedScale e = (e.feature? "shared_scale" = some "true")

@[instance_reducible]

instance Kennedy1999.instDecidableSharedScale (e : Data.Examples.LinguisticExample) : Decidable (sharedScale e)

Equations

• Kennedy1999.instDecidableSharedScale e = Kennedy1999.instDecidableSharedScale._aux_1 e

def Kennedy1999.crossPolarRows : List Data.Examples.LinguisticExample

The subdeletion comparatives of §3.1.3–§3.1.7: cross-polar anomalies, same-polarity controls, the ficus quadruple, and the incommensurability cases.

Equations

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

theorem Kennedy1999.comparison_defined_iff (e : Data.Examples.LinguisticExample) : e ∈ crossPolarRows → (e.judgment = Features.Judgment.acceptable ↔ samePolarity e ∧ sharedScale e)

A subdeletion comparative is acceptable exactly when the compared extents are of the same sort on a shared scale — sortal cross-polar anomaly and incommensurability under one condition. Degree.not_crossExtentInclusion is the lattice-algebraic shadow of the polarity half.

Measure phrase distribution (§3.1.8–§3.1.9)

Measure phrases denote bounded extents. On a scale with a minimum, positive extents are bounded but negative extents are not, so an absolute construction composing a measure phrase with a negative adjective is undefined — (69) "My Cadillac is 8 feet long" vs (70) "#My Fiat is 5 feet short". The phrasal comparative (73) "My fiat is shorter than 8 feet" is the paper's contrast: there the standard is derived by applying the adjective to the measure phrase.

def Kennedy1999.measurePhraseAbsoluteRows : List Data.Examples.LinguisticExample

The absolute measure-phrase constructions of §3.1.8–§3.1.9.

Equations

• Kennedy1999.measurePhraseAbsoluteRows = [Kennedy1999.Examples.mp_cadillac, Kennedy1999.Examples.mp_fiat, Kennedy1999.Examples.mp_reich, Kennedy1999.Examples.mp_slow]

theorem Kennedy1999.measurePhrase_positive_iff (e : Data.Examples.LinguisticExample) : e ∈ measurePhraseAbsoluteRows → (e.judgment = Features.Judgment.acceptable ↔ e.feature? "polarity" = some "positive")

An absolute measure-phrase construction is acceptable exactly with a positive adjective, whose extents are bounded.

DegP projection

Degree morphemes are functional heads taking AdjP as complement: [DegP [Deg° -er, as, -est, too, enough] [AdjP tall]] (ch. 2, the extended projection of A). The head inventory is Degree.Head.

structure Kennedy1999.HistoricalDegP : Type

A degree head with its adjective complement.

• head : Degree.Head
• adjective : String

def Kennedy1999.instReprHistoricalDegP.repr : HistoricalDegP → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Kennedy1999.instReprHistoricalDegP : Repr HistoricalDegP

Equations

• Kennedy1999.instReprHistoricalDegP = { reprPrec := Kennedy1999.instReprHistoricalDegP.repr }

def Kennedy1999.exampleDegPs : List HistoricalDegP

DegP constructions from the paper.

Equations

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