Documentation

Linglib.Theories.Semantics.Comparison.Delineation

Klein's Delineation Approach #

@cite{klein-1980} @cite{kennedy-2007} @cite{kamp-1975}

@cite{klein-1980} "A Semantics for Positive and Comparative Adjectives": a degree-free analysis where gradable adjectives are simple predicates (type ⟨e,t⟩) whose extension is determined relative to a comparison class — a contextually supplied set of entities.

Lineage from Kamp (1975) #

Klein's comparative — ∃ C. tall(a,C) ∧ ¬tall(b,C) — is a direct formalization of @cite{kamp-1975}'s definition (12): u₁ is at least as A as u₂ iff in every completion where u₂ is in the extension, u₁ is too. Kamp's "completions" become Klein's "comparison classes"; both derive the comparative from existential quantification over ways of making a vague predicate precise.

Key Ideas #

  1. No degrees: "tall" does not denote a relation between entities and degrees. It is simply a predicate whose extension varies with context.

  2. Comparison class: The positive form "Kim is tall" is true iff Kim is tall relative to the contextually relevant comparison class C (e.g., basketball players, children, people in general).

  3. Comparative via supervaluation: "Kim is taller than Lee" is true iff there exists a comparison class C where Kim is tall and Lee is not. This uses a supervaluation over comparison classes rather than degree comparison.

Comparison with Kennedy #

Feature@cite{kennedy-2007}@cite{klein-1980}
OntologyDegrees existNo degrees
⟦tall⟧λd.λx. height(x) ≥ dλx. tall(x) in C
Comparativemax > max∃C. tall(x) ∧ ¬tall(y)
VaguenessThreshold variabilityComparison class var.
Comparison classNot a semantic argumentSemantic argument of pos
Measure phrasesDirect (3 inches of d)Via ≈-classes (§4.2)

@cite{kennedy-2007} argues (§2.2–2.3) that the comparison class is NOT a semantic argument of pos (contra Klein). Instead, the standard is determined by a context-sensitive function s (eq 27) that may draw on domain information descriptively called a "comparison class" but which "does not correspond to a constituent of the logical form" (p. 16).

Klein handles degree modifiers via comparison-class narrowing (§4.1, eqs 42–43) and measure phrases via equivalence classes on a measurement scale (§4.2), though the degree-based treatment is arguably more direct.

For the formal subsumption hierarchy (Klein ← Kennedy ← Measurement), see Theories/Semantics/Comparison/Hierarchy.lean.

@[reducible, inline]

A comparison class: a set of entities relevant for evaluating a gradable predicate. In Klein's framework, this is the only contextual parameter — there are no degrees or thresholds.

Equations
Instances For
    def Semantics.Comparison.Delineation.positiveSem {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (C : ComparisonClass Entity) (x : Entity) :

    Klein's positive form: "Kim is tall" is true iff Kim is in the positive extension of "tall" relative to comparison class C.

    The delineation function partitions entities in C into those that satisfy the predicate and those that don't. The partition can be indeterminate (vagueness = gap between positive and negative extension).

    Equations
    Instances For
      def Semantics.Comparison.Delineation.comparativeSem {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (a b : Entity) :

      Klein's comparative: "Kim is taller than Lee" is true iff there EXISTS a comparison class C such that Kim is tall-in-C but Lee is not tall-in-C.

      This is a supervaluation over comparison classes: the comparative holds when the predicate can discriminate the two entities.

      Equations
      Instances For
        def Semantics.Comparison.Delineation.IsMonotoneDelineation {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (allClasses : Set (ComparisonClass Entity)) :

        Klein's comparative is asymmetric: if a is taller than b, then b is not taller than a.

        This requires the monotonicity constraint on delineations: if a is tall-in-C and b is not, then for any C' where b is tall, a is also tall. Without this constraint, the comparative can fail to be asymmetric.

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

          @cite{klein-1980}'s comparative is the existential dual of @cite{fine-1975}'s supervaluation. Where supervaluation asks "true at ALL specifications?", Klein asks "true at SOME specification where the other is false?" Both quantify over the same space — comparison classes (Klein) = specification points (Fine). The positive form "a is tall" maps to superTrue (delineation · a), and Klein's comparative ∃ C. tall(a,C) ∧ ¬tall(b,C) captures the asymmetry between a's and b's supervaluation status.

          Under monotone delineation, Klein's comparative entails Fine's
          comparative entailment: if b is super-true (tall in every comparison
          class), then a — who is at least as tall — must also be super-true. 
          
          theorem Semantics.Comparison.Delineation.monotone_comparative_superTrue {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) [(C : ComparisonClass Entity) → (x : Entity) → Decidable (delineation C x)] (a b : Entity) (S : Supervaluation.SpecSpace (ComparisonClass Entity)) (hmono : C₁S.admissible, C₂S.admissible, ∀ (x y : Entity), delineation C₁ x¬delineation C₁ ydelineation C₂ ydelineation C₂ x) (hdisc : CS.admissible, delineation C a ¬delineation C b) (hb : Supervaluation.superTrue (fun (C : ComparisonClass Entity) => decide (delineation C b)) S = Core.Duality.Truth3.true) :

          Under monotone delineation, Klein's comparative entails Fine's comparative entailment: if b is super-true, a is super-true.

          The proof extracts the discriminating comparison class C₀ (where a is tall but b isn't), then uses monotonicity: in any class C₂ where b is tall, a must also be tall.

          theorem Semantics.Comparison.Delineation.comparative_prevents_superTrue {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) [(C : ComparisonClass Entity) → (x : Entity) → Decidable (delineation C x)] (a b : Entity) (S : Supervaluation.SpecSpace (ComparisonClass Entity)) (hdisc : CS.admissible, delineation C a ¬delineation C b) :

          Klein's comparative witnesses supervaluation indefiniteness for b: if a is taller than b (∃ discriminating class IN the space), then b is not super-true — the discriminating class falsifies b.

          Klein's partial extension function (§2.3, eq 12). For a vague predicate ζ at context c, F_ζ(c) assigns each entity in the comparison class to the positive extension (some true), negative extension (some false), or the extension gap (none).

          The total delineation in §§1–5 is the special case where every entity receives a definite value (no gap).

          Equations
          Instances For

            Positive extension: pos_ζ(c) = {u ∈ U : F_ζ(c)(u) = 1} (eq 13i).

            Equations
            Instances For

              Negative extension: neg_ζ(c) = {u ∈ U : F_ζ(c)(u) = 0} (eq 13ii).

              Equations
              Instances For

                Extension gap: entities in the comparison class whose truth value is undefined — the borderline cases.

                Equations
                Instances For
                  theorem Semantics.Comparison.Delineation.PartialDelineation.trichotomy {Entity : Type u_1} (d : PartialDelineation Entity) (C : ComparisonClass Entity) (x : Entity) (_hx : x C) (hdom : d C x none) :
                  x d.posExt C x d.negExt C

                  The three zones partition the comparison class: every member is in exactly one of posExt, negExt, or extGap.

                  def Semantics.Comparison.Delineation.ordering {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (cc : ComparisonClass Entity) (u u' : Entity) :

                  Klein's ordering at context c (eq 29): u >_{c,ζ} u' iff there exists a comparison class X ⊆ 𝒰(c) that puts u in the positive extension and u' in the negative extension. The existing comparativeSem is the unrestricted case (𝒰(c) = U).

                  Equations
                  Instances For
                    theorem Semantics.Comparison.Delineation.comparativeSem_eq_ordering_univ {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (a b : Entity) :
                    comparativeSem delineation a b ordering delineation Set.univ a b

                    The unrestricted comparative is the ordering over all of U.

                    theorem Semantics.Comparison.Delineation.ordering_asymm {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (hmono : IsMonotoneDelineation delineation Set.univ) (cc : ComparisonClass Entity) (u v : Entity) :
                    ordering delineation cc u v¬ordering delineation cc v u

                    Klein's ordering is asymmetric under monotone delineation (§3.3, p. 23): if u >{c,ζ} u', then u' ≯{c,ζ} u.

                    theorem Semantics.Comparison.Delineation.ordering_trans {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (hmono : IsMonotoneDelineation delineation Set.univ) (cc : ComparisonClass Entity) (u v w : Entity) :
                    ordering delineation cc u vordering delineation cc v wordering delineation cc u w

                    Klein's ordering is transitive under monotone delineation (§3.3, p. 23): if u >{c,ζ} v and v >{c,ζ} w, then u >_{c,ζ} w.

                    Proof: take X₂ (the class separating v from w). By monotonicity with X₁ separating u from v, u must also be positive in X₂. Since w is negative in X₂, X₂ separates u from w.

                    theorem Semantics.Comparison.Delineation.ordering_neg_trans {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (cc : ComparisonClass Entity) (u v w : Entity) :
                    ordering delineation cc u wordering delineation cc u v ordering delineation cc v w

                    Negative transitivity of the ordering: if u >{c,ζ} w then for any v, either u >{c,ζ} v or v >_{c,ζ} w. No conditions required — follows from excluded middle on delineation X v.

                    This is the key structural property that, combined with asymmetry (from monotonicity), makes the ordering a strict weak order.

                    def Semantics.Comparison.Delineation.nondistinct {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (cc : ComparisonClass Entity) (u u' : Entity) :

                    Two entities are NONDISTINCT w.r.t. ζ at c (eq 30) iff no comparison class containing both can distinguish them.

                    Nondistinctness is reflexive and symmetric but NOT transitive in general. For linear adjectives, nondistinctness collapses to equivalence (eq 40); for nonlinear adjectives it does not — this is what makes clever-type adjectives special.

                    Equations
                    Instances For
                      theorem Semantics.Comparison.Delineation.nondistinct_refl {Entity : Type u_1} {delineation : ComparisonClass EntityEntityProp} {cc : ComparisonClass Entity} {u : Entity} :
                      nondistinct delineation cc u u
                      theorem Semantics.Comparison.Delineation.nondistinct_symm {Entity : Type u_1} {delineation : ComparisonClass EntityEntityProp} {cc : ComparisonClass Entity} {u u' : Entity} (h : nondistinct delineation cc u u') :
                      nondistinct delineation cc u' u
                      theorem Semantics.Comparison.Delineation.nondistinct_of_incomparable {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (cc : ComparisonClass Entity) (u u' : Entity) (hno1 : ¬ordering delineation cc u u') (hno2 : ¬ordering delineation cc u' u) :
                      nondistinct delineation cc u u'

                      Incomparability implies nondistinctness: if neither u > u' nor u' > u in the ordering, then u and u' are nondistinct. No conditions required — follows from excluded middle on delineation.

                      The converse (nondistinct → incomparable) holds under Klein's domain restriction where the ordering additionally requires both entities to be members of the witness class X.

                      def Semantics.Comparison.Delineation.IsLinearDelineation {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) :

                      A delineation is LINEAR (eq 9) iff the ordering it induces is connected: for any two distinct members of a comparison class, either one is ranked above the other or they are nondistinct.

                      Examples: tall, heavy, expensive — single-criterion adjectives that induce total orderings.

                      This is orthogonal to Kennedy's open/closed (RGA/AGA) axis: tall is both linear AND relative-gradable.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Semantics.Comparison.Delineation.IsNonlinearDelineation {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) :

                        A delineation is NONLINEAR iff its ordering can go both ways: there exist u, u' and a comparison class cc such that both u >_{cc} u' and u' >_{cc} u. This happens when different subsets of cc apply different criteria (e.g., math vs. social skills for "clever"), so the delineation is not monotone.

                        For linear adjectives (tall, heavy), monotonicity ensures the ordering is asymmetric; for nonlinear ones (clever, nice), the ordering can cycle. This is orthogonal to Kennedy's open/closed (RGA/AGA) distinction.

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

                          A measure function μ : E → D naturally induces a Klein delineation: entity x is "tall in C" iff x is strictly taller than some member of C. This bridges the degree world (Kennedy) and the degreeless world (Klein): the delineation is determined by the measure, but the semantics never mentions degrees directly.

                          def Semantics.Comparison.Delineation.measureDelineation {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : ED) :
                          ComparisonClass EEProp

                          Delineation induced by a measure function: x is "A-in-C" iff there exists a member of C that x strictly exceeds on μ.

                          Equations
                          Instances For

                            A measure-induced delineation is monotone: if a is tall-in-C₁ and b is not, and b is tall-in-C₂, then a is tall-in-C₂.

                            theorem Semantics.Comparison.Delineation.ordering_implies_degree {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : ED) (cc : ComparisonClass E) (a b : E) :
                            ordering (measureDelineation μ) cc a bμ b < μ a

                            Forward: Klein's ordering entails degree ordering.

                            theorem Semantics.Comparison.Delineation.degree_implies_ordering {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : ED) (cc : ComparisonClass E) (a b : E) (ha : a cc) (hb : b cc) :
                            μ b < μ aordering (measureDelineation μ) cc a b

                            Backward: degree ordering entails Klein's ordering (provided both entities are in the comparison class).

                            theorem Semantics.Comparison.Delineation.ordering_iff_degree {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : ED) (cc : ComparisonClass E) (a b : E) (ha : a cc) (hb : b cc) :
                            ordering (measureDelineation μ) cc a b μ b < μ a

                            Equivalence: Klein's ordering ↔ degree comparison. Justifies Klein's claim that degrees are dispensable (§4.2).

                            A measure-induced delineation is linear: for any two entities in a comparison class, either one ranks above the other or they are nondistinct (equal measure). This connects Klein's typology (§2.2): single-criterion adjectives like "tall" are always linear.

                            Klein handles degree modifiers WITHOUT degrees: very and fairly are comparison-class narrowers. Under the correspondence with degree semantics, narrowing the CC is equivalent to shifting the threshold.

                            def Semantics.Comparison.Delineation.veryDelineation {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (C : ComparisonClass Entity) (x : Entity) :

                            Klein's very (§4.1, eq 42): narrows the comparison class to the positive extension. "Very tall" = tall relative to the tall people.

                            Under the degree correspondence, this is equivalent to raising the threshold from θ to a higher θ' — the threshold for being tall among tall people.

                            Equations
                            Instances For
                              def Semantics.Comparison.Delineation.fairlyDelineation {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (C : ComparisonClass Entity) (x : Entity) :

                              Klein's fairly (§4.1, eq 43): narrows the comparison class to exclude the very-A entities. "Fairly tall" = tall among those who aren't very tall.

                              Equations
                              Instances For
                                theorem Semantics.Comparison.Delineation.very_entails_base {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (hcc : ∀ (C : ComparisonClass Entity) (x : Entity), delineation C xx C) (C : ComparisonClass Entity) (x : Entity) (hv : veryDelineation delineation C x) :
                                delineation C x

                                very entails the base predicate: if x is very-tall-in-C then x is tall-in-C. (The positive extension of very A is a subset of the positive extension of A.)

                                This requires Klein's domain restriction: the delineation only classifies entities that are members of the comparison class. Klein §2.3 eq (12) specifies that F_ζ(c) is a partial function on 𝒰(c), so delineation C x implies x ∈ C. Given this, the proof is immediate: if x is tall among the tall people, then x must be one of the tall people, hence tall in C.

                                For measure-induced delineations (which don't satisfy this domain restriction), very → base holds by a different argument — see Klein1980.measureDelineation_very_entails_base.

                                theorem Semantics.Comparison.Delineation.fairly_excludes_very {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (hcc : ∀ (C : ComparisonClass Entity) (x : Entity), delineation C xx C) (C : ComparisonClass Entity) (x : Entity) (hf : fairlyDelineation delineation C x) :
                                ¬veryDelineation delineation C x

                                fairly excludes very: if x is fairly-A-in-C then x is NOT very-A-in-C. Under domain restriction, being in the fairly-CC requires being outside the very-positive extension.

                                def Semantics.Comparison.Delineation.lessThanSem {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (u u' : Entity) :

                                "u is less A than u'" (§5.3, eq 89a) iff u' is more A than u. Klein shows this follows directly from the symmetry of his comparative, without any special degree machinery.

                                Equations
                                Instances For
                                  def Semantics.Comparison.Delineation.asAsSem {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (u u' : Entity) :

                                  "u is as A as u'" (§5.3, eq 89b) iff in every comparison class where u' is A, u is also A. This is exactly Kamp's atLeastAs from Kamp1975.lean.

                                  Equations
                                  Instances For
                                    theorem Semantics.Comparison.Delineation.more_iff_less {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (a b : Entity) :
                                    comparativeSem delineation a b lessThanSem delineation b a

                                    Klein's equivalences (§5.3, eq 90): the three constructions are interdefinable via classical logic: (a) "A is taller than B" ↔ (b) "B is less tall than A" ↔ (c) "B is not as tall as A".

                                    (a) ↔ (b) is definitional. (a) → ¬(c) uses the existential witness from the comparative to falsify the universal in asAsSem. ¬(c) → (a) is the converse: if "as" fails, there is a discriminating comparison class.

                                    theorem Semantics.Comparison.Delineation.more_implies_not_asAs {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (a b : Entity) (h : comparativeSem delineation a b) :
                                    ¬asAsSem delineation b a
                                    theorem Semantics.Comparison.Delineation.not_asAs_implies_more {Entity : Type u_1} (delineation : ComparisonClass EntityEntityProp) (a b : Entity) (h : ¬asAsSem delineation b a) :
                                    comparativeSem delineation a b