[SS11]: Two Types of Vagueness

[SS11] [Kri07a] [Las99]

[SS11] argue from the distribution of approximators that vagueness comes in two kinds: scalar (point-denoting scalar terms — numerals, 6 o'clock — interpreted at a contextual granularity, following [Kri07a]) and epistemic (heap, Beef Stroganoff — extension varies across indistinguishable worlds). Scalar approximators (exactly, approximately, completely, more or less) are granularity setters: their (19) resets the context's granularity parameter to the finest (exactly) or coarsest (approximately) available level — here Degree.Granularity.finestWidth/coarsestWidth. Epistemic approximators (definitely, maybe) quantify over worlds instead, which is why the two classes distribute complementarily (their §6.2, §6.4) — the argument the distribution table below reproduces. Their §6.3.5: stacked scalar approximators are vacuous, since the first reset leaves a singleton granularity set — second_reset_vacuous.

Within the scalar class, endpoint-approximators (absolutely, completely, more or less) combine only with scale endpoints, blocking plain exactly/approximately there (their §6.4, (32), (35)–(45)).

Main definitions

• Item, ItemClass: their example expressions and the two-vagueness classification
• Approximator, Approximator.selects: the approximator inventory and which item class each selects
• Judgment.rows: their cited acceptability judgments ((4)–(6), (35), (37), (44)–(45))

Main results

• classification_predicts_distribution: the two-type theory reproduces every cited judgment
• exactly_narrowest, approximately_widest: the reset targets bound all available interpretations (their (19), via finestWidth_le/ le_coarsestWidth and finer_contained)
• second_reset_vacuous: approximator stacking is vacuous (their §6.3.5)
• fragment_setter_directions: the English.NumeralModifiers entries carry the setter classification

The two-vagueness classification (their §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

@[implicit_reducible]

instance SauerlandStateva2011.instDecidableEqItem : DecidableEq Item

Equations

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

@[implicit_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 classification the dualistic theory assigns: scalar terms denote scale points — non-endpoints (numerals) or endpoints (dry, full, their §6.4 closed-scale adjectives) — while epistemically vague terms denote no point at all.

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

@[implicit_reducible]

instance SauerlandStateva2011.instDecidableEqItemClass : DecidableEq ItemClass

Equations

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

@[implicit_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

@[implicit_reducible]

instance SauerlandStateva2011.instDecidableEqApproximator : DecidableEq Approximator

Equations

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

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

Equations

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

@[implicit_reducible]

instance SauerlandStateva2011.instReprApproximator : Repr Approximator

Equations

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

def SauerlandStateva2011.Approximator.selects : Approximator → ItemClass

The item class each approximator selects: plain scalar approximators take non-endpoints, the specialized endpoint approximators take endpoints (their §6.4, (32): absolutely/completely/more or less make endpoints more or less precise and block exactly/approximately there).

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's compatibility prediction: an approximator combines with an item iff the item is of the class it selects.

Equations

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

@[implicit_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

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

Equations

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

@[implicit_reducible]

instance SauerlandStateva2011.instReprJudgment : Repr Judgment

Equations

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

def SauerlandStateva2011.Judgment.rows : List Judgment

Their cited judgments: (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; (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 dualism argument: the two-type classification reproduces every cited judgment — approximator acceptability is class match.

Granularity setting (their (18)–(19))

Scalar approximators reset the context's granularity parameter: exactly to the finest available level, approximately to the coarsest. The reset targets bound every available interpretation — at the finest width the denotation interval (their (12)–(13), mkGranInterval) is contained in all others.

theorem SauerlandStateva2011.exactly_narrowest (𝒢 : Finset ℚ) (h𝒢 : 𝒢.Nonempty) {ε : ℚ} (hε : ε ∈ 𝒢) (d : ℚ) : (Degree.Granularity.mkGranInterval ε d).lo ≤ (Degree.Granularity.mkGranInterval (Degree.Granularity.finestWidth 𝒢 h𝒢) d).lo ∧ (Degree.Granularity.mkGranInterval (Degree.Granularity.finestWidth 𝒢 h𝒢) d).hi ≤ (Degree.Granularity.mkGranInterval ε d).hi

Their (19a): exactly yields the narrowest available interpretation — its denotation interval sits inside every available one.

theorem SauerlandStateva2011.approximately_widest (𝒢 : Finset ℚ) (h𝒢 : 𝒢.Nonempty) {ε : ℚ} (hε : ε ∈ 𝒢) (d : ℚ) : (Degree.Granularity.mkGranInterval (Degree.Granularity.coarsestWidth 𝒢 h𝒢) d).lo ≤ (Degree.Granularity.mkGranInterval ε d).lo ∧ (Degree.Granularity.mkGranInterval ε d).hi ≤ (Degree.Granularity.mkGranInterval (Degree.Granularity.coarsestWidth 𝒢 h𝒢) d).hi

Their (19b): approximately yields the widest available interpretation.

theorem SauerlandStateva2011.second_reset_vacuous (ε : ℚ) : Degree.Granularity.finestWidth {ε} ⋯ = ε ∧ Degree.Granularity.coarsestWidth {ε} ⋯ = ε

Their §6.3.5: a second scalar approximator is vacuous — the first reset leaves a singleton granularity set, on which resetting (in either direction) returns the same width. Hence #exactly approximately 30.

Fragment bridge

The English.NumeralModifiers entries carry the setter classification: exactifiers signal a point distribution and set the finest grain; tolerance modifiers signal a peaked distribution and set a coarser one.

theorem SauerlandStateva2011.fragment_setter_directions : English.NumeralModifiers.exactly.modType = English.NumeralModifiers.ModifierType.exactifier ∧ English.NumeralModifiers.exactly.pragFunction = English.NumeralModifiers.PragmaticFunction.pointSignal ∧ English.NumeralModifiers.precisely.modType = English.NumeralModifiers.ModifierType.exactifier ∧ English.NumeralModifiers.precisely.pragFunction = English.NumeralModifiers.PragmaticFunction.pointSignal ∧ English.NumeralModifiers.approximately.modType = English.NumeralModifiers.ModifierType.tolerance ∧ English.NumeralModifiers.approximately.pragFunction = English.NumeralModifiers.PragmaticFunction.peakedSignal ∧ English.NumeralModifiers.about.modType = English.NumeralModifiers.ModifierType.tolerance ∧ English.NumeralModifiers.about.pragFunction = English.NumeralModifiers.PragmaticFunction.peakedSignal

The fragment's exactly/precisely are finest-setters (pointSignal exactifiers) and its about/around/approximately/roughly are coarse-setters (peakedSignal tolerance modifiers).