Degree Semantics: Positive-Form Semantics

Threshold-comparison predicates on the concrete Degree max / Threshold max carriers declared in Defs.lean [Ken07] [Hei01] [KMcN05]. The abstract positive-form predicate μ(x) ≥ θ is just Comparison.ge.over μ θ — used directly where needed. Kennedy 2007's interpretive economy lives in the sibling Kennedy.lean.

Main definitions

• positiveMeaning (tall), negativeMeaning (short), notPositiveMeaning (not tall) — the three opposition relations as concrete threshold-comparison predicates on Degree max / Threshold max

Main theorems

• positiveMeaning_monotone — monotonicity in the threshold

Relationship to Gradability.Basic

This module's concrete Degree max := Fin (max + 1) predicates serve computation in RSA models and Fragment entries. Gradability.Basic serves the same clients; this module is imported by Degree/Comparative.lean and other framework siblings, while Gradability.Basic is imported by Fragments/English/ and gradability Studies/ files.

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 Degree.positiveMeaning {max : ℕ} (d : Degree max) (t : Threshold max) : Prop

Positive form (tall): t < d.

Equations

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

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

Polar antonym (short): d < t, evaluated against the antonym's own threshold (which may sit below the positive's — see Gradability.ThresholdPair).

Equations

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

def Degree.notPositiveMeaning {max : ℕ} (d : Degree max) (t : Threshold max) : Prop

Contradictory negation (not tall): d ≤ t, the complement of positiveMeaning. Not the polar antonym — that is negativeMeaning.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Degree.instDecidableNotPositiveMeaning {max : ℕ} (d : Degree max) (t : Threshold max) : Decidable (notPositiveMeaning d t)

Equations

• Degree.instDecidableNotPositiveMeaning d t = Degree.instDecidableNotPositiveMeaning._aux_1 d t

theorem Degree.positiveMeaning_monotone {max : ℕ} (d : Degree max) (θ_weak θ_strong : 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).