@cite{sassoon-2013}

Galit W. Sassoon (2013). A Typology of Multidimensional Adjectives. Journal of Semantics 30: 335–380.

Key Claims

Multidimensional adjectives bind their dimensions via implicit quantifiers:

• healthy is conjunctive: healthy in ALL dimensions (blood pressure AND cholesterol AND lung function …)
• sick is disjunctive: sick in SOME dimension (blood pressure OR cholesterol …)
• intelligent is mixed: context determines ∀ vs ∃

Three hypothesis sets connect dimension binding to other properties:

1. Typology (Hypothesis 1): adjectives classify as conjunctive, disjunctive, or mixed based on co-occurrence with exception phrases (except)
2. Polarity (Hypothesis 2): positive antonyms are conjunctive, negative are disjunctive — follows from a negation theory of antonymy + De Morgan
3. Standard type (Hypothesis 3): total (max standard) → conjunctive, partial (min standard) → disjunctive, relative → mixed

Formalization

The dimension-binding operations and De Morgan theorems are in Theories/Semantics/Lexical/Adjective/Theory.lean. This file contains:

• The 18-adjective sample with empirical classifications from (36a–c), p. 359–360
• Corpus data from Table 3 (conjunctivity/disjunctivity raw counts)
• The 3:1 ratio criterion (p. 358) for classifying adjectives
• Antonym pair structure with De Morgan consistency verification
• Verification theorems connecting polarity, standard type, and binding type

Scale type note

Scale types here use @cite{kennedy-mcnally-2005} Boundedness values, which match the Fragment lexicon. Sassoon's own modifier-distribution analysis (Section 2.3, Table 4) reclassifies several adjectives: good and dissimilar as total, bad and similar as partial. These reclassifications are noted in comments but not encoded, since the correlational H3 test (r = 0.62, p < 0.013 for non-comparatives) is the paper's actual finding — per-adjective binary predictions are our addition for verification purposes.

structure Phenomena.Gradability.Studies.Sassoon2013.MultidimAdj : Type

An adjective in Sassoon's 18-item sample, classified along three axes.

• form : String
• isPositive : Bool

  Evaluative polarity: positive adjectives denote membership under a generalization across ALL dimensional properties; negative adjectives denote the existence of a counterexample to SOME dimensional standard. Distinct from scale-endpoint polarity (AdjModifierEntry.isLowerEndpoint): empty is lower-endpoint but evaluatively positive.

• scaleType : Core.Scale.Boundedness

  Scale structure classification (@cite{kennedy-mcnally-2005}).

• binding : Semantics.Lexical.Adjective.DimensionBindingType

  Observed default binding type from exception-phrase corpus data (36a–c).

instance Phenomena.Gradability.Studies.Sassoon2013.instReprMultidimAdj : Repr MultidimAdj

Equations

• Phenomena.Gradability.Studies.Sassoon2013.instReprMultidimAdj = { reprPrec := Phenomena.Gradability.Studies.Sassoon2013.instReprMultidimAdj.repr }

def Phenomena.Gradability.Studies.Sassoon2013.instReprMultidimAdj.repr : MultidimAdj → ℕ → Std.Format

Equations

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

instance Phenomena.Gradability.Studies.Sassoon2013.instBEqMultidimAdj : BEq MultidimAdj

Equations

• Phenomena.Gradability.Studies.Sassoon2013.instBEqMultidimAdj = { beq := Phenomena.Gradability.Studies.Sassoon2013.instBEqMultidimAdj.beq }

def Phenomena.Gradability.Studies.Sassoon2013.instBEqMultidimAdj.beq : MultidimAdj → MultidimAdj → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Gradability.Studies.Sassoon2013.instBEqMultidimAdj.beq x✝¹ x✝ = false

instance Phenomena.Gradability.Studies.Sassoon2013.instDecidableEqMultidimAdj : DecidableEq MultidimAdj

Equations

• Phenomena.Gradability.Studies.Sassoon2013.instDecidableEqMultidimAdj = Phenomena.Gradability.Studies.Sassoon2013.instDecidableEqMultidimAdj.decEq

