Kennedy 2007: Relative vs Absolute Gradable Adjectives

Study of [Ken07] ("Vagueness and grammar"), grounding the paper's central claims against the degree substrate and the English adjective Fragment. [KMcN05] [RW04b]

1. Scale structure fixes the standard. Interpretive Economy ([Ken07] eq. (66)) derives a contextual standard for open scales and an endpoint standard for closed ones, building on the scale typology of [KMcN05] and [RW04b]. A totally closed scale is interpretively variable: both endpoint standards are admitted (eq. (67)–(68), opaque/transparent, open/exposed), with the maximum a mere out-of-context pragmatic default.

2. The relative/absolute split surfaces in comparatives. Comparatives with absolute adjectives carry an entailment to the bare positive form whose direction is fixed by the standard type — minimum-standard absolutes (wet, bent) give a positive entailment (eq. (49)), maximum-standard absolutes (dry, straight) a negative one (eq. (50)) — whereas relative adjectives (long, tall) carry neither (eq. (51)–(52)).

3. Scale structure licenses degree modifiers. [Ken07] eq. (61) (= [KMcN05] eq. (15)): maximizers/proportional modifiers (completely, half) require an upper endpoint, minimizers/diminishers (slightly) a lower one. The Licenses matrix encodes this, and the bridges below check it against the English Fragment entries (tall, full, wet, dry) and the LicensingPipeline substrate.

Main results

• closed_admits_both_endpoints — totally closed scales are interpretively variable.
• minStandard_comparative_entails_positive / maxStandard_comparative_entails_negative / relative_comparative_not_entails_positive — the eq. (49)–(52) asymmetry.
• Licenses — the eq. (61) modifier-class licensing matrix.
• k2007_matrix_agrees_with_typology, k2007_modifier_data_agrees, pipeline_agrees_with_measure — the matrix agrees with the per-adjective typology data and with the DirectedMeasure / LicensingPipeline substrate.
• tall_requires_cc, full_no_cc (etc.) — comparison-class sensitivity read off each Fragment adjective's scale structure.

Scale structure and Interpretive Economy

[Ken07]'s generalisation: open scales take a contextual standard, closed scales an endpoint standard. The content beyond the substrate's default table is the interpretive variability of totally closed scales.

theorem Kennedy2007.open_requires_comparison_class : (Degree.interpretiveEconomy Core.Order.Boundedness.open_).RequiresComparisonClass

Open-scale (relative) adjectives — tall, expensive, big — take a contextual standard, so their interpretation requires a comparison class.

theorem Kennedy2007.closed_admits_both_endpoints : Degree.ieAdmits Core.Order.Boundedness.closed Degree.PositiveStandard.minEndpoint ∧ Degree.ieAdmits Core.Order.Boundedness.closed Degree.PositiveStandard.maxEndpoint

Totally closed scales are interpretively variable: Interpretive Economy admits both the minimum and the maximum endpoint standard ([Ken07] eq. (67)–(68), opaque/transparent, open/exposed). The substrate's single-valued interpretiveEconomy .closed = .maxEndpoint is only the out-of-context pragmatic default, not an IE determination.

Relative vs absolute adjectives in comparatives

[Ken07] eq. (49)–(52): the standard type of an absolute adjective surfaces as an entailment from the comparative to the bare positive form. On a scale D, a minimum-standard absolute (wet) is positive iff its degree is above the scale bottom (PositiveStandard.minEndpoint), a maximum-standard absolute (dry) iff its degree is the scale top (PositiveStandard.maxEndpoint), and a relative adjective (long) iff its degree exceeds a contextual threshold (PositiveStandard.contextual).

