Delineation semantics

import Linglib.Semantics.Degree.Delineation · namespace Degree

In delineation semantics a gradable adjective has no degree argument. A delineation sends each comparison class, a set of entities the adjective is evaluated against, to a positive and a negative extension relative to it. The two are disjoint, and what lies in neither is the extension gap, the borderline cases. a is taller than b holds when some comparison class puts a in the positive extension and b in the negative one; Klein develops this analysis from Kamp's account of the comparative. Within a comparison class C the ordering this induces is a strict partial order as soon as no subclass of C reverses a ranking another subclass makes, Klein's consistency constraint. If moreover every subclass whose members C tells apart has members in both extensions, any two members of C are ranked one way or the other or are nondistinct, so the ordering is linear where nondistinct members are equivalent, that is, where no more determinate delineation tells them apart.

A delineation without gaps is fixed by its positive extensions (Delineation.ofExtension), and nothing is more determinate than it, so it is complete. A measure function induces one, whose ordering within a class is degree comparison. Its positive extension at a class holds what measures above the least member of the class, so the measure embeds the comparative, not the threshold semantics of the positive form.

Main definitions

Degree.Delineation: disjoint positive and negative extensions relative to comparison classes, ordered by determinacy.
Degree.Delineation.ofExtension, Degree.Delineation.IsGapless: the delineations without gaps.
Degree.Delineation.Comparative, Degree.Delineation.Outranks: Klein's comparative and the ordering within a comparison class.
Degree.Delineation.IsMonotoneOn, Degree.Delineation.IsNontrivialOn: Klein's constraints on admissible delineations.
Degree.Delineation.Nondistinct, Degree.Delineation.Equivalent, Degree.Delineation.IsComplete, Degree.Delineation.IsLinear: no subclass tells two entities apart; no more determinate admissible delineation does; the two agree at a class; they agree at every class.
Degree.Delineation.ofMeasure: the delineation a measure function induces.
Degree.Delineation.very, Degree.Delineation.fairly: the modifiers very and fairly.

Main statements

Degree.Delineation.IsMonotoneOn.isStrictOrder_outranks: under the consistency constraint the ordering is a strict partial order.
Degree.Delineation.equivalent_or_outranks_or_outranks: at a complete class meeting the second constraint any two members are equivalent or ranked.
Degree.Delineation.IsGapless.isComplete: a delineation without gaps is complete, and Degree.Delineation.IsGapless.isStrictWeakOrder_outranks: its ordering is a strict weak order.
Degree.Delineation.outranks_ofMeasure_iff: under a measure-induced delineation the ordering is degree comparison.

Implementation notes

The comparison class of Klein's context is the parameter C of Outranks, and his constraints are imposed on the subclasses of C, 𝒫 C. A delineation is not required to leave entities outside a class undecided, Klein's restriction of a valuation to its class; the results that need it assume it. Klein's equivalence quantifies over the contexts at least as determinate as the given one, which are here the delineations of an admissible family 𝒟 extending the given one.

References

Klein 1980, A Semantics for Positive and Comparative Adjectives formalized
Kamp 1975, Two theories about adjectives formalized
Fine 1975, Vagueness, Truth and Logic formalized
Bochnak 2015, The Degree Semantics Parameter and cross-linguistic variation formalized
Burnett 2017, Gradability in Natural Language
Cobreros et al. 2012, Tolerant, Classical, Strict formalized
Kennedy 2011, Vagueness and Comparison
van Rooij 2011a, Implicit versus Explicit Comparatives

Declarations

A delineation sends each comparison class to a positive and a negative extension of a gradable adjective relative to it, which are disjoint; what lies in neither is in the extension gap.

structure Delineation L77–87

(E : Type u_1) :

Type u_1

pos : Set E → Set E
The positive extension relative to a comparison class.
neg : Set E → Set E
The negative extension relative to a comparison class.
disjoint_pos_neg (C : Set E) : Disjoint (self.pos C) (self.neg C)
Nothing is in both extensions.