def Phenomena.Gradability.Studies.Sassoon2013.instDecidableEqMultidimAdj.decEq (x✝ x✝¹ : MultidimAdj) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.normal : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.typical : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.healthy : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.familiar : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.bad_ : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.sick : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.atypical : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.abnormal : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.different : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.identical : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.similar_ : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.good_ : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.intelligent : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.dissimilar : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.worse_ : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.unfamiliar : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.healthier : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.better_ : MultidimAdj

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.allAdjs : List MultidimAdj

Equations

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

theorem Phenomena.Gradability.Studies.Sassoon2013.sample_size : allAdjs.length = 18

structure Phenomena.Gradability.Studies.Sassoon2013.ExceptData : Type

Exception-phrase corpus data from Table 3. Each adjective has two counts:

• conj: dimensional uses in positive contexts ("P except Dim")
• disj: dimensional uses in negative contexts ("not P except Dim")

The chi-square tests in the paper compare the [conj, disj] distribution between antonym pairs to test whether polarity predicts binding type.

• adj : String
• conj : ℕ
• disj : ℕ

instance Phenomena.Gradability.Studies.Sassoon2013.instReprExceptData : Repr ExceptData

Equations

• Phenomena.Gradability.Studies.Sassoon2013.instReprExceptData = { reprPrec := Phenomena.Gradability.Studies.Sassoon2013.instReprExceptData.repr }

def Phenomena.Gradability.Studies.Sassoon2013.instReprExceptData.repr : ExceptData → ℕ → Std.Format

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.exceptData : List ExceptData

Table 3 data. Values are raw counts of dimensional exception-phrase uses per adjective in positive vs. negative contexts.

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.isStronglyConjunctive (d : ExceptData) : Bool

The 3:1 ratio criterion from p. 358: Sassoon classifies adjectives as conjunctive when the conj/disj ratio is "significantly larger," which she operationalizes as ≥ 3 times the other count.

Equations

• Phenomena.Gradability.Studies.Sassoon2013.isStronglyConjunctive d = decide (d.conj ≥ 3 * d.disj)

def Phenomena.Gradability.Studies.Sassoon2013.isStronglyDisjunctive (d : ExceptData) : Bool

Equations

• Phenomena.Gradability.Studies.Sassoon2013.isStronglyDisjunctive d = decide (d.disj ≥ 3 * d.conj)

def Phenomena.Gradability.Studies.Sassoon2013.classifyFromCorpus (d : ExceptData) : Semantics.Lexical.Adjective.DimensionBindingType

Classification from 3:1 criterion: conjunctive, disjunctive, or mixed.

Equations

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

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_healthy : classifyFromCorpus { adj := "healthy", conj := 54, disj := 11 } = Semantics.Lexical.Adjective.DimensionBindingType.conjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_normal : classifyFromCorpus { adj := "normal", conj := 69, disj := 10 } = Semantics.Lexical.Adjective.DimensionBindingType.conjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_typical : classifyFromCorpus { adj := "typical", conj := 54, disj := 9 } = Semantics.Lexical.Adjective.DimensionBindingType.conjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_familiar : classifyFromCorpus { adj := "familiar", conj := 45, disj := 9 } = Semantics.Lexical.Adjective.DimensionBindingType.conjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_healthier : classifyFromCorpus { adj := "healthier", conj := 35, disj := 9 } = Semantics.Lexical.Adjective.DimensionBindingType.conjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_bad : classifyFromCorpus { adj := "bad", conj := 3, disj := 55 } = Semantics.Lexical.Adjective.DimensionBindingType.disjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_sick : classifyFromCorpus { adj := "sick", conj := 2, disj := 26 } = Semantics.Lexical.Adjective.DimensionBindingType.disjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_atypical : classifyFromCorpus { adj := "atypical", conj := 19, disj := 68 } = Semantics.Lexical.Adjective.DimensionBindingType.disjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_abnormal : classifyFromCorpus { adj := "abnormal", conj := 6, disj := 20 } = Semantics.Lexical.Adjective.DimensionBindingType.disjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_different : classifyFromCorpus { adj := "different", conj := 13, disj := 40 } = Semantics.Lexical.Adjective.DimensionBindingType.disjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_identical : classifyFromCorpus { adj := "identical", conj := 86, disj := 49 } = Semantics.Lexical.Adjective.DimensionBindingType.mixed

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_similar : classifyFromCorpus { adj := "similar", conj := 80, disj := 67 } = Semantics.Lexical.Adjective.DimensionBindingType.mixed

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_good : classifyFromCorpus { adj := "good", conj := 24, disj := 21 } = Semantics.Lexical.Adjective.DimensionBindingType.mixed

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_intelligent : classifyFromCorpus { adj := "intelligent", conj := 37, disj := 41 } = Semantics.Lexical.Adjective.DimensionBindingType.mixed

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_dissimilar : classifyFromCorpus { adj := "dissimilar", conj := 58, disj := 83 } = Semantics.Lexical.Adjective.DimensionBindingType.mixed

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_unfamiliar : classifyFromCorpus { adj := "unfamiliar", conj := 15, disj := 27 } = Semantics.Lexical.Adjective.DimensionBindingType.mixed

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_better : classifyFromCorpus { adj := "better", conj := 25, disj := 25 } = Semantics.Lexical.Adjective.DimensionBindingType.mixed