def Kennedy2007.MinStandardPos {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [OrderBot D] (μ : Entity → D) (x : Entity) : Prop

Positive form of a minimum-standard absolute adjective: x is wet iff its degree is strictly above the scale minimum.

Equations

• Kennedy2007.MinStandardPos μ x = (⊥ < μ x)

def Kennedy2007.MaxStandardPos {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [OrderTop D] (μ : Entity → D) (x : Entity) : Prop

Positive form of a maximum-standard absolute adjective: x is dry iff its degree is the scale maximum.

Equations

• Kennedy2007.MaxStandardPos μ x = (μ x = ⊤)

def Kennedy2007.RelativePos {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (θ : D) (x : Entity) : Prop

Positive form of a relative adjective: x is long iff its degree exceeds the contextual threshold θ.

Equations

• Kennedy2007.RelativePos μ θ x = (θ < μ x)

theorem Kennedy2007.minStandard_comparative_entails_positive {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [OrderBot D] (μ : Entity → D) (a b : Entity) (h : Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive) : MinStandardPos μ a

Eq. (49): minimum-standard positive entailment. "The floor is wetter than the countertop" entails "the floor is wet": exceeding another degree puts you strictly above the scale minimum.

theorem Kennedy2007.maxStandard_comparative_entails_negative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [OrderTop D] (μ : Entity → D) (a b : Entity) (h : Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive) : ¬MaxStandardPos μ b

Eq. (50): maximum-standard negative entailment. "The floor is drier than the countertop" entails "the countertop is not dry": being exceeded keeps you strictly below the scale maximum.

Relative adjectives carry no entailment from the comparative to the positive form ([Ken07] eq. (51)–(52)): "Rod A is longer than Rod B" entails neither that A is long nor that B is not long, because the standard is contextual. Non-entailment is witnessed by concrete ℕ-valued models in which the comparative holds but the positive form goes either way.

theorem Kennedy2007.relative_comparative_not_entails_positive : ∃ (μ : Bool → ℕ) (θ : ℕ) (a : Bool) (b : Bool), Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive ∧ ¬RelativePos μ θ a

"Longer than" does not entail "long": a model where a exceeds b yet a falls below the contextual threshold.

theorem Kennedy2007.relative_comparative_not_entails_negative : ∃ (μ : Bool → ℕ) (θ : ℕ) (a : Bool) (b : Bool), Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive ∧ RelativePos μ θ a

"Longer than" does not entail "not long" either: a model where a exceeds b and is also above the threshold. Together with the previous theorem this shows the comparative leaves a relative adjective's positive form undetermined.

Concrete entailment witnesses

The general entailments fire on the paper's scenarios, here on a 0–3 scale (Fin 4, with ⊥ = 0 and ⊤ = 3).

Empirical data

Hand-typed stimulus tables recording [Ken07]'s descriptive patterns: comparison-class shift, antonym scales, the adjective typology, and degree modifier compatibility.

structure Kennedy2007.ContextShiftDatum : Type

Empirical pattern: Scalar adjective thresholds shift with comparison class.

The same individual can be "tall" relative to one class but "not tall" relative to another. The threshold tracks statistical properties of the comparison class (especially mean and variance).

Examples:

• 5'10" is tall for a jockey but not tall for a basketball player
• $500,000 is expensive for Atlanta but cheap for San Francisco

Source: [Ken07], [Gra00], [LG17]

• adjective : String

  The adjective being used

• individual : String

  The individual/item being described

• scaleValue : String

  The value on the underlying scale (as string for flexibility)

• comparisonClass1 : String

  First comparison class

• comparisonClass2 : String

  Second comparison class

• judgmentInClass1 : Bool

  Judgment in first class (true = adjective applies)

• judgmentInClass2 : Bool

  Judgment in second class

def Kennedy2007.instReprContextShiftDatum.repr : ContextShiftDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kennedy2007.instReprContextShiftDatum : Repr ContextShiftDatum

Equations

• Kennedy2007.instReprContextShiftDatum = { reprPrec := Kennedy2007.instReprContextShiftDatum.repr }

def Kennedy2007.jockeyBasketball : ContextShiftDatum

Classic height example: 5'10" person.

Equations

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

def Kennedy2007.atlantaSanFrancisco : ContextShiftDatum

House price example.

Equations

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

def Kennedy2007.microbePlanet : ContextShiftDatum

Size example across orders of magnitude.

Equations

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

def Kennedy2007.contextShiftExamples : List ContextShiftDatum

Equations

• Kennedy2007.contextShiftExamples = [Kennedy2007.jockeyBasketball, Kennedy2007.atlantaSanFrancisco, Kennedy2007.microbePlanet]

structure Kennedy2007.AntonymDatum : Type

Empirical pattern: Antonym pairs share a scale with reversed polarity.

"Tall" and "short" live on the same height scale but point in opposite directions. This creates the "excluded middle gap" where neither applies clearly (the borderline region).

Source: [Ken07], [LG17]

• positive : String

  The positive adjective

• negative : String

  The negative adjective

• scale : String

  The underlying scale

• negationType : Features.NegationType

  Contradictory (A ≡ ¬B, no gap) or contrary (can both be false, gap).

• positiveExample : String

  Example where positive applies

• negativeExample : String

  Example where negative applies

• neitherExample : String

  Example where neither clearly applies

def Kennedy2007.instReprAntonymDatum.repr : AntonymDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kennedy2007.instReprAntonymDatum : Repr AntonymDatum

Equations

• Kennedy2007.instReprAntonymDatum = { reprPrec := Kennedy2007.instReprAntonymDatum.repr }

def Kennedy2007.tallShortAntonym : AntonymDatum

Equations

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

def Kennedy2007.expensiveCheapAntonym : AntonymDatum

Equations

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

def Kennedy2007.antonymExamples : List AntonymDatum

Equations

• Kennedy2007.antonymExamples = [Kennedy2007.tallShortAntonym, Kennedy2007.expensiveCheapAntonym]

structure Kennedy2007.AdjectiveTypologyDatum : Type

Data capturing Kennedy's adjective typology predictions.

Key diagnostic: behavior with degree modifiers

• RGA: "??slightly tall", "??completely tall" (odd)
• AGA-max: "slightly bent", "completely straight" (natural)
• AGA-min: "slightly wet", "??completely wet" (asymmetric)

Source: [Ken07] §3

• adjective : String

  The adjective

• classification : Degree.AdjectiveClass

  Its classification

• scale : String

  The underlying scale name (e.g., "height", "fullness")

• scaleType : Core.Order.Boundedness

  Scale structure (Kennedy 2007's 4-way typology), the canonical Boundedness enum rather than a Bool-pair re-encoding.

• naturalWithSlightly : Bool

  Natural with "slightly X"?

• naturalWithCompletely : Bool

  Natural with "completely X"?

• thresholdShifts : Bool

  Threshold shifts with comparison class?

def Kennedy2007.instReprAdjectiveTypologyDatum.repr : AdjectiveTypologyDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kennedy2007.instReprAdjectiveTypologyDatum : Repr AdjectiveTypologyDatum

Equations

• Kennedy2007.instReprAdjectiveTypologyDatum = { reprPrec := Kennedy2007.instReprAdjectiveTypologyDatum.repr }

def Kennedy2007.tallTypology : AdjectiveTypologyDatum

"Tall" — prototypical relative gradable adjective; open scale.

Equations

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

def Kennedy2007.fullTypology : AdjectiveTypologyDatum

"Full" — absolute maximum standard adjective; totally closed scale.

Equations

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

def Kennedy2007.wetTypology : AdjectiveTypologyDatum

"Wet" — absolute minimum standard adjective; lower-bounded scale.

Equations

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

def Kennedy2007.straightTypology : AdjectiveTypologyDatum

"Straight" — absolute maximum standard adjective; totally closed scale.

Equations

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

def Kennedy2007.bentTypology : AdjectiveTypologyDatum

"Bent" — absolute minimum standard adjective; lower-bounded scale.

Equations

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

def Kennedy2007.adjectiveTypologyExamples : List AdjectiveTypologyDatum

Equations

• Kennedy2007.adjectiveTypologyExamples = [Kennedy2007.tallTypology, Kennedy2007.fullTypology, Kennedy2007.wetTypology, Kennedy2007.straightTypology, Kennedy2007.bentTypology]

structure Kennedy2007.RGAvsAGAPrediction : Type

The key prediction: RGAs are context-sensitive, AGAs are not.

This is testable: change comparison class, see if threshold shifts.

• "tall for a basketball player" vs "tall for a jockey" - shifts
• "wet for a desert" vs "wet for a rainforest" - does NOT shift

• rgaAdjective : String
• agaAdjective : String
• rgaShifts : Bool
• agaShifts : Bool
• rgaShiftExample : String
• agaNonShiftExample : String

@[implicit_reducible]

instance Kennedy2007.instReprRGAvsAGAPrediction : Repr RGAvsAGAPrediction

Equations

• Kennedy2007.instReprRGAvsAGAPrediction = { reprPrec := Kennedy2007.instReprRGAvsAGAPrediction.repr }

def Kennedy2007.instReprRGAvsAGAPrediction.repr : RGAvsAGAPrediction → ℕ → Std.Format

Equations

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

def Kennedy2007.rgaVsAgaPrediction : RGAvsAGAPrediction

Equations

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

inductive Kennedy2007.DegreeModifierType : Type

Degree modifiers and their interactions with adjective types.

Key modifiers:

• Proportional: "half", "completely", "partially"
• Measure phrases: "6 feet tall", "3 degrees warmer"
• Intensifiers: "very", "extremely", "incredibly"
• Diminishers: "slightly", "somewhat", "a bit"

Source: [KMcN05], [Bur17]

• proportional : DegreeModifierType
• measurePhrase : DegreeModifierType
• intensifier : DegreeModifierType
• diminisher : DegreeModifierType

def Kennedy2007.instReprDegreeModifierType.repr : DegreeModifierType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kennedy2007.instReprDegreeModifierType : Repr DegreeModifierType

Equations

• Kennedy2007.instReprDegreeModifierType = { reprPrec := Kennedy2007.instReprDegreeModifierType.repr }

@[implicit_reducible]

instance Kennedy2007.instDecidableEqDegreeModifierType : DecidableEq DegreeModifierType

Equations

• Kennedy2007.instDecidableEqDegreeModifierType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Kennedy2007.DegreeModifierDatum : Type

Data capturing degree modifier compatibility patterns.

The puzzle: Why can you say "completely full" but not "??completely tall"?

Answer: Proportional modifiers require a BOUNDED scale (endpoints).

• "Full" has a maximum → "completely full" works
• "Tall" has no maximum → "??completely tall" is odd

Source: [KMcN05]

• modifier : String
• modifierType : DegreeModifierType
• worksWithRGA : Bool
• worksWithAGAMax : Bool
• worksWithAGAMin : Bool
• goodExample : String
• badExample : String

@[implicit_reducible]

instance Kennedy2007.instReprDegreeModifierDatum : Repr DegreeModifierDatum

Equations

• Kennedy2007.instReprDegreeModifierDatum = { reprPrec := Kennedy2007.instReprDegreeModifierDatum.repr }

def Kennedy2007.instReprDegreeModifierDatum.repr : DegreeModifierDatum → ℕ → Std.Format

Equations

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

def Kennedy2007.completelyModifier : DegreeModifierDatum

Equations

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

def Kennedy2007.slightlyModifier : DegreeModifierDatum

Equations

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

def Kennedy2007.veryModifier : DegreeModifierDatum

Equations

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

def Kennedy2007.halfModifier : DegreeModifierDatum

Equations

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

def Kennedy2007.degreeModifierExamples : List DegreeModifierDatum

Equations

• Kennedy2007.degreeModifierExamples = [Kennedy2007.completelyModifier, Kennedy2007.slightlyModifier, Kennedy2007.veryModifier, Kennedy2007.halfModifier]

structure Kennedy2007.ScaleClosurePuzzle : Type

The degree modifier puzzle: Why the distribution?

Formal constraint: Proportional modifiers require a CLOSED scale.

• Closed scale: has both minimum and maximum endpoints
• Open scale: missing at least one endpoint

This explains:

• "completely full" ✓ (fullness scale: empty to full)
• "??completely tall" ✗ (height scale: 0 to... what?)

Source: [KMcN05], [RW04b]

• closedScaleAdj : String
• openScaleAdj : String
• modifier : String
• worksWithClosed : Bool
• worksWithOpen : Bool

def Kennedy2007.instReprScaleClosurePuzzle.repr : ScaleClosurePuzzle → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kennedy2007.instReprScaleClosurePuzzle : Repr ScaleClosurePuzzle

Equations

• Kennedy2007.instReprScaleClosurePuzzle = { reprPrec := Kennedy2007.instReprScaleClosurePuzzle.repr }

def Kennedy2007.closurePuzzle : ScaleClosurePuzzle

Equations

• Kennedy2007.closurePuzzle = { closedScaleAdj := "full", openScaleAdj := "tall", modifier := "completely", worksWithClosed := true, worksWithOpen := false }

Modifier-class licensing matrix (eq. (61))

[Ken07] eq. (61) (= [KMcN05] eq. (15)) is the central typological prediction: which scale-structure types license which modifier classes. The matrix is the load-bearing connection between the data fields above (completelyModifier/slightlyModifier/halfModifier/veryModifier) and the Boundedness scale-structure substrate.

Per the matrix:

• Maximizers / proportional (completely, perfectly, absolutely, half) require an UPPER endpoint → license iff Boundedness.HasMax.
• Minimizers / diminishers (slightly, partially, somewhat) require a LOWER endpoint → license iff Boundedness.HasMin.
• Intensifiers (very, extremely) work on all scales (modulo pragmatic considerations).
• Measure phrases (6 feet tall) work on all dimensional scales ([HKL99]).

def Kennedy2007.Licenses : DegreeModifierType → Core.Order.Boundedness → Prop

Equations

• Kennedy2007.Licenses Kennedy2007.DegreeModifierType.proportional x✝ = x✝.HasMax
• Kennedy2007.Licenses Kennedy2007.DegreeModifierType.diminisher x✝ = x✝.HasMin
• Kennedy2007.Licenses Kennedy2007.DegreeModifierType.intensifier x✝ = True
• Kennedy2007.Licenses Kennedy2007.DegreeModifierType.measurePhrase x✝ = True

@[implicit_reducible]

instance Kennedy2007.instDecidableLicenses (m : DegreeModifierType) (b : Core.Order.Boundedness) : Decidable (Licenses m b)

Equations

• Kennedy2007.instDecidableLicenses Kennedy2007.DegreeModifierType.proportional x✝ = Kennedy2007.instDecidableLicenses._aux_1 x✝
• Kennedy2007.instDecidableLicenses Kennedy2007.DegreeModifierType.diminisher x✝ = Kennedy2007.instDecidableLicenses._aux_3 x✝
• Kennedy2007.instDecidableLicenses Kennedy2007.DegreeModifierType.intensifier x✝ = isTrue trivial
• Kennedy2007.instDecidableLicenses Kennedy2007.DegreeModifierType.measurePhrase x✝ = isTrue trivial

Fragment licensing bridges

Connects the abstract adjMeasure and LicensingPipeline algebra to the concrete English Fragment entries (tall, full, wet, dry) and the empirical data above, and verifies the per-entry typology data against the Fragment annotations.

Fragment → DirectedMeasure licensing

theorem Kennedy2007.tall_blocks_completely {max : ℕ} {W : Type u_1} (μ : W → Degree.Degree max) : ¬(Semantics.Gradability.adjMeasure μ English.Predicates.Adjectival.tall).IsLicensed

"tall" (open scale) → DirectedMeasure blocks degree modification.

theorem Kennedy2007.full_licenses_completely {max : ℕ} {W : Type u_1} (μ : W → Degree.Degree max) : (Semantics.Gradability.adjMeasure μ English.Predicates.Adjectival.full).IsLicensed

"full" (closed scale) → DirectedMeasure licenses degree modification.

theorem Kennedy2007.wet_licensed {max : ℕ} {W : Type u_1} (μ : W → Degree.Degree max) : (Semantics.Gradability.adjMeasure μ English.Predicates.Adjectival.wet).IsLicensed

"wet" (closed scale) → DirectedMeasure licenses.

theorem Kennedy2007.dry_licensed {max : ℕ} {W : Type u_1} (μ : W → Degree.Degree max) : (Semantics.Gradability.adjMeasure μ English.Predicates.Adjectival.dry).IsLicensed

"dry" (closed scale) → DirectedMeasure licenses.

DirectedMeasure → data bridges

theorem Kennedy2007.closurePuzzle_predicted {max : ℕ} {W : Type u_1} (μ : W → Degree.Degree max) : ((Semantics.Gradability.adjMeasure μ English.Predicates.Adjectival.full).IsLicensed ↔ closurePuzzle.worksWithClosed = true) ∧ ((Semantics.Gradability.adjMeasure μ English.Predicates.Adjectival.tall).IsLicensed ↔ closurePuzzle.worksWithOpen = true)

The closure puzzle is predicted by DirectedMeasure: closed-scale adjectives license "completely", open-scale ones don't. Matches closurePuzzle.worksWithClosed / .worksWithOpen.

theorem Kennedy2007.completely_distribution {max : ℕ} {W : Type u_1} (μ : W → Degree.Degree max) : ((Semantics.Gradability.adjMeasure μ English.Predicates.Adjectival.full).IsLicensed ↔ completelyModifier.worksWithAGAMax = true) ∧ ((Semantics.Gradability.adjMeasure μ English.Predicates.Adjectival.tall).IsLicensed ↔ completelyModifier.worksWithRGA = true)

"completely" works with AGA-max (closed) but not RGA (open). adjMeasure licensing matches completelyModifier fields.

LicensingPipeline bridges

theorem Kennedy2007.adj_pipeline_tall : ¬Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.tall)

"tall" through the universal pipeline: open_ → blocked.

theorem Kennedy2007.adj_pipeline_full : Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.full)

"full" through the universal pipeline: closed → licensed.

theorem Kennedy2007.adj_pipeline_wet : Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.wet)

"wet" through the universal pipeline: closed (endpoint) → licensed.

theorem Kennedy2007.adj_pipeline_dry : Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.dry)

"dry" through the universal pipeline: closed (endpoint) → licensed.

theorem Kennedy2007.pipeline_agrees_with_measure {max : ℕ} {W : Type u_1} (μ : W → Degree.Degree max) : (Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.tall) ↔ (Semantics.Gradability.adjMeasure μ English.Predicates.Adjectival.tall).IsLicensed) ∧ (Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.full) ↔ (Semantics.Gradability.adjMeasure μ English.Predicates.Adjectival.full).IsLicensed) ∧ (Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.wet) ↔ (Semantics.Gradability.adjMeasure μ English.Predicates.Adjectival.wet).IsLicensed) ∧ (Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.dry) ↔ (Semantics.Gradability.adjMeasure μ English.Predicates.Adjectival.dry).IsLicensed)

