Degree Semantics: Positive-Form Semantics

Positive-form semantic operations on the types declared in Defs.lean, plus threshold-comparison predicates on the concrete Degree max / Threshold max carriers @cite{kennedy-2007} @cite{heim-2001} @cite{kennedy-mcnally-2005}. Kennedy 2007's interpretive economy lives in the sibling Kennedy.lean.

Main definitions

• positiveSem — abstract positive-form predicate μ(x) ≥ θ
• positiveMeaning, negativeMeaning, antonymMeaning — concrete threshold-comparison predicates on Degree max / Threshold max

Main theorems

• positiveMeaning_monotone — monotonicity in the threshold

Relationship to Gradability.Basic

This module uses abstract types (Entity D : Type* with LinearOrder D) for framework-level theorems. Gradability.Basic uses concrete Degree max := Fin (max + 1) for computation in RSA models and Fragment entries. The two serve different clients: this module is imported by Degree/Comparative.lean and other framework siblings; Gradability.Basic is imported by Fragments/English/ and Phenomena/Gradability/ bridges.

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

The positive (unmarked) form of a gradable adjective: "Kim is tall" is true iff μ(Kim) ≥ θ for a contextual standard θ.

This is the common core across Kennedy and Heim:

• Kennedy: ⟦tall⟧ = λd.λx. height(x) ≥ d, with θ = pos(tall)
• Heim: ⟦tall⟧ = λx. height(x) ≥ θ_c

Klein's approach is different: "tall" is true relative to a comparison class, with no degree parameter.

Equations

• Semantics.Degree.positiveSem μ θ x = (μ x ≥ θ)

Concrete threshold-based meanings

Threshold-comparison predicates on the concrete Degree max / Threshold max carriers. These are general degree operations, not adjective-specific. Decidability is inherited from the underlying Degree/Threshold order.

def Semantics.Degree.positiveMeaning {max : ℕ} (d : Core.Scale.Degree max) (t : Core.Scale.Threshold max) : Prop

Positive form: t < d.

Equations

• Semantics.Degree.positiveMeaning d t = ({ value := t.value.castSucc } < d)

def Semantics.Degree.negativeMeaning {max : ℕ} (d : Core.Scale.Degree max) (t : Core.Scale.Threshold max) : Prop

Negative form: d < t.

Equations

• Semantics.Degree.negativeMeaning d t = (d < { value := t.value.castSucc })

def Semantics.Degree.antonymMeaning {max : ℕ} (d : Core.Scale.Degree max) (t : Core.Scale.Threshold max) : Prop

Antonym: d ≤ t.

Equations

• Semantics.Degree.antonymMeaning d t = (d ≤ { value := t.value.castSucc })

@[implicit_reducible]

instance Semantics.Degree.instDecidablePositiveMeaning {max : ℕ} (d : Core.Scale.Degree max) (t : Core.Scale.Threshold max) : Decidable (positiveMeaning d t)

Equations

• Semantics.Degree.instDecidablePositiveMeaning d t = Semantics.Degree.instDecidablePositiveMeaning._aux_1 d t

@[implicit_reducible]

instance Semantics.Degree.instDecidableNegativeMeaning {max : ℕ} (d : Core.Scale.Degree max) (t : Core.Scale.Threshold max) : Decidable (negativeMeaning d t)

Equations

• Semantics.Degree.instDecidableNegativeMeaning d t = Semantics.Degree.instDecidableNegativeMeaning._aux_1 d t

@[implicit_reducible]

instance Semantics.Degree.instDecidableAntonymMeaning {max : ℕ} (d : Core.Scale.Degree max) (t : Core.Scale.Threshold max) : Decidable (antonymMeaning d t)

Equations

• Semantics.Degree.instDecidableAntonymMeaning d t = Semantics.Degree.instDecidableAntonymMeaning._aux_1 d t

theorem Semantics.Degree.positiveMeaning_monotone {max : ℕ} (d : Core.Scale.Degree max) (θ_weak θ_strong : Core.Scale.Threshold max) (h_ord : θ_weak ≤ θ_strong) (h_strong : positiveMeaning d θ_strong) : positiveMeaning d θ_weak

Monotonicity of positiveMeaning in the threshold: a higher threshold is informationally stronger. If d > θ_strong and θ_weak ≤ θ_strong, then d > θ_weak. Grounds the weak-vs-strong-adjective distinction (InformationalStrength).