LITTLE: Degree Negation

The LITTLE operator [Hei06] [Bur07] as degree-predicate complementation: short = LITTLE tall, less = LITTLE -er, fewer = LITTLE many. Semantically, ⟦LITTLE⟧(P)(d) = ¬P(d). On extents, LITTLE maps posExt to negExt; on intervals (see Intervals.lean §6), it inverts the measured region.

[Bur07] uses LITTLE to analyse cross-polar nomalies: "the ladder was shorter than the house was high" works because MORE [LITTLE long] -er can be reinterpreted as LITTLE-er long (the "more-to-less metamorphosis").

Main definitions

• littlePred — degree-predicate complement, ⟦LITTLE⟧ = λP.λd. ¬ P d

Main theorems

• little_posExt_eq_negExt — the formal content of "short = LITTLE tall"
• little_involution — LITTLE is its own inverse
• little_reverses_comparison — LITTLE flips comparison direction

def Degree.Little.littlePred {D : Type u_1} (P : D → Prop) : D → Prop

LITTLE on degree predicates: complementation.

Equations

• Degree.Little.littlePred P d = ¬P d

theorem Degree.Little.little_posExt_eq_negExt {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (x : Entity) (d : D) : littlePred (fun (x_1 : D) => x_1 ∈ posExt μ x) d ↔ d ∈ negExt μ x

LITTLE maps the positive extent to the negative extent: LITTLE({d | d ≤ μ(x)}) = {d | μ(x) < d}. The formal content of "short = LITTLE tall" — the degree predicate for 'short' is the complement of the degree predicate for 'tall', exactly the relation between posExt and negExt from [Ken99].

theorem Degree.Little.little_involution {D : Type u_1} (P : D → Prop) (d : D) : littlePred (littlePred P) d ↔ P d

LITTLE is an involution: double degree negation cancels.

theorem Degree.Little.little_reverses_comparison {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) : comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ comparativeSem μ b a Core.Order.ScalePolarity.negative

LITTLE reverses the comparison direction: "A is LITTLE-er Adj than B" ↔ "B is Adj-er than A". Delegates to taller_shorter_antonymy.