@cite{kennedy-2007} Adjective Licensing Bridge

@cite{kennedy-2007} @cite{kennedy-mcnally-2005}

Connects the abstract adjMeasure and LicensingPipeline algebra (Core/Scale) to concrete Fragment entries (tall, full, wet, dry) and Phenomena data (closurePuzzle, completelyModifier).

Bridge Structure

1. Fragment → DirectedMeasure: each Fragment entry's scaleType determines a DirectedMeasure, whose .licensed field yields the licensing prediction.

2. DirectedMeasure → Data: the licensing prediction matches the empirical patterns recorded in closurePuzzle and completelyModifier.

3. LicensingPipeline: the same prediction is available through the universal LicensingPipeline.isLicensed interface, connecting adjective licensing to telicity, path shape, and mereological licensing.

structure Phenomena.Gradability.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: @cite{kennedy-2007}, @cite{fara-2000}, @cite{lassiter-goodman-2017}

• 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 Phenomena.Gradability.Kennedy2007.instReprContextShiftDatum.repr : ContextShiftDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Gradability.Kennedy2007.instReprContextShiftDatum : Repr ContextShiftDatum

Equations

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

def Phenomena.Gradability.Kennedy2007.jockeyBasketball : ContextShiftDatum

Classic height example: 5'10" person.

Equations

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

def Phenomena.Gradability.Kennedy2007.atlantaSanFrancisco : ContextShiftDatum

House price example.

Equations

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

def Phenomena.Gradability.Kennedy2007.microbePlanet : ContextShiftDatum

Size example across orders of magnitude.

Equations

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

def Phenomena.Gradability.Kennedy2007.contextShiftExamples : List ContextShiftDatum

Equations

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

structure Phenomena.Gradability.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: @cite{kennedy-2007}, @cite{lassiter-goodman-2017}

• positive : String

  The positive adjective

• negative : String

  The negative adjective

• scale : String

  The underlying scale

• negationType : Core.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 Phenomena.Gradability.Kennedy2007.instReprAntonymDatum.repr : AntonymDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Gradability.Kennedy2007.instReprAntonymDatum : Repr AntonymDatum

Equations

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

def Phenomena.Gradability.Kennedy2007.tallShortAntonym : AntonymDatum

Equations

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

def Phenomena.Gradability.Kennedy2007.expensiveCheapAntonym : AntonymDatum

Equations

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

def Phenomena.Gradability.Kennedy2007.antonymExamples : List AntonymDatum

Equations

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

structure Phenomena.Gradability.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: @cite{kennedy-2007} Section 3

• adjective : String

  The adjective

• classification : Semantics.Degree.AdjectiveClass

  Its classification

• scale : String

  The underlying scale

• hasMaxEndpoint : Bool

  Does it have a maximum endpoint?

• hasMinEndpoint : Bool

  Does it have a minimum endpoint?

• naturalWithSlightly : Bool

  Natural with "slightly X"?

• naturalWithCompletely : Bool

  Natural with "completely X"?

• thresholdShifts : Bool

  Threshold shifts with comparison class?

instance Phenomena.Gradability.Kennedy2007.instReprAdjectiveTypologyDatum : Repr AdjectiveTypologyDatum

Equations

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

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

Equations

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

def Phenomena.Gradability.Kennedy2007.tallTypology : AdjectiveTypologyDatum

"Tall" - prototypical relative gradable adjective.

Equations

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

def Phenomena.Gradability.Kennedy2007.fullTypology : AdjectiveTypologyDatum

"Full" - absolute maximum standard adjective.

Equations

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

def Phenomena.Gradability.Kennedy2007.wetTypology : AdjectiveTypologyDatum

"Wet" - absolute minimum standard adjective.

Equations

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

def Phenomena.Gradability.Kennedy2007.straightTypology : AdjectiveTypologyDatum

"Straight" - absolute maximum standard adjective.

Equations

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

def Phenomena.Gradability.Kennedy2007.bentTypology : AdjectiveTypologyDatum

"Bent" - absolute minimum standard adjective.

Equations

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

def Phenomena.Gradability.Kennedy2007.adjectiveTypologyExamples : List AdjectiveTypologyDatum

Equations

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

structure Phenomena.Gradability.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

instance Phenomena.Gradability.Kennedy2007.instReprRGAvsAGAPrediction : Repr RGAvsAGAPrediction

Equations

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

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

Equations

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

def Phenomena.Gradability.Kennedy2007.rgaVsAgaPrediction : RGAvsAGAPrediction

Equations

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

inductive Phenomena.Gradability.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: @cite{kennedy-mcnally-2005}, @cite{burnett-2017}

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

instance Phenomena.Gradability.Kennedy2007.instReprDegreeModifierType : Repr DegreeModifierType