Used by Delineation.instCoeFunForallSet, Delineation.instPartialOrder, Delineation.le_def, Delineation.notMem_neg_of_mem, Delineation.IsGapless, Delineation.ofExtension, Delineation.IsGapless.mem_neg_iff, Delineation.IsGapless.eq_of_le, Delineation.Comparative, Delineation.Outranks, Delineation.comparative_iff_outranks_univ, Delineation.IsMonotoneOn, Delineation.IsMonotone, Delineation.Nondistinct, Delineation.IsNontrivialOn, Delineation.IsMonotoneOn.mono, Delineation.Nondistinct.refl, Delineation.Nondistinct.symm, Delineation.Outranks.irrefl, Delineation.IsMonotoneOn.outranks_asymm, Delineation.IsMonotoneOn.outranks_trans, Delineation.IsMonotoneOn.isStrictOrder_outranks, Delineation.IsNontrivialOn.nondistinct_or_outranks_or_outranks, Delineation.Equivalent, Delineation.IsComplete, Delineation.IsLinear, Delineation.equivalent_or_outranks_or_outranks, Delineation.IsGapless.isComplete, Delineation.isLinear_of_forall_isGapless, Delineation.IsGapless.nondistinct_of_not_outranks, Delineation.IsGapless.outranks_cotrans, Delineation.IsGapless.isStrictWeakOrder_outranks, Delineation.IsMonotoneOn.supervaluation_eq_true_of_comparative, Delineation.supervaluation_ne_true_of_comparative, Delineation.ofMeasure, Delineation.very, Delineation.fairly, Delineation.very_subset, Delineation.fairly_disjoint_very, Delineation.preorder, Delineation.preorder_le_iff, Delineation.IsSoundFor, Delineation.IsCompleteFor, Delineation.comparative_iff_of_isSoundFor_of_isCompleteFor

Used in Bochnak2015, Klein1980, RudolphKocurek2024

Delineations without gaps

A delineation is gapless when every entity is in the positive or the negative extension of every class.

def Delineation.IsGapless L112–114

{E : Type u_1} (d : Delineation E) :

Prop

d.IsGapless = ∀ (C : Set E), d.neg C = (d.pos C)ᶜ

Built from

Used by Delineation.isGapless_ofExtension, Delineation.IsGapless.mem_neg_iff, Delineation.IsGapless.eq_of_le, Delineation.IsGapless.isComplete, Delineation.isLinear_of_forall_isGapless, Delineation.IsGapless.nondistinct_of_not_outranks, Delineation.IsGapless.outranks_cotrans, Delineation.IsGapless.isStrictWeakOrder_outranks, Delineation.isGapless_ofMeasure

The gapless delineation with the positive extensions f.

def Delineation.ofExtension L116–118

{E : Type u_1} (f : Set E → Set E) :

Delineation E

Delineation.ofExtension f = { pos := f, neg := fun (C : Set E) => (f C)ᶜ, disjoint_pos_neg := ⋯ }

Built from

Used by Delineation.pos_ofExtension, Delineation.neg_ofExtension, Delineation.isGapless_ofExtension, Delineation.isMonotoneOn_ofExtension_iff, Delineation.ofMeasure

Used in Bochnak2015, CarianiSantorioWellwood2023

The comparative

Klein's comparative ((29)) holds of a and b when some comparison class puts a in the positive extension and b in the negative one.

def Delineation.Comparative L146–149

{E : Type u_1} (d : Delineation E) (a b : E) :

Prop

d.Comparative a b = ∃ (C : Set E), a ∈ d.pos C ∧ b ∈ d.neg C

Built from

Used by Delineation.comparative_iff_outranks_univ, Delineation.IsCompleteFor, Delineation.comparative_iff_of_isSoundFor_of_isCompleteFor, Delineation.comparative_ofMeasure_iff

Used in RudolphKocurek2024

Within the comparison class C, u outranks v when some subclass of C puts u in the positive extension and v in the negative one.

def Delineation.Outranks L151–154

{E : Type u_1} (d : Delineation E) (C : Set E) (u v : E) :

Prop

d.Outranks C u v = ∃ X ⊆ C, u ∈ d.pos X ∧ v ∈ d.neg X

Built from

Used by Delineation.comparative_iff_outranks_univ, Delineation.Outranks.irrefl, Delineation.IsMonotoneOn.outranks_asymm, Delineation.IsMonotoneOn.outranks_trans, Delineation.IsMonotoneOn.isStrictOrder_outranks, Delineation.IsNontrivialOn.nondistinct_or_outranks_or_outranks, Delineation.equivalent_or_outranks_or_outranks, Delineation.IsGapless.nondistinct_of_not_outranks, Delineation.IsGapless.outranks_cotrans, Delineation.IsGapless.isStrictWeakOrder_outranks, Delineation.outranks_ofMeasure_iff

Used in Klein1980, VonStechow1984

L156–157

Klein's constraints

A delineation is monotone on a set of comparison classes, Klein's consistency constraint ((37)), when once a class in the set puts a in the positive and b in the negative extension, no class in the set puts b in the positive extension without a, or a in the negative extension without b.