Pipeline agrees with DirectedMeasure for all four test adjectives.

Scale structure → comparison-class sensitivity

Whether an adjective's standard depends on contextual domain information is read off its scale structure ([Ken07]): scaleType → interpretiveEconomy → PositiveStandard → PositiveStandard.RequiresComparisonClass. An open scale yields a contextual s (requires a comparison class); a closed scale fixes the standard at an endpoint via Interpretive Economy.

Kennedy argues that the comparison class is descriptively real but NOT a semantic argument of pos; it feeds into s contextually rather than as a constituent of logical form.

theorem Kennedy2007.tall_requires_cc : (Degree.interpretiveEconomy (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.tall)).RequiresComparisonClass

"tall": open scale ⇒ CC-dependence.

theorem Kennedy2007.full_no_cc : ¬(Degree.interpretiveEconomy (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.full)).RequiresComparisonClass

"full": maximum-standard (closed scale) ⇒ CC-independence.

theorem Kennedy2007.wet_no_cc : ¬(Degree.interpretiveEconomy (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.wet)).RequiresComparisonClass

"wet": closed scale ⇒ endpoint standard ⇒ CC-independence.

theorem Kennedy2007.dry_no_cc : ¬(Degree.interpretiveEconomy (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.dry)).RequiresComparisonClass

