Sauerland & Stateva (2011): Two Types of Vagueness

Sauerland and Stateva argue from the distribution of approximators that vagueness comes in two kinds. Scalar vagueness belongs to terms that denote a point on a scale, such as numerals: a contextual granularity maps the point to an interval around it, after Krifka, and scalar approximators such as exactly and approximately reset the granularity to the finest or the coarsest available one. Epistemic vagueness belongs to terms like heap, whose extension varies across indistinguishable worlds, and epistemic approximators quantify over those worlds. Within the scalar class, absolutely, completely and more or less take only scale endpoints and block exactly and approximately there.

Main results

• SauerlandStateva2011.classification_predicts_distribution: the two-type classification reproduces every cited judgment.
• SauerlandStateva2011.exactly_narrowest, SauerlandStateva2011.approximately_widest: at a degree that is a scale point of every available granularity, exactly yields the narrowest reading and approximately the widest, (19).
• SauerlandStateva2011.second_reset_vacuous: a second scalar approximator is vacuous, §6.3.5.

Implementation notes

Granularities are the grains Degree.grain, identified by their widths, and the interval a term denotes is the cell of its degree. Cells are half-open so that they partition the scale; the chapter writes them closed, (12)–(13). The examples at the end check the intervals of (13) and the oddity of (20).

References

• [SS11]
• [Kri07a]
• [Las99]

The two-vagueness classification (§6.3)

inductive SauerlandStateva2011.Item : Type

Their example expressions ((4)–(6), (35), (37), (44)–(45)).

• fifty : Item
• three : Item
• dry : Item
• full : Item
• beefStroganoff : Item

@[instance_reducible]

instance SauerlandStateva2011.instDecidableEqItem : DecidableEq Item

Equations

• SauerlandStateva2011.instDecidableEqItem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SauerlandStateva2011.instReprItem : Repr Item

Equations

• SauerlandStateva2011.instReprItem = { reprPrec := SauerlandStateva2011.instReprItem.repr }

def SauerlandStateva2011.instReprItem.repr : Item → ℕ → Std.Format

Equations

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

inductive SauerlandStateva2011.ItemClass : Type

The dualistic theory classifies scalar terms as denoting scale points, non-endpoints (numerals) or endpoints (dry, full, the closed-scale adjectives of §6.4), and epistemically vague terms as denoting no point at all.

• scalarNonEndpoint : ItemClass
• scalarEndpoint : ItemClass
• epistemic : ItemClass

@[instance_reducible]

instance SauerlandStateva2011.instDecidableEqItemClass : DecidableEq ItemClass

Equations

• SauerlandStateva2011.instDecidableEqItemClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SauerlandStateva2011.instReprItemClass : Repr ItemClass

Equations

• SauerlandStateva2011.instReprItemClass = { reprPrec := SauerlandStateva2011.instReprItemClass.repr }

def SauerlandStateva2011.instReprItemClass.repr : ItemClass → ℕ → Std.Format

Equations

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

def SauerlandStateva2011.Item.itemClass : Item → ItemClass

Their classification of the example items.

Equations

• SauerlandStateva2011.Item.fifty.itemClass = SauerlandStateva2011.ItemClass.scalarNonEndpoint
• SauerlandStateva2011.Item.three.itemClass = SauerlandStateva2011.ItemClass.scalarNonEndpoint
• SauerlandStateva2011.Item.dry.itemClass = SauerlandStateva2011.ItemClass.scalarEndpoint
• SauerlandStateva2011.Item.full.itemClass = SauerlandStateva2011.ItemClass.scalarEndpoint
• SauerlandStateva2011.Item.beefStroganoff.itemClass = SauerlandStateva2011.ItemClass.epistemic

inductive SauerlandStateva2011.Approximator : Type

The approximators whose distribution they cite.

• exactly : Approximator
• approximately : Approximator
• absolutely : Approximator
• completely : Approximator
• moreOrLess : Approximator

@[instance_reducible]

instance SauerlandStateva2011.instDecidableEqApproximator : DecidableEq Approximator

Equations

• SauerlandStateva2011.instDecidableEqApproximator x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SauerlandStateva2011.instReprApproximator : Repr Approximator

Equations

• SauerlandStateva2011.instReprApproximator = { reprPrec := SauerlandStateva2011.instReprApproximator.repr }

def SauerlandStateva2011.instReprApproximator.repr : Approximator → ℕ → Std.Format

Equations

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

def SauerlandStateva2011.Approximator.selects : Approximator → ItemClass