Equations

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

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

Equations

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

instance Phenomena.Gradability.Kennedy2007.instDecidableEqDegreeModifierType : DecidableEq DegreeModifierType

Equations

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

instance Phenomena.Gradability.Kennedy2007.instBEqDegreeModifierType : BEq DegreeModifierType

Equations

• Phenomena.Gradability.Kennedy2007.instBEqDegreeModifierType = { beq := Phenomena.Gradability.Kennedy2007.instBEqDegreeModifierType.beq }

def Phenomena.Gradability.Kennedy2007.instBEqDegreeModifierType.beq : DegreeModifierType → DegreeModifierType → Bool

Equations

• Phenomena.Gradability.Kennedy2007.instBEqDegreeModifierType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Gradability.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: @cite{kennedy-mcnally-2005}

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

instance Phenomena.Gradability.Kennedy2007.instReprDegreeModifierDatum : Repr DegreeModifierDatum

Equations

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

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

Equations

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

def Phenomena.Gradability.Kennedy2007.completelyModifier : DegreeModifierDatum

Equations

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

def Phenomena.Gradability.Kennedy2007.slightlyModifier : DegreeModifierDatum

Equations

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

def Phenomena.Gradability.Kennedy2007.veryModifier : DegreeModifierDatum

Equations

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

def Phenomena.Gradability.Kennedy2007.halfModifier : DegreeModifierDatum

Equations

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

def Phenomena.Gradability.Kennedy2007.degreeModifierExamples : List DegreeModifierDatum

Equations

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

structure Phenomena.Gradability.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: @cite{kennedy-mcnally-2005}, @cite{rotstein-winter-2004}

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

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

Equations

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

instance Phenomena.Gradability.Kennedy2007.instReprScaleClosurePuzzle : Repr ScaleClosurePuzzle

Equations

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

def Phenomena.Gradability.Kennedy2007.closurePuzzle : ScaleClosurePuzzle

Equations

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

theorem Phenomena.Gradability.KennedyLicensingBridge.tall_blocks_completely {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) : (Semantics.Lexical.Adjective.adjMeasure μ Fragments.English.Predicates.Adjectival.tall).licensed = false

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

theorem Phenomena.Gradability.KennedyLicensingBridge.full_licenses_completely {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) : (Semantics.Lexical.Adjective.adjMeasure μ Fragments.English.Predicates.Adjectival.full).licensed = true

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

theorem Phenomena.Gradability.KennedyLicensingBridge.wet_licensed {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) : (Semantics.Lexical.Adjective.adjMeasure μ Fragments.English.Predicates.Adjectival.wet).licensed = true

"wet" (lower-bounded) → DirectedMeasure licenses.

theorem Phenomena.Gradability.KennedyLicensingBridge.dry_licensed {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) : (Semantics.Lexical.Adjective.adjMeasure μ Fragments.English.Predicates.Adjectival.dry).licensed = true

"dry" (upper-bounded) → DirectedMeasure licenses.

theorem Phenomena.Gradability.KennedyLicensingBridge.closurePuzzle_predicted {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) : (Semantics.Lexical.Adjective.adjMeasure μ Fragments.English.Predicates.Adjectival.full).licensed = Kennedy2007.closurePuzzle.worksWithClosed ∧ (Semantics.Lexical.Adjective.adjMeasure μ Fragments.English.Predicates.Adjectival.tall).licensed = Kennedy2007.closurePuzzle.worksWithOpen

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

theorem Phenomena.Gradability.KennedyLicensingBridge.completely_distribution {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) : (Semantics.Lexical.Adjective.adjMeasure μ Fragments.English.Predicates.Adjectival.full).licensed = Kennedy2007.completelyModifier.worksWithAGAMax ∧ (Semantics.Lexical.Adjective.adjMeasure μ Fragments.English.Predicates.Adjectival.tall).licensed = Kennedy2007.completelyModifier.worksWithRGA

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

theorem Phenomena.Gradability.KennedyLicensingBridge.adj_pipeline_tall : Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.tall.scaleType = false

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

theorem Phenomena.Gradability.KennedyLicensingBridge.adj_pipeline_full : Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.full.scaleType = true

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

theorem Phenomena.Gradability.KennedyLicensingBridge.adj_pipeline_wet : Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.wet.scaleType = true

"wet" through the universal pipeline: lowerBounded → licensed.

theorem Phenomena.Gradability.KennedyLicensingBridge.adj_pipeline_dry : Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.dry.scaleType = true

"dry" through the universal pipeline: upperBounded → licensed.