"dry": closed scale ⇒ endpoint standard ⇒ CC-independence.

MPA classification ([Bel25])

theorem Kennedy2007.mpa_mildly_positive : Semantics.Gradability.GradableAdjective.adjectiveClass English.Predicates.Adjectival.decent = Degree.AdjectiveClass.mildlyPositive ∧ Semantics.Gradability.GradableAdjective.adjectiveClass English.Predicates.Adjectival.acceptable = Degree.AdjectiveClass.mildlyPositive ∧ Semantics.Gradability.GradableAdjective.adjectiveClass English.Predicates.Adjectival.adequate = Degree.AdjectiveClass.mildlyPositive

MPAs are the mildly-positive class: an open .value scale carrying a functional (necessity) standard via standardOverride. Their special status is the standard, not scale boundedness — so on scale shape they pattern with the relative adjectives (not endpoint-licensed), and their resistance to very/extremely is pragmatic (conflicts with the middling inference).

theorem Kennedy2007.mpa_good_same_licensing : Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.decent) ↔ Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.good)

MPAs and good share scale-structure licensing status: both sit on the open .value scale, so neither is endpoint-licensed. Their difference is in standard type (functional vs contextual), not in structural licensing.

theorem Kennedy2007.mpa_ie_exception : Degree.interpretiveEconomy (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.decent) = Degree.PositiveStandard.contextual ∧ Semantics.Gradability.GradableAdjective.standard English.Predicates.Adjectival.decent = Degree.PositiveStandard.functional