theorem Phenomena.Gradability.Studies.Sassoon2013.classify_worse : classifyFromCorpus { adj := "worse", conj := 20, disj := 32 } = Semantics.Lexical.Adjective.DimensionBindingType.mixed

theorem Phenomena.Gradability.Studies.Sassoon2013.corpus_matches_classification : (exceptData.all fun (d : ExceptData) => classifyFromCorpus d == (Option.map MultidimAdj.binding (List.find? (fun (a : MultidimAdj) => a.form == d.adj) allAdjs)).getD Semantics.Lexical.Adjective.DimensionBindingType.mixed) = true

All 18 adjectives: corpus classification matches assigned binding type.

def Phenomena.Gradability.Studies.Sassoon2013.antonymPairs : List (MultidimAdj × MultidimAdj)

Antonym pairs from the paper's sample. Each pair (positive, negative) should satisfy De Morgan consistency: if the positive is conjunctive, the negative should be disjunctive, and vice versa. Mixed adjectives are exempt (mixed.negate = mixed).

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.deMorganConsistent (pos neg : MultidimAdj) : Bool

De Morgan consistency: the negative antonym's binding type matches .negate of the positive antonym's binding, or one of them is mixed (context-dependent, so not constrained by De Morgan).

Equations

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

theorem Phenomena.Gradability.Studies.Sassoon2013.antonyms_consistent : (antonymPairs.all fun (x : MultidimAdj × MultidimAdj) => match x with | (p, n) => deMorganConsistent p n) = true

theorem Phenomena.Gradability.Studies.Sassoon2013.healthy_sick_consistent : deMorganConsistent healthy sick = true

theorem Phenomena.Gradability.Studies.Sassoon2013.normal_abnormal_consistent : deMorganConsistent normal abnormal = true

theorem Phenomena.Gradability.Studies.Sassoon2013.typical_atypical_consistent : deMorganConsistent typical atypical = true

theorem Phenomena.Gradability.Studies.Sassoon2013.familiar_unfamiliar_consistent : deMorganConsistent familiar unfamiliar = true

theorem Phenomena.Gradability.Studies.Sassoon2013.good_bad_consistent : deMorganConsistent good_ bad_ = true

theorem Phenomena.Gradability.Studies.Sassoon2013.similar_dissimilar_consistent : deMorganConsistent similar_ dissimilar = true

theorem Phenomena.Gradability.Studies.Sassoon2013.identical_different_consistent : deMorganConsistent identical different = true

theorem Phenomena.Gradability.Studies.Sassoon2013.healthier_inherits : healthier.binding = healthy.binding

Comparatives inherit binding type from their base adjective (p. 360). healthier inherits conjunctive from healthy; better inherits mixed from good.

theorem Phenomena.Gradability.Studies.Sassoon2013.better_inherits : better_.binding = good_.binding

theorem Phenomena.Gradability.Studies.Sassoon2013.worse_diverges : worse_.binding ≠ bad_.binding

worse diverges from bad: bad is disjunctive, but worse is mixed. This is expected — comparative morphology changes scale structure (closed → open), which shifts the H3 prediction.