theorem Phenomena.Gradability.KennedyLicensingBridge.pipeline_agrees_with_measure {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) : Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.tall.scaleType = (Semantics.Lexical.Adjective.adjMeasure μ Fragments.English.Predicates.Adjectival.tall).licensed ∧ Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.full.scaleType = (Semantics.Lexical.Adjective.adjMeasure μ Fragments.English.Predicates.Adjectival.full).licensed ∧ Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.wet.scaleType = (Semantics.Lexical.Adjective.adjMeasure μ Fragments.English.Predicates.Adjectival.wet).licensed ∧ Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.dry.scaleType = (Semantics.Lexical.Adjective.adjMeasure μ Fragments.English.Predicates.Adjectival.dry).licensed

Pipeline agrees with DirectedMeasure for all four test adjectives.

Two independent paths to the same prediction

@cite{kennedy-2007}'s scale structure and PropertyDomain.requiresComparisonClass are two independent classifications that converge on the same prediction for whether an adjective's standard depends on contextual domain information:

• Scale-structure path (@cite{kennedy-2007}): scaleType → interpretiveEconomy → PositiveStandard → PositiveStandard.requiresComparisonClass Open scale → contextual s → requires "the distribution of objects in some domain (a comparison class)" (Kennedy 2007, p. 42)
• Domain path (@cite{sedivy-etal-1999}): dimension.domain → PropertyDomain.requiresComparisonClass Size/evaluative/sensory domains → context-sensitive threshold

Note: Kennedy argues (§2.3, p. 16) that the comparison class is descriptively real but NOT a semantic argument of pos. Our requiresComparisonClass tracks whether contextual domain information is needed — compatible with Kennedy's view that this information feeds into s contextually rather than as a constituent of the logical form.

For every concrete Fragment adjective, the two paths agree. This convergence is non-trivial: it reflects the empirical fact that open-scale adjectives tend to belong to context-sensitive domains (size, evaluative), while closed-scale adjectives tend to belong to context-insensitive domains (state).

theorem Phenomena.Gradability.KennedyLicensingBridge.tall_cc_convergence : (Semantics.Degree.interpretiveEconomy Fragments.English.Predicates.Adjectival.tall.scaleType).requiresComparisonClass = true ∧ Fragments.English.Predicates.Adjectival.tall.dimension.domain.requiresComparisonClass = true

"tall": both paths predict CC-dependence.

theorem Phenomena.Gradability.KennedyLicensingBridge.full_no_cc_convergence : (Semantics.Degree.interpretiveEconomy Fragments.English.Predicates.Adjectival.full.scaleType).requiresComparisonClass = false ∧ Fragments.English.Predicates.Adjectival.full.dimension.domain.requiresComparisonClass = false

"full": both paths predict CC-independence.

theorem Phenomena.Gradability.KennedyLicensingBridge.wet_no_cc_convergence : (Semantics.Degree.interpretiveEconomy Fragments.English.Predicates.Adjectival.wet.scaleType).requiresComparisonClass = false ∧ Fragments.English.Predicates.Adjectival.wet.dimension.domain.requiresComparisonClass = false

"wet": both paths predict CC-independence (lower-bounded → endpoint standard; state domain).

theorem Phenomena.Gradability.KennedyLicensingBridge.dry_no_cc_convergence : (Semantics.Degree.interpretiveEconomy Fragments.English.Predicates.Adjectival.dry.scaleType).requiresComparisonClass = false ∧ Fragments.English.Predicates.Adjectival.dry.dimension.domain.requiresComparisonClass = false

"dry": both paths predict CC-independence (upper-bounded → endpoint standard; state domain).

theorem Phenomena.Gradability.KennedyLicensingBridge.mpa_licensed : Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.decent.scaleType = true ∧ Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.acceptable.scaleType = true ∧ Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.adequate.scaleType = true

MPAs (lower-bounded scale) are licensed by the pipeline, just like wet. Their resistance to very/extremely is pragmatic (conflicts with middling inference), not structural.

theorem Phenomena.Gradability.KennedyLicensingBridge.mpa_good_same_licensing : Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.decent.scaleType = Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.good.scaleType

MPAs and good have the same scale-structure licensing status (both lower-bounded → licensed). Their difference is in standard type (functional vs contextual), not in structural licensing.

theorem Phenomena.Gradability.KennedyLicensingBridge.mpa_ie_exception : Semantics.Degree.interpretiveEconomy Fragments.English.Predicates.Adjectival.decent.scaleType = Semantics.Degree.PositiveStandard.minEndpoint ∧ (Semantics.Degree.interpretiveEconomy Fragments.English.Predicates.Adjectival.decent.scaleType).requiresComparisonClass = false ∧ Fragments.English.Predicates.Adjectival.decent.dimension.domain.requiresComparisonClass = true

IE path diverges for MPAs: lower-bounded → minEndpoint, but MPAs actually receive a functional standard. This is a genuine exception to Interpretive Economy, distinct from good's exception.