IE path diverges for MPAs: the open-scale shape-default is a contextual standard (interpretiveEconomy .open_), yet MPAs actually receive a functional standard via standardOverride. A genuine exception to Interpretive Economy, distinct from good's (which keeps the contextual default).

Modifier-class matrix consistency (eq. (61))

theorem Kennedy2007.k2007_matrix_agrees_with_typology (d : AdjectiveTypologyDatum) : d ∈ adjectiveTypologyExamples → (Licenses DegreeModifierType.diminisher d.scaleType ↔ d.naturalWithSlightly = true) ∧ (Licenses DegreeModifierType.proportional d.scaleType ↔ d.naturalWithCompletely = true)

The Licenses matrix agrees with the per-adjective typology data in adjectiveTypologyExamples: for each of the 5 adjectives spanning the 4-way Boundedness typology, the matrix predicts naturalWithSlightly from Licenses .diminisher and naturalWithCompletely from Licenses .proportional.

theorem Kennedy2007.k2007_modifier_data_agrees (d : DegreeModifierDatum) : d ∈ degreeModifierExamples → (Licenses d.modifierType Core.Order.Boundedness.closed ↔ d.worksWithAGAMax = true) ∧ (Licenses d.modifierType Core.Order.Boundedness.lowerBounded ↔ d.worksWithAGAMin = true) ∧ (Licenses d.modifierType Core.Order.Boundedness.open_ ↔ d.worksWithRGA = true)