Plain scalar approximators select non-endpoints, and the endpoint approximators absolutely, completely and more or less, which make endpoints more or less precise and block exactly and approximately there, select endpoints, §6.4 and (32).

Equations

• SauerlandStateva2011.Approximator.exactly.selects = SauerlandStateva2011.ItemClass.scalarNonEndpoint
• SauerlandStateva2011.Approximator.approximately.selects = SauerlandStateva2011.ItemClass.scalarNonEndpoint
• SauerlandStateva2011.Approximator.absolutely.selects = SauerlandStateva2011.ItemClass.scalarEndpoint
• SauerlandStateva2011.Approximator.completely.selects = SauerlandStateva2011.ItemClass.scalarEndpoint
• SauerlandStateva2011.Approximator.moreOrLess.selects = SauerlandStateva2011.ItemClass.scalarEndpoint

def SauerlandStateva2011.compatible (a : Approximator) (i : Item) : Prop

The theory predicts that an approximator combines with an item exactly when the item is of the class the approximator selects.

Equations

• SauerlandStateva2011.compatible a i = (a.selects = i.itemClass)

@[instance_reducible]

instance SauerlandStateva2011.instDecidableCompatible (a : Approximator) (i : Item) : Decidable (compatible a i)

Equations

• SauerlandStateva2011.instDecidableCompatible a i = SauerlandStateva2011.instDecidableCompatible._aux_1 a i

structure SauerlandStateva2011.Judgment : Type

One cited acceptability judgment.

• approximator : Approximator
• item : Item
• acceptable : Bool

@[instance_reducible]

instance SauerlandStateva2011.instReprJudgment : Repr Judgment

Equations

• SauerlandStateva2011.instReprJudgment = { reprPrec := SauerlandStateva2011.instReprJudgment.repr }

def SauerlandStateva2011.instReprJudgment.repr : Judgment → ℕ → Std.Format

Equations

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

def SauerlandStateva2011.Judgment.rows : List Judgment

The cited judgments are (4a)/(4b) exactly/approximately fifty vs #…Beef Stroganoff; (6a)/(6b) *absolutely fifty vs absolutely + endpoint; (35a)/(35b) #exactly dry/full vs exactly three; (37) completely dry vs #completely three; (44) approximately three vs #…dry; and (45) more or less dry vs #…three.

Equations

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

theorem SauerlandStateva2011.classification_predicts_distribution (j : Judgment) : j ∈ Judgment.rows → (compatible j.approximator j.item ↔ j.acceptable = true)

The two-type classification reproduces every cited judgment, an approximator being acceptable exactly with the class it selects; this is the dualism argument.

Granularity setting, (12)–(20)

theorem SauerlandStateva2011.exactly_narrowest {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (𝒢 : Finset α) (h𝒢 : 𝒢.Nonempty) {d ε : α} (hpos : ∀ ε ∈ 𝒢, 0 < ε) (hd : ∀ ε ∈ 𝒢, d ∈ AddSubgroup.zmultiples ε) (hε : ε ∈ 𝒢) : (Degree.grain (𝒢.min' h𝒢)).cell d ⊆ (Degree.grain ε).cell d

At a degree that is a scale point of every available granularity, as 5 meters is in Figure 6.1, exactly yields the narrowest available reading, (19a), since the cell at the finest width lies inside the cell at every available one.

theorem SauerlandStateva2011.approximately_widest {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (𝒢 : Finset α) (h𝒢 : 𝒢.Nonempty) {d ε : α} (hpos : ∀ ε ∈ 𝒢, 0 < ε) (hd : ∀ ε ∈ 𝒢, d ∈ AddSubgroup.zmultiples ε) (hε : ε ∈ 𝒢) : (Degree.grain ε).cell d ⊆ (Degree.grain (𝒢.max' h𝒢)).cell d

At a degree that is a scale point of every available granularity, approximately yields the widest available reading, (19b).

theorem SauerlandStateva2011.second_reset_vacuous {β : Type u_2} [LinearOrder β] (ε : β) : {ε}.min' ⋯ = ε ∧ {ε}.max' ⋯ = ε

A second scalar approximator is vacuous, §6.3.5, since the first resets the granularities to a single one, which either reset returns.

(13): 5 meters at 1 m, 4 meters 50 at 50 cm, and 4 meters 90 at 10 cm.

(20): at a coarsest width of ten, 49 and 50 share a cell, which the shorter 50 denotes, so approximately 49 is odd.