def Delineation.IsMonotoneOn L161–167

{E : Type u_1} (d : Delineation E) (S : Set (Set E)) :

Prop

d.IsMonotoneOn S = ∀ C₁ ∈ S, ∀ C₂ ∈ S, ∀ (a b : E), a ∈ d.pos C₁ → b ∈ d.neg C₁ → (b ∈ d.pos C₂ → a ∈ d.pos C₂) ∧ (a ∈ d.neg C₂ → b ∈ d.neg C₂)

Built from

Used by Delineation.IsMonotone, Delineation.IsMonotoneOn.mono, Delineation.isMonotoneOn_ofExtension_iff, Delineation.IsMonotoneOn.outranks_asymm, Delineation.IsMonotoneOn.outranks_trans, Delineation.IsMonotoneOn.isStrictOrder_outranks, Delineation.IsGapless.isStrictWeakOrder_outranks, Delineation.IsMonotoneOn.supervaluation_eq_true_of_comparative

Used in CarianiSantorioWellwood2023, Klein1980

L169–170

Two entities are nondistinct in C ((30)) when every subclass of C containing both gives them the same value: both positive, both negative, or both in the gap.

def Delineation.Nondistinct L172–175

{E : Type u_1} (d : Delineation E) (C : Set E) (u v : E) :

Prop

d.Nondistinct C u v = ∀ X ⊆ C, u ∈ X → v ∈ X → (u ∈ d.pos X ↔ v ∈ d.pos X) ∧ (u ∈ d.neg X ↔ v ∈ d.neg X)

Built from

Used by Delineation.IsNontrivialOn, Delineation.Nondistinct.refl, Delineation.Nondistinct.symm, Delineation.IsNontrivialOn.nondistinct_or_outranks_or_outranks, Delineation.Equivalent, Delineation.IsComplete, Delineation.IsGapless.nondistinct_of_not_outranks

Used in Klein1980

A delineation is nontrivial on C, Klein's condition (36), when every subclass of C with two members that are not nondistinct in C has a member in its positive and a member in its negative extension.

def Delineation.IsNontrivialOn L177–182

{E : Type u_1} (d : Delineation E) (C : Set E) :

Prop

d.IsNontrivialOn C = ∀ X ⊆ C, (∃ u ∈ X, ∃ v ∈ X, ¬d.Nondistinct C u v) → (∃ w ∈ X, w ∈ d.pos X) ∧ ∃ w ∈ X, w ∈ d.neg X

Built from ,

Used by Delineation.IsNontrivialOn.nondistinct_or_outranks_or_outranks, Delineation.equivalent_or_outranks_or_outranks

Used in Klein1980

The ordering within a comparison class

L208–209

L211–213

L215–217

Under the consistency constraint the ordering within a class is a strict partial order. Klein derives this from both of his constraints (p. 23); the consistency constraint suffices.

theorem Delineation.IsMonotoneOn.isStrictOrder_outranks L219–224

{E : Type u_1} {d : Delineation E} {C : Set E} (hm : d.IsMonotoneOn (𝒫 C)) :

IsStrictOrder E (d.Outranks C)

Built from , ,

L226–240

Equivalence and completeness

Two entities are equivalent in C relative to a family 𝒟 of admissible delineations ((33)), exactly as A as each other, when every delineation of 𝒟 at least as determinate as d leaves them nondistinct.

def Delineation.Equivalent L245–249

{E : Type u_1} (d : Delineation E) (𝒟 : Set (Delineation E)) (C : Set E) (u v : E) :

Prop

d.Equivalent 𝒟 C u v = ∀ d' ∈ 𝒟, d ≤ d' → d'.Nondistinct C u v

Built from ,

Used by Delineation.IsComplete, Delineation.equivalent_or_outranks_or_outranks

Used in Klein1980

A delineation is complete at C ((39)) when the members of C it leaves nondistinct are equivalent.

def Delineation.IsComplete L252–255

{E : Type u_1} (d : Delineation E) (𝒟 : Set (Delineation E)) (C : Set E) :

Prop

d.IsComplete 𝒟 C = ∀ u ∈ C, ∀ v ∈ C, d.Nondistinct C u v → d.Equivalent 𝒟 C u v

Built from , ,

Used by Delineation.IsLinear, Delineation.equivalent_or_outranks_or_outranks, Delineation.IsGapless.isComplete

Used in Klein1980

An adjective interpreted by the family 𝒟 of delineations is linear when each of them is complete at every comparison class, as single-criterion adjectives such as tall are.

def Delineation.IsLinear L257–259