Per-modifier consistency: each DegreeModifierDatum's worksWithRGA / worksWithAGAMax / worksWithAGAMin fields agree with Licenses on the corresponding Boundedness cases. The AGA-max cases are read at the canonical totally-closed scale (.closed, e.g. full).

theorem Kennedy2007.closurePuzzle_via_matrix : (Licenses DegreeModifierType.proportional Core.Order.Boundedness.closed ↔ closurePuzzle.worksWithClosed = true) ∧ (Licenses DegreeModifierType.proportional Core.Order.Boundedness.open_ ↔ closurePuzzle.worksWithOpen = true)

closurePuzzle (full vs tall, completely) is a direct corollary of the matrix: Licenses .proportional .closed = true matches worksWithClosed, and Licenses .proportional .open_ = false matches worksWithOpen.

Per-entry typology consistency

For each adjective with both a typology datum above and a Fragment entry, verify form match, scale-type consistency, and licensing/threshold agreement.

theorem Kennedy2007.tall_form_match : tallTypology.adjective = English.Predicates.Adjectival.tall.form

"tall" typology datum matches Fragment form.

theorem Kennedy2007.full_form_match : fullTypology.adjective = English.Predicates.Adjectival.full.form

"full" typology datum matches Fragment form.

theorem Kennedy2007.wet_form_match : wetTypology.adjective = English.Predicates.Adjectival.wet.form

"wet" typology datum matches Fragment form.

theorem Kennedy2007.tall_scaleType_consistency : tallTypology.scaleType = Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.tall

"tall" (open): Data scaleType matches Fragment scaleType.

theorem Kennedy2007.full_scaleType_consistency : fullTypology.scaleType = Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.full

"full" (closed): Data scaleType matches Fragment scaleType.

theorem Kennedy2007.wet_class_consistency : Semantics.Gradability.GradableAdjective.adjectiveClass English.Predicates.Adjectival.wet = wetTypology.classification

"wet": Fragment's derived Kennedy class matches the paper typology datum. The raw Boundedness labels now differ — the Fragment models wetness as one closed scale with wet at the lower pole, where Kennedy's datum labels it lower-bounded — but both yield the same absolute-minimum class.

theorem Kennedy2007.straight_scaleType_consistency : straightTypology.scaleType = Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.straight

"straight" (closed): Data scaleType matches Fragment scaleType.

theorem Kennedy2007.bent_class_consistency : Semantics.Gradability.GradableAdjective.adjectiveClass English.Predicates.Adjectival.bent = bentTypology.classification

"bent": Fragment's derived Kennedy class matches the paper typology datum (closed + lower pole vs Kennedy's lower-bounded label; same absolute-minimum class).

theorem Kennedy2007.tall_completely_agrees : Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.tall) ↔ completelyModifier.worksWithRGA = true

"tall" (open scale): pipeline blocked = "completely" doesn't work with RGA.

theorem Kennedy2007.full_completely_agrees : Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.full) ↔ completelyModifier.worksWithAGAMax = true

"full" (closed scale): pipeline licensed = "completely" works with AGA-max.

theorem Kennedy2007.tall_completely_from_pipeline : tallTypology.naturalWithCompletely = true ↔ Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.tall)

"tall": typology's naturalWithCompletely matches pipeline prediction.

theorem Kennedy2007.full_completely_from_pipeline : fullTypology.naturalWithCompletely = true ↔ Core.Order.LicensingPipeline.IsLicensed (Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.full)

"full": typology's naturalWithCompletely matches pipeline prediction.

theorem Kennedy2007.tall_threshold_shifts : tallTypology.thresholdShifts = true ∧ Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.tall = Core.Order.Boundedness.open_

"tall" (open): threshold shifts with comparison class.

theorem Kennedy2007.full_threshold_stable : fullTypology.thresholdShifts = false ∧ Semantics.Gradability.GradableAdjective.scaleType English.Predicates.Adjectival.full = Core.Order.Boundedness.closed

"full" (closed): threshold does NOT shift.