Under a negation theory of antonymy (@cite{heim-2006}, @cite{buering-2007}), if a positive adjective P is conjunctive (∀Q∈DIM: Q(x)), then its negative antonym ¬P is disjunctive (∃Q∈DIM: ¬Q(x)), by De Morgan's laws. The proof is in Theory.lean as deMorgan_conjunctive_disjunctive.

def Phenomena.Gradability.Studies.Sassoon2013.predictedFromPolarity (isPositive : Bool) : Semantics.Lexical.Adjective.DimensionBindingType

Predicted binding type from evaluative polarity, assuming positive member of each antonym pair is conjunctive.

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.hypothesis2Holds (a : MultidimAdj) : Bool

Hypothesis 2 is satisfied when the adjective is mixed (context-dependent) or when its binding matches the polarity prediction.

Equations

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

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis2_all : allAdjs.all hypothesis2Holds = true

def Phenomena.Gradability.Studies.Sassoon2013.predictedFromStandard (b : Core.Scale.Boundedness) : Semantics.Lexical.Adjective.DimensionBindingType

Predicted binding type from scale structure via Interpretive Economy. Max-endpoint standard → conjunctive, min-endpoint → disjunctive, contextual → mixed.

Equations

• Phenomena.Gradability.Studies.Sassoon2013.predictedFromStandard b = Semantics.Lexical.Adjective.predictedBinding (Semantics.Degree.interpretiveEconomy b)

theorem Phenomena.Gradability.Studies.Sassoon2013.standard_closed_conjunctive : predictedFromStandard Core.Scale.Boundedness.closed = Semantics.Lexical.Adjective.DimensionBindingType.conjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.standard_upperBounded_conjunctive : predictedFromStandard Core.Scale.Boundedness.upperBounded = Semantics.Lexical.Adjective.DimensionBindingType.conjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.standard_lowerBounded_disjunctive : predictedFromStandard Core.Scale.Boundedness.lowerBounded = Semantics.Lexical.Adjective.DimensionBindingType.disjunctive

theorem Phenomena.Gradability.Studies.Sassoon2013.standard_open_mixed : predictedFromStandard Core.Scale.Boundedness.open_ = Semantics.Lexical.Adjective.DimensionBindingType.mixed

def Phenomena.Gradability.Studies.Sassoon2013.hypothesis3Holds (a : MultidimAdj) : Bool

Equations

• Phenomena.Gradability.Studies.Sassoon2013.hypothesis3Holds a = (a.binding == Phenomena.Gradability.Studies.Sassoon2013.predictedFromStandard a.scaleType)

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_normal : hypothesis3Holds normal = true

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_typical : hypothesis3Holds typical = true

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_healthy : hypothesis3Holds healthy = true

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_sick : hypothesis3Holds sick = true

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_atypical : hypothesis3Holds atypical = true

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_abnormal : hypothesis3Holds abnormal = true

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_different : hypothesis3Holds different = true

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_similar : hypothesis3Holds similar_ = true

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_good : hypothesis3Holds good_ = true

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_intelligent : hypothesis3Holds intelligent = true

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_dissimilar : hypothesis3Holds dissimilar = true

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_worse : hypothesis3Holds worse_ = true

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_identical_fails : hypothesis3Holds identical = false

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_familiar_fails : hypothesis3Holds familiar = false

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_unfamiliar_fails : hypothesis3Holds unfamiliar = false

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_bad_fails : hypothesis3Holds bad_ = false

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_healthier_fails : hypothesis3Holds healthier = false

theorem Phenomena.Gradability.Studies.Sassoon2013.hypothesis3_success_count : (List.filter hypothesis3Holds allAdjs).length = 13

H3 holds for 13 of 18 adjectives (72%) using K&M2005 scale types.

The full chain connecting Hypothesis 2 to the De Morgan theorems:

1. *healthy* is conjunctive: `conjunctiveBinding healthDims x`
2. Under negation theory of antonymy, *sick* ≈ ¬*healthy*
3. By `deMorgan_conjunctive_disjunctive`:
   `!conjunctiveBinding healthDims x = disjunctiveBinding (neg healthDims) x`
4. Therefore *sick* is disjunctive: QED

We demonstrate this with a concrete 3-dimension health model. 

structure Phenomena.Gradability.Studies.Sassoon2013.HealthState : Type

• bp : Bool
• cholesterol : Bool
• lung : Bool

def Phenomena.Gradability.Studies.Sassoon2013.instDecidableEqHealthState.decEq (x✝ x✝¹ : HealthState) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Gradability.Studies.Sassoon2013.instDecidableEqHealthState : DecidableEq HealthState

Equations

• Phenomena.Gradability.Studies.Sassoon2013.instDecidableEqHealthState = Phenomena.Gradability.Studies.Sassoon2013.instDecidableEqHealthState.decEq

def Phenomena.Gradability.Studies.Sassoon2013.instReprHealthState.repr : HealthState → ℕ → Std.Format

Equations

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

instance Phenomena.Gradability.Studies.Sassoon2013.instReprHealthState : Repr HealthState

Equations

• Phenomena.Gradability.Studies.Sassoon2013.instReprHealthState = { reprPrec := Phenomena.Gradability.Studies.Sassoon2013.instReprHealthState.repr }

def Phenomena.Gradability.Studies.Sassoon2013.healthDims : List (HealthState → Bool)

Equations

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

def Phenomena.Gradability.Studies.Sassoon2013.dan : HealthState

Dan: high on 2 dimensions, fails lung.

Equations

• Phenomena.Gradability.Studies.Sassoon2013.dan = { bp := true, cholesterol := true, lung := false }

def Phenomena.Gradability.Studies.Sassoon2013.sam : HealthState

Sam: meets all 3 standards.

Equations

• Phenomena.Gradability.Studies.Sassoon2013.sam = { bp := true, cholesterol := true, lung := true }

theorem Phenomena.Gradability.Studies.Sassoon2013.dan_not_healthy : Semantics.Lexical.Adjective.conjunctiveBinding healthDims dan = false

theorem Phenomena.Gradability.Studies.Sassoon2013.sam_healthy : Semantics.Lexical.Adjective.conjunctiveBinding healthDims sam = true

theorem Phenomena.Gradability.Studies.Sassoon2013.dan_sick : Semantics.Lexical.Adjective.disjunctiveBinding (List.map (fun (d : HealthState → Bool) (a : HealthState) => !d a) healthDims) dan = true

theorem Phenomena.Gradability.Studies.Sassoon2013.sam_not_sick : Semantics.Lexical.Adjective.disjunctiveBinding (List.map (fun (d : HealthState → Bool) (a : HealthState) => !d a) healthDims) sam = false

theorem Phenomena.Gradability.Studies.Sassoon2013.not_healthy_iff_sick (s : HealthState) : (!Semantics.Lexical.Adjective.conjunctiveBinding healthDims s) = Semantics.Lexical.Adjective.disjunctiveBinding (List.map (fun (d : HealthState → Bool) (a : HealthState) => !d a) healthDims) s

End-to-end: "not healthy" and "sick" are equivalent under the negation theory of antonymy + De Morgan.

structure Phenomena.Gradability.Studies.Sassoon2013.PolarityJudgment : Type

Polarity judgment on a 1–7 scale (1 = perfectly negative, 7 = perfectly positive). Mean from 20 AMT participants.

• adj : String
• mean : Float
• isPositive : Bool

def Phenomena.Gradability.Studies.Sassoon2013.instReprPolarityJudgment.repr : PolarityJudgment → ℕ → Std.Format

Equations

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

instance Phenomena.Gradability.Studies.Sassoon2013.instReprPolarityJudgment : Repr PolarityJudgment

Equations

• Phenomena.Gradability.Studies.Sassoon2013.instReprPolarityJudgment = { reprPrec := Phenomena.Gradability.Studies.Sassoon2013.instReprPolarityJudgment.repr }

def Phenomena.Gradability.Studies.Sassoon2013.polarityData : List PolarityJudgment

Equations

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

theorem Phenomena.Gradability.Studies.Sassoon2013.polarity_above_midpoint : (polarityData.all fun (j : PolarityJudgment) => if j.isPositive = true then decide (j.mean > 4.0) else decide (j.mean < 4.0)) = true

All positive adjectives have mean > 4, all negative have mean < 4. Midpoint 4 cleanly separates the two groups.