{E : Type u_1} (𝒟 : Set (Delineation E)) :

Prop

Delineation.IsLinear 𝒟 = ∀ d ∈ 𝒟, ∀ (C : Set E), d.IsComplete 𝒟 C

Built from ,

Used by Delineation.isLinear_of_forall_isGapless

Used in Klein1980

At a class where the delineation is complete and meets Klein's condition (36), any two members are equivalent or ranked one way or the other: the ordering is connected up to equivalence, and with the consistency constraint it is linear (Klein 1980, p. 25).

theorem Delineation.equivalent_or_outranks_or_outranks L261–267

{E : Type u_1} {d : Delineation E} {C : Set E} {u v : E} {𝒟 : Set (Delineation E)} (hc : d.IsComplete 𝒟 C) (hs : d.IsNontrivialOn C) (hu : u ∈ C) (hv : v ∈ C) :

d.Equivalent 𝒟 C u v ∨ d.Outranks C u v ∨ d.Outranks C v u

Built from , , , ,

A gapless delineation is complete: nothing is more determinate than it.

theorem Delineation.IsGapless.isComplete L269–273

{E : Type u_1} {d : Delineation E} (hd : d.IsGapless) (𝒟 : Set (Delineation E)) (C : Set E) :

d.IsComplete 𝒟 C

Built from , ,

L275–277

L279–285

L287–293

On a gapless delineation under the consistency constraint the ordering is a strict weak order, the order a degree scale would give.

theorem Delineation.IsGapless.isStrictWeakOrder_outranks L295–303

{E : Type u_1} {d : Delineation E} {C : Set E} (hd : d.IsGapless) (hm : d.IsMonotoneOn (𝒫 C)) :

IsStrictWeakOrder E (d.Outranks C)

Built from , , ,

The Fine duality

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

L314–320

L323–326

The delineation of a measure

ofMeasure maps threshold semantics into delineation semantics, and outranks_ofMeasure_iff says the map is faithful to the comparative.

The delineation a measure induces is gapless and puts x in the positive extension relative to C when x measures strictly more than some member of C.

def Delineation.ofMeasure L339–341

{E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) :

Delineation E

Delineation.ofMeasure μ = Delineation.ofExtension fun (C : Set E) => {x : E | ∃ y ∈ C, μ y < μ x}

Built from ,

Used by Delineation.mem_ofMeasure, Delineation.mem_neg_ofMeasure, Delineation.isGapless_ofMeasure, Delineation.isMonotone_ofMeasure, Delineation.monotone_ofMeasure, Delineation.outranks_ofMeasure_iff, Delineation.isSoundFor_ofMeasure, Delineation.isCompleteFor_ofMeasure, Delineation.comparative_ofMeasure_iff

Used in Bochnak2015, Klein1980, VonStechow1984

Under a measure-induced delineation, the ordering of two members of a comparison class is degree comparison.

theorem Delineation.outranks_ofMeasure_iff L360–368

{E : Type u_1} {C : Set E} {D : Type u_2} [LinearOrder D] (μ : E → D) {a b : E} (ha : a ∈ C) (hb : b ∈ C) :

(ofMeasure μ).Outranks C a b ↔ μ b < μ a

Built from ,

Degree modifiers as narrowings of the comparison class

Klein's very A ((42)) evaluates A relative to the members of C that A holds of.

def Delineation.very L375–377

{E : Type u_1} (d : Delineation E) :

Delineation E

d.very = { pos := fun (C : Set E) => d.pos (d.pos C), neg := fun (C : Set E) => d.neg (d.pos C), disjoint_pos_neg := ⋯ }

Built from

Used by Delineation.fairly, Delineation.very_subset, Delineation.fairly_disjoint_very

Used in Klein1980

Klein's fairly A ((43)) evaluates A relative to the members of C that very A does not hold of.

def Delineation.fairly L380–384

{E : Type u_1} (d : Delineation E) :

Delineation E

d.fairly = { pos := fun (C : Set E) => d.pos (C \ d.very.pos C), neg := fun (C : Set E) => d.neg (C \ d.very.pos C), disjoint_pos_neg := ⋯ }

Built from ,

Used by Delineation.fairly_disjoint_very

L386–387

L389–390

The equative

L395–398

L400

Faithfulness to a scalar relation

A delineation is sound for a scalar relation R when separation by a comparison class entails R, which is Bochnak's second consistency constraint; it is complete when every pair related by R is separated by some class, closer to Burnett's axioms. Both are classical: under the tolerant semantics of Cobreros and colleagues, similar pairs would defeat strict separation.