Klein's delineation semantics

[Kle80] [Kam75] [Ken07]

Degree-free gradability: a gradable adjective is a predicate whose extension varies with a contextually supplied comparison class, and the comparative holds when some class discriminates the two entities ([Kle80], formalizing [Kam75]'s definition (12)). The rival threshold analysis is Degree/Basic.lean; the representation maps between them and the strict-separation theorem are in Degree/Hom.lean.

Main definitions

• comparativeSem — Klein's comparative: ∃ C, tall(a, C) ∧ ¬tall(b, C).
• IsMonotoneDelineation — [Boc15a]'s Consistency Constraint a.
• PartialDelineation — extension gaps (Klein §2.3, eqs 12–13).
• ordering, nondistinct — the context-relative comparison and indistinguishability relations (§3.3, eqs 29–30).
• IsLinearDelineation, IsNonlinearDelineation — single- vs multi-criteria adjectives (§2.2 eq 9; tall vs clever).
• measureDelineation — the delineation a measure function induces.
• veryDelineation, fairlyDelineation — degree modifiers as comparison-class narrowers (§4.1, eqs 42–43).
• kleinPreorder — as A as (§5.3, eq 89b; Kamp's definition 12).
• IsSoundDelineation, IsCompleteDelineation — faithfulness to an abstract scalar relation ([Boc15a] eq (28b) and its converse).

Main results

• ordering_asymm, ordering_trans, ordering_neg_trans — under monotonicity the ordering is a strict weak order (§3.3, p. 23).
• ordering_iff_degree — measure-induced delineations are faithful: Klein's ordering is exactly degree comparison (§4.2).
• comparativeSem_iff_of_sound_and_complete — the comparative coincides with any scalar relation the delineation is sound and complete for.
• monotone_comparative_superTrue, comparative_prevents_superTrue — the [Fin75] duality: comparison classes are specification points.

@[reducible, inline]

abbrev Degree.Delineation.ComparisonClass (Entity : Type u_1) : Type u_1

A comparison class: the set of entities a gradable predicate is evaluated against — Klein's only contextual parameter.

Equations

• Degree.Delineation.ComparisonClass Entity = Set Entity

The comparative

def Degree.Delineation.comparativeSem {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (a b : Entity) : Prop

Klein's comparative: some comparison class discriminates a from b.

Equations

• Degree.Delineation.comparativeSem delineation a b = ∃ (C : Degree.Delineation.ComparisonClass Entity), delineation C a ∧ ¬delineation C b

def Degree.Delineation.IsMonotoneDelineation {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (allClasses : Set (ComparisonClass Entity)) : Prop

Monotone delineation ([Boc15a] eq (28a), Consistency Constraint a): a class that ranks a above b is never contradicted by another class. Forces asymmetry of the comparative.

Equations

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

The Fine duality

Comparison classes are specification points: Klein's comparative is the existential dual of [Fin75]'s supervaluation.

theorem Degree.Delineation.monotone_comparative_superTrue {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) [(C : ComparisonClass Entity) → (x : Entity) → Decidable (delineation C x)] (a b : Entity) (S : Semantics.Supervaluation.SpecSpace (ComparisonClass Entity)) (hmono : ∀ C₁ ∈ S.admissible, ∀ C₂ ∈ S.admissible, ∀ (x y : Entity), delineation C₁ x → ¬delineation C₁ y → delineation C₂ y → delineation C₂ x) (hdisc : ∃ C ∈ S.admissible, delineation C a ∧ ¬delineation C b) (hb : Semantics.Supervaluation.superTrue (fun (C : ComparisonClass Entity) => decide (delineation C b) = true) S = Trivalent.true) : Semantics.Supervaluation.superTrue (fun (C : ComparisonClass Entity) => decide (delineation C a) = true) S = Trivalent.true

Under monotone delineation, a discriminating class carries super-truth upward: if b is tall in every admissible class, so is the a that outranks it.

theorem Degree.Delineation.comparative_prevents_superTrue {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) [(C : ComparisonClass Entity) → (x : Entity) → Decidable (delineation C x)] (a b : Entity) (S : Semantics.Supervaluation.SpecSpace (ComparisonClass Entity)) (hdisc : ∃ C ∈ S.admissible, delineation C a ∧ ¬delineation C b) : Semantics.Supervaluation.superTrue (fun (C : ComparisonClass Entity) => decide (delineation C b) = true) S ≠ Trivalent.true

A discriminating class in the space falsifies b's super-truth.

Partial extensions (Klein §2.3, eqs 12–13)

def Degree.Delineation.PartialDelineation (Entity : Type u_2) : Type u_2

Klein's partial extension function: each entity lands in the positive extension (some true), negative extension (some false), or the gap (none). The total delineation elsewhere in this file is the gap-free special case.

Equations

• Degree.Delineation.PartialDelineation Entity = (Degree.Delineation.ComparisonClass Entity → Entity → Option Bool)

def Degree.Delineation.PartialDelineation.posExt {Entity : Type u_1} (d : PartialDelineation Entity) (C : ComparisonClass Entity) : Set Entity

Positive extension (eq 13i).

Equations

• d.posExt C = {x : Entity | d C x = some true}

def Degree.Delineation.PartialDelineation.negExt {Entity : Type u_1} (d : PartialDelineation Entity) (C : ComparisonClass Entity) : Set Entity

Negative extension (eq 13ii).

Equations

• d.negExt C = {x : Entity | d C x = some false}

def Degree.Delineation.PartialDelineation.extGap {Entity : Type u_1} (d : PartialDelineation Entity) (C : ComparisonClass Entity) : Set Entity

The extension gap: borderline cases.

Equations

• d.extGap C = {x : Entity | x ∈ C ∧ d C x = none}

theorem Degree.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

Gap-free members fall in the positive or negative extension.

The context-relative ordering (Klein §3.3, eqs 29–30)

def Degree.Delineation.ordering {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (cc : ComparisonClass Entity) (u u' : Entity) : Prop

Klein's ordering at a context (eq 29): some subclass of cc puts u in the positive and u' in the negative extension.

Equations

• Degree.Delineation.ordering delineation cc u u' = ∃ X ⊆ cc, delineation X u ∧ ¬delineation X u'

theorem Degree.Delineation.comparativeSem_eq_ordering_univ {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (a b : Entity) : comparativeSem delineation a b ↔ ordering delineation Set.univ a b

comparativeSem is the ordering over the universal class.

theorem Degree.Delineation.ordering_asymm {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) {cc : ComparisonClass Entity} {u v : Entity} (hmono : IsMonotoneDelineation delineation Set.univ) : ordering delineation cc u v → ¬ordering delineation cc v u

Under monotonicity the ordering is asymmetric (§3.3, p. 23).

theorem Degree.Delineation.ordering_trans {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) {cc : ComparisonClass Entity} {u v w : Entity} (hmono : IsMonotoneDelineation delineation Set.univ) : ordering delineation cc u v → ordering delineation cc v w → ordering delineation cc u w

Under monotonicity the ordering is transitive (§3.3, p. 23).

theorem Degree.Delineation.ordering_neg_trans {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) {cc : ComparisonClass Entity} {u v w : Entity} : ordering delineation cc u w → ordering delineation cc u v ∨ ordering delineation cc v w

Negative transitivity, with no side conditions: together with asymmetry this makes the ordering a strict weak order.

def Degree.Delineation.nondistinct {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (cc : ComparisonClass Entity) (u u' : Entity) : Prop

Nondistinctness (eq 30): no subclass containing both can distinguish them. Reflexive and symmetric; transitive only for linear adjectives (eq 40).

Equations

• Degree.Delineation.nondistinct delineation cc u u' = ∀ X ⊆ cc, u ∈ X → u' ∈ X → (delineation X u ↔ delineation X u')

theorem Degree.Delineation.nondistinct_refl {Entity : Type u_1} {delineation : ComparisonClass Entity → Entity → Prop} {cc : ComparisonClass Entity} {u : Entity} : nondistinct delineation cc u u

theorem Degree.Delineation.nondistinct_symm {Entity : Type u_1} {delineation : ComparisonClass Entity → Entity → Prop} {cc : ComparisonClass Entity} {u v : Entity} (h : nondistinct delineation cc u v) : nondistinct delineation cc v u

theorem Degree.Delineation.nondistinct_of_incomparable {Entity : Type u_1} {delineation : ComparisonClass Entity → Entity → Prop} {cc : ComparisonClass Entity} {u v : Entity} (hno1 : ¬ordering delineation cc u v) (hno2 : ¬ordering delineation cc v u) : nondistinct delineation cc u v

Incomparable entities are nondistinct. The converse holds under Klein's domain restriction (witness classes contain both entities).

Linear and nonlinear adjectives (Klein §2.2 eq 9, §3.3)

def Degree.Delineation.IsLinearDelineation {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) : Prop

Linear (eq 9): any two class-mates are ordered or nondistinct — single-criterion adjectives (tall, heavy). Orthogonal to Kennedy's relative/absolute axis.

Equations

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

def Degree.Delineation.IsNonlinearDelineation {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) : Prop

Nonlinear: the ordering cycles — different subclasses apply different criteria (clever, nice). No measure function induces such a delineation (Degree/Hom.lean, delineation_strictly_more_general).

Equations

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

Morphisms

measureDelineation maps threshold-degree semantics into delineation semantics; ordering_iff_degree is its faithfulness. Strictness — some delineations come from no measure — and the composite from typed measurement live in Degree/Hom.lean.

def Degree.Delineation.measureDelineation {E : Type u_2} {D : Type u_3} [LinearOrder D] (μ : E → D) : ComparisonClass E → E → Prop

The delineation a measure induces: x qualifies in C iff it strictly exceeds some member of C.

Equations

• Degree.Delineation.measureDelineation μ C x = ∃ y ∈ C, μ y < μ x

theorem Degree.Delineation.measureDelineation_monotone {E : Type u_2} {D : Type u_3} [LinearOrder D] (μ : E → D) : IsMonotoneDelineation (measureDelineation μ) Set.univ

Measure-induced delineations are monotone.

theorem Degree.Delineation.measureDelineation_mono_in_class {E : Type u_2} {D : Type u_3} [LinearOrder D] (μ : E → D) (x : E) : Monotone fun (C : ComparisonClass E) => measureDelineation μ C x

For fixed x, membership is Monotone in the class: larger classes only add witnesses. General delineations are not — that is the point of nonlinear adjectives.

theorem Degree.Delineation.ordering_implies_degree {E : Type u_2} {D : Type u_3} [LinearOrder D] (μ : E → D) (cc : ComparisonClass E) (a b : E) : ordering (measureDelineation μ) cc a b → μ b < μ a

Klein's ordering entails degree comparison.

theorem Degree.Delineation.degree_implies_ordering {E : Type u_2} {D : Type u_3} [LinearOrder D] (μ : E → D) (cc : ComparisonClass E) (a b : E) (ha : a ∈ cc) (hb : b ∈ cc) : μ b < μ a → ordering (measureDelineation μ) cc a b

Degree comparison entails Klein's ordering for class-mates, with the two-element class {a, b} as witness.

theorem Degree.Delineation.ordering_iff_degree {E : Type u_2} {D : Type u_3} [LinearOrder D] (μ : E → D) (cc : ComparisonClass E) (a b : E) (ha : a ∈ cc) (hb : b ∈ cc) : ordering (measureDelineation μ) cc a b ↔ μ b < μ a

Faithfulness: Klein's ordering under the induced delineation is exactly degree comparison — degrees are dispensable (§4.2).

theorem Degree.Delineation.measureDelineation_is_linear {E : Type u_2} {D : Type u_3} [LinearOrder D] (μ : E → D) : IsLinearDelineation (measureDelineation μ)

Measure-induced delineations are linear.

Degree modifiers as class narrowers (Klein §4.1, eqs 42–43)

def Degree.Delineation.veryDelineation {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (C : ComparisonClass Entity) (x : Entity) : Prop

Klein's very (eq 42): tall relative to the tall people — the class narrows to the positive extension.

Equations

• Degree.Delineation.veryDelineation delineation C x = delineation {u : Entity | delineation C u} x

def Degree.Delineation.fairlyDelineation {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (C : ComparisonClass Entity) (x : Entity) : Prop

Klein's fairly (eq 43): tall among those not very tall.

Equations

• Degree.Delineation.fairlyDelineation delineation C x = delineation {u : Entity | u ∈ C ∧ u ∉ {u : Entity | delineation {v : Entity | delineation C v} u}} x

theorem Degree.Delineation.very_entails_base {Entity : Type u_1} {delineation : ComparisonClass Entity → Entity → Prop} {C : ComparisonClass Entity} {x : Entity} (hcc : ∀ (C : ComparisonClass Entity) (x : Entity), delineation C x → x ∈ C) (hv : veryDelineation delineation C x) : delineation C x

very A entails A, given Klein's domain restriction (eq 12: only class members are classified). For measure-induced delineations see Klein1980.measureDelineation_very_entails_base.

theorem Degree.Delineation.fairly_excludes_very {Entity : Type u_1} {delineation : ComparisonClass Entity → Entity → Prop} {C : ComparisonClass Entity} {x : Entity} (hcc : ∀ (C : ComparisonClass Entity) (x : Entity), delineation C x → x ∈ C) (hf : fairlyDelineation delineation C x) : ¬veryDelineation delineation C x

fairly A excludes very A.

The Kamp preorder (Klein §5.3, eq 89b)

@[reducible]

def Degree.Delineation.kleinPreorder {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) : Preorder Entity

as A as : u ≤ v iff every class where v qualifies also qualifies u ([Kam75] definition 12). Under monotone delineation its strict part is comparativeSem.

Equations

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

Faithfulness to a scalar relation

Soundness is [Boc15a] eq (28b) (Consistency Constraint b, cf. [Kle80] [Ken11] [vR11]); completeness is its converse (closer to [Bur17]'s Plenitude/Granularity axioms — [Boc15a]'s footnote 11 notes the one-directional character). CC-b is strict-classical: under [CERvR12]'s tolerant semantics, similar pairs would defeat strict separation.

class Degree.Delineation.IsSoundDelineation {Entity : Type u_1} (del : ComparisonClass Entity → Entity → Prop) (R : Entity → Entity → Prop) : Prop

Sound w.r.t. a scalar relation R: per-class separation entails R.

• sound (C : ComparisonClass Entity) (x y : Entity) : del C x → ¬del C y → R x y

  Per-context separation implies the scalar relation.

class Degree.Delineation.IsCompleteDelineation {Entity : Type u_1} (del : ComparisonClass Entity → Entity → Prop) (R : Entity → Entity → Prop) : Prop

Complete w.r.t. R: every R-distinguished pair admits a discriminating class.

• complete (x y : Entity) : R x y → ∃ (C : ComparisonClass Entity), del C x ∧ ¬del C y

  R-distinguished pairs admit a discriminating context.

theorem Degree.Delineation.comparativeSem_iff_of_sound_and_complete {Entity : Type u_1} {del : ComparisonClass Entity → Entity → Prop} {R : Entity → Entity → Prop} [hSound : IsSoundDelineation del R] [hComplete : IsCompleteDelineation del R] {x y : Entity} : comparativeSem del x y ↔ R x y

comparativeSem coincides with any scalar relation the delineation is sound and complete for — the comparison entailment without a measure function in the lexical entry.

instance Degree.Delineation.instSoundMeasureDelineation {E : Type u_2} {D : Type u_3} [LinearOrder D] (μ : E → D) : IsSoundDelineation (measureDelineation μ) fun (a b : E) => μ b < μ a

instance Degree.Delineation.instCompleteMeasureDelineation {E : Type u_2} {D : Type u_3} [LinearOrder D] (μ : E → D) : IsCompleteDelineation (measureDelineation μ) fun (a b : E) => μ b < μ a