structure Phenomena.Gradability.Vagueness.BorderlineDatum : Type

Empirical pattern: Borderline cases elicit hedging and uncertainty.

For individuals near the inferred threshold:

• Speakers hedge or refuse to answer
• Judgments show high variance across informants
• Neither "A" nor "not A" feels fully appropriate

Source: @cite{lassiter-goodman-2017} Section 1, @cite{kennedy-2007}

• adjective : String

  The adjective

• context : String

  Description of the context/comparison class

• clearPositive : String

  Clear positive case (definitely A)

• clearPositiveValue : String

  Clear positive value

• clearNegative : String

  Clear negative case (definitely not A)

• clearNegativeValue : String

  Clear negative value

• borderline : String

  Borderline case

• borderlineValue : String

  Borderline value

instance Phenomena.Gradability.Vagueness.instReprBorderlineDatum : Repr BorderlineDatum

Equations

• Phenomena.Gradability.Vagueness.instReprBorderlineDatum = { reprPrec := Phenomena.Gradability.Vagueness.instReprBorderlineDatum.repr }

def Phenomena.Gradability.Vagueness.instReprBorderlineDatum.repr : BorderlineDatum → Nat → Std.Format

Equations

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

def Phenomena.Gradability.Vagueness.expensiveHouse : BorderlineDatum

House price borderline example.

Equations

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

def Phenomena.Gradability.Vagueness.tallPerson : BorderlineDatum

Height borderline example.

Equations

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

def Phenomena.Gradability.Vagueness.borderlineExamples : List BorderlineDatum

Equations

• Phenomena.Gradability.Vagueness.borderlineExamples = [Phenomena.Gradability.Vagueness.expensiveHouse, Phenomena.Gradability.Vagueness.tallPerson]

structure Phenomena.Gradability.Vagueness.SoritesDatum : Type

Empirical pattern: The sorites paradox.

Given:

1. A clearly Adj individual (premise 1)
2. A tolerance principle: "If x is Adj and y is ε smaller, then y is Adj" (premise 2)
3. Iterated application leads to a clearly non-Adj individual (conclusion)

Empirical observations:

• People accept premise 1 (the clear case)
• People accept individual instances of premise 2 (each step seems valid)
• People reject the conclusion (the absurd case)
• People show gradient acceptance as cases approach the threshold

Source: @cite{edgington-1997}, @cite{lassiter-goodman-2017} Section 5

• adjective : String
• scale : String
• toleranceGap : String
• clearPositive : String
• positiveValue : String
• clearNegative : String
• negativeValue : String
• numSteps : Nat
• acceptPremise1 : Bool
• acceptToleranceSteps : Bool
• acceptConclusion : Bool

def Phenomena.Gradability.Vagueness.instReprSoritesDatum.repr : SoritesDatum → Nat → Std.Format

Equations

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

instance Phenomena.Gradability.Vagueness.instReprSoritesDatum : Repr SoritesDatum

Equations

• Phenomena.Gradability.Vagueness.instReprSoritesDatum = { reprPrec := Phenomena.Gradability.Vagueness.instReprSoritesDatum.repr }

def Phenomena.Gradability.Vagueness.tallSorites : SoritesDatum

Equations

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

def Phenomena.Gradability.Vagueness.heapSorites : SoritesDatum

Equations

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

def Phenomena.Gradability.Vagueness.expensiveSorites : SoritesDatum

Equations

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

def Phenomena.Gradability.Vagueness.soritesExamples : List SoritesDatum

Equations

• Phenomena.Gradability.Vagueness.soritesExamples = [Phenomena.Gradability.Vagueness.tallSorites, Phenomena.Gradability.Vagueness.heapSorites, Phenomena.Gradability.Vagueness.expensiveSorites]

structure Phenomena.Gradability.Vagueness.HigherOrderVaguenessData : Type

The problem of higher-order vagueness.

If "tall" has borderline cases, what about "borderline tall"? Is there a sharp boundary between "borderline tall" and "clearly tall"?

• First-order vagueness: borderline cases of "tall"
• Second-order vagueness: borderline cases of "borderline tall"
• Third-order vagueness: borderline cases of "borderline borderline tall" -... and so on

This threatens any theory that posits sharp boundaries anywhere.

Source: @cite{fine-1975}, @cite{williamson-1994},

• basePredicate : String
• clearlyPositive : String
• borderline : String
• clearlyNegative : String
• sharpClearlyBorderline : Bool
• sharpBorderlineNot : Bool
• iteratesUpward : Bool

def Phenomena.Gradability.Vagueness.instReprHigherOrderVaguenessData.repr : HigherOrderVaguenessData → Nat → Std.Format

Equations

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

instance Phenomena.Gradability.Vagueness.instReprHigherOrderVaguenessData : Repr HigherOrderVaguenessData

Equations

• Phenomena.Gradability.Vagueness.instReprHigherOrderVaguenessData = { reprPrec := Phenomena.Gradability.Vagueness.instReprHigherOrderVaguenessData.repr }

def Phenomena.Gradability.Vagueness.tallHigherOrder : HigherOrderVaguenessData

Equations

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

def Phenomena.Gradability.Vagueness.higherOrderExamples : List HigherOrderVaguenessData

Equations

• Phenomena.Gradability.Vagueness.higherOrderExamples = [Phenomena.Gradability.Vagueness.tallHigherOrder]

structure Phenomena.Gradability.Vagueness.DefinitelyOperatorData : Type

The "definitely" operator and higher-order vagueness.

If "Definitely tall" means "clearly tall" (not borderline), then:

• "Definitely tall" should have sharper boundaries than "tall"
• But "definitely" is itself vague.
• So we get: "borderline definitely tall"

Iterating: "definitely definitely tall", etc.

Source: @cite{fine-1975}, @cite{williamson-1994}

• predicate : String
• eliminatesBorderline : Bool
• definitelyIsVague : Bool
• borderlineDefinitely : Bool
• iterationHelps : Bool

instance Phenomena.Gradability.Vagueness.instReprDefinitelyOperatorData : Repr DefinitelyOperatorData

Equations

• Phenomena.Gradability.Vagueness.instReprDefinitelyOperatorData = { reprPrec := Phenomena.Gradability.Vagueness.instReprDefinitelyOperatorData.repr }

def Phenomena.Gradability.Vagueness.instReprDefinitelyOperatorData.repr : DefinitelyOperatorData → Nat → Std.Format

Equations

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

def Phenomena.Gradability.Vagueness.definitelyOperator : DefinitelyOperatorData

Equations

• Phenomena.Gradability.Vagueness.definitelyOperator = { predicate := "tall", eliminatesBorderline := true, definitelyIsVague := true, borderlineDefinitely := true, iterationHelps := false }

structure Phenomena.Gradability.Vagueness.PenumbralConnectionData : Type

Penumbral connections: logical relationships that hold even in borderline cases.

Even if we don't know whether John is tall:

• "John is tall ∨ John is not tall" is true (excluded middle)
• "John is tall ∧ John is not tall" is false (non-contradiction)
• If John = 5'9" and Mary = 5'9", then "John is tall ↔ Mary is tall" (same-height)

These are "penumbral truths" - true in the borderline region.

Supervaluationism: true iff true on ALL precisifications. Degree theories: must explain why these have degree 1.

Source: @cite{fine-1975}, @cite{keefe-2000}

• connectionName : String
• formalStatement : String
• alwaysTrue : Bool
• borderlineExample : String
• supervaluationismCaptures : Bool
• degreeTheoryCaptures : Bool

instance Phenomena.Gradability.Vagueness.instReprPenumbralConnectionData : Repr PenumbralConnectionData

Equations

• Phenomena.Gradability.Vagueness.instReprPenumbralConnectionData = { reprPrec := Phenomena.Gradability.Vagueness.instReprPenumbralConnectionData.repr }

def Phenomena.Gradability.Vagueness.instReprPenumbralConnectionData.repr : PenumbralConnectionData → Nat → Std.Format

Equations

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

def Phenomena.Gradability.Vagueness.excludedMiddle : PenumbralConnectionData

Equations

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

def Phenomena.Gradability.Vagueness.nonContradiction : PenumbralConnectionData

Equations

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

def Phenomena.Gradability.Vagueness.sameHeightConnection : PenumbralConnectionData

Equations

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

def Phenomena.Gradability.Vagueness.comparativeEntailment : PenumbralConnectionData

Equations

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

def Phenomena.Gradability.Vagueness.penumbralExamples : List PenumbralConnectionData

Equations

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

structure Phenomena.Gradability.Vagueness.TolerancePrincipleData : Type

The tolerance principle: the central ingredient in sorites paradoxes.

Tolerance: If x is F and y differs from x by only a tiny amount, then y is also F.

This seems true for vague predicates:

• 1mm can't make the difference between tall and not-tall
• $1 can't make the difference between expensive and not-expensive
• 1 grain can't make the difference between heap and not-heap

But iterated application leads to absurdity (the sorites).

Source: @cite{wright-1976}, @cite{fara-2000}

• predicate : String
• scale : String
• toleranceMargin : String
• individualStepAcceptable : Bool
• iterationAbsurd : Bool
• proposedResolution : String

instance Phenomena.Gradability.Vagueness.instReprTolerancePrincipleData : Repr TolerancePrincipleData

Equations

• Phenomena.Gradability.Vagueness.instReprTolerancePrincipleData = { reprPrec := Phenomena.Gradability.Vagueness.instReprTolerancePrincipleData.repr }

def Phenomena.Gradability.Vagueness.instReprTolerancePrincipleData.repr : TolerancePrincipleData → Nat → Std.Format

Equations

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

def Phenomena.Gradability.Vagueness.heightTolerance : TolerancePrincipleData

Equations

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

def Phenomena.Gradability.Vagueness.priceTolerance : TolerancePrincipleData

Equations

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

def Phenomena.Gradability.Vagueness.toleranceExamples : List TolerancePrincipleData

Equations

• Phenomena.Gradability.Vagueness.toleranceExamples = [Phenomena.Gradability.Vagueness.heightTolerance, Phenomena.Gradability.Vagueness.priceTolerance]

structure Phenomena.Gradability.Vagueness.ProbabilisticSoritesData : Type

Probabilistic sorites analysis.

Each tolerance step is highly probable, not certain.

Let P(step) = 0.99 (each step is 99% acceptable) After N steps: P(all steps) = 0.99^N

For N = 762 (mm from 7'4" to 4'10"): 0.99^762 ≈ 0.0005 (extremely unlikely)

The paradox dissolves: the argument is valid but unsound. Each premise is probably true, but the conjunction is probably false.

Source: @cite{edgington-1997}, @cite{lassiter-goodman-2017} Section 5

• predicate : String
• singleStepProbability : Float
• numSteps : Nat
• cumulativeProbability : Float
• premise1Accepted : Bool
• eachStepAccepted : Bool
• fullArgumentAccepted : Bool

instance Phenomena.Gradability.Vagueness.instReprProbabilisticSoritesData : Repr ProbabilisticSoritesData

Equations

• Phenomena.Gradability.Vagueness.instReprProbabilisticSoritesData = { reprPrec := Phenomena.Gradability.Vagueness.instReprProbabilisticSoritesData.repr }

def Phenomena.Gradability.Vagueness.instReprProbabilisticSoritesData.repr : ProbabilisticSoritesData → Nat → Std.Format

Equations

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

def Phenomena.Gradability.Vagueness.tallProbabilisticSorites : ProbabilisticSoritesData

Equations

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

def Phenomena.Gradability.Vagueness.probabilisticSoritesExamples : List ProbabilisticSoritesData

Equations

• Phenomena.Gradability.Vagueness.probabilisticSoritesExamples = [Phenomena.Gradability.Vagueness.tallProbabilisticSorites]

structure Phenomena.Gradability.Vagueness.VaguenessDesideratum : Type

Formal constraints that any adequate theory of vagueness should satisfy.

These are theory-neutral desiderata. A theory's success is measured by how well it accounts for these patterns.

Source: Various

• name : String
• description : String
• formalStatement : String
• importance : String

instance Phenomena.Gradability.Vagueness.instReprVaguenessDesideratum : Repr VaguenessDesideratum

Equations

• Phenomena.Gradability.Vagueness.instReprVaguenessDesideratum = { reprPrec := Phenomena.Gradability.Vagueness.instReprVaguenessDesideratum.repr }

def Phenomena.Gradability.Vagueness.instReprVaguenessDesideratum.repr : VaguenessDesideratum → Nat → Std.Format

Equations

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

def Phenomena.Gradability.Vagueness.borderlineCasesExist : VaguenessDesideratum

Equations

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

def Phenomena.Gradability.Vagueness.toleranceIntuition : VaguenessDesideratum

Equations

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

def Phenomena.Gradability.Vagueness.soritesParadoxicality : VaguenessDesideratum

Equations

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

def Phenomena.Gradability.Vagueness.penumbralPreservation : VaguenessDesideratum

Equations

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

def Phenomena.Gradability.Vagueness.higherOrderProblem : VaguenessDesideratum

Equations

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

def Phenomena.Gradability.Vagueness.desiderata : List VaguenessDesideratum

Equations

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

structure Phenomena.Gradability.Vagueness.InterestRelativityDatum : Type

Interest-relativity of vague extension.

The extension of a vague gradable adjective can change when an agent's interests change, even if the precise measured property stays constant. This is evidence that the degrees of vague quantities incorporate information about interests, not just objective measurements.

Source: @cite{fara-2000}, @cite{dinis-jacinto-2026} §5.3

• adjective : String
• individual : String
• preciseProperty : String
• preciseValueUnchanged : Bool
• interestsChanged : String
• extensionBefore : Bool
• extensionAfter : Bool
• extensionFlipped : Bool

instance Phenomena.Gradability.Vagueness.instReprInterestRelativityDatum : Repr InterestRelativityDatum

Equations

• Phenomena.Gradability.Vagueness.instReprInterestRelativityDatum = { reprPrec := Phenomena.Gradability.Vagueness.instReprInterestRelativityDatum.repr }

def Phenomena.Gradability.Vagueness.instReprInterestRelativityDatum.repr : InterestRelativityDatum → Nat → Std.Format

Equations

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

def Phenomena.Gradability.Vagueness.charlesIIIBaldness : InterestRelativityDatum

Prince William / Charles III: as William ages, his interests shift toward considering people with m hairs bald whom he previously didn't. Charles III has the same number of hairs, but was bald∅ before and isn't now — his baldness degree changed because degrees partially reflect interests.

Equations

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

def Phenomena.Gradability.Vagueness.houseExpensiveness : InterestRelativityDatum

Context-dependent expensiveness: same price, different interests.

Equations

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

def Phenomena.Gradability.Vagueness.interestRelativityExamples : List InterestRelativityDatum

Equations

• Phenomena.Gradability.Vagueness.interestRelativityExamples = [Phenomena.Gradability.Vagueness.charlesIIIBaldness, Phenomena.Gradability.Vagueness.houseExpensiveness]

structure Phenomena.Gradability.Vagueness.ToleranceStepDatum : Type

Tolerance step non-uniformity.

Not all tolerance steps feel equally acceptable. In a Soritical sequence where adjacent elements differ by one precise unit (one hair, one mm, one dollar), some steps feel like negligible differences and others feel like significant jumps — even though the precise difference is identical.

This is evidence that the vague difference between adjacent elements is not a simple function of the precise difference.

Source: @cite{fara-2000} on salient similarity, @cite{dinis-jacinto-2026} §6.1

• adjective : String
• preciseDifference : String
• clearRegionAcceptance : String

  Steps near clear cases feel negligible

• thresholdRegionAcceptance : String

  Steps near the threshold feel significant

• nonUniform : Bool

  Same precise difference, different perceived significance

def Phenomena.Gradability.Vagueness.instReprToleranceStepDatum.repr : ToleranceStepDatum → Nat → Std.Format

Equations

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

instance Phenomena.Gradability.Vagueness.instReprToleranceStepDatum : Repr ToleranceStepDatum

Equations

• Phenomena.Gradability.Vagueness.instReprToleranceStepDatum = { reprPrec := Phenomena.Gradability.Vagueness.instReprToleranceStepDatum.repr }

def Phenomena.Gradability.Vagueness.baldnessToleranceSteps : ToleranceStepDatum

Baldness tolerance: removing one hair from someone with 100,000 hairs feels negligible; removing one hair from someone near the "boundary" can feel significant.

Equations

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

def Phenomena.Gradability.Vagueness.heightToleranceSteps : ToleranceStepDatum

Height tolerance: 1mm difference between two clearly tall people feels negligible; 1mm difference near the threshold feels more significant.

Equations

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

def Phenomena.Gradability.Vagueness.toleranceStepExamples : List ToleranceStepDatum

Equations

• Phenomena.Gradability.Vagueness.toleranceStepExamples = [Phenomena.Gradability.Vagueness.baldnessToleranceSteps, Phenomena.Gradability.Vagueness.heightToleranceSteps]

structure Phenomena.Gradability.Vagueness.BorderlineContradictionDatum : Type

Borderline contradiction acceptance.

Experimental data on whether subjects accept sentences of the form "X is P and not P" (contradictions) and "X is neither P nor not P" (gaps) for borderline cases of vague predicates.

Key finding: acceptance rates for both contradictions and gaps are significantly higher for borderline cases than for clear cases. This is evidence against both classical logic (which rejects all contradictions) and standard supervaluationism (which makes contradictions super-false even for borderline cases).

The data is compatible with the TCS framework (@cite{cobreros-etal-2012}), which predicts that borderline cases tolerantly satisfy P ∧ ¬P.

Source: @cite{alxatib-pelletier-2011}, @cite{ripley-2011}, @cite{serchuk-hargreaves-zach-2011}

• study : String

  Study identifier

• predicate : String

  The vague predicate tested

• stimulusType : String

  Stimulus type (visual, scenario-based, etc.)

• borderlineCase : String

  Description of the borderline case

• contradictionAcceptance : Option Float

  Acceptance rate for "X is P and not P" (contradiction)

• gapAcceptance : Option Float

  Acceptance rate for "X is neither P nor not P" (gap)

• borderlinePeaks : Bool

  Whether rates are significantly higher for borderline than clear cases

instance Phenomena.Gradability.Vagueness.instReprBorderlineContradictionDatum : Repr BorderlineContradictionDatum

Equations

• Phenomena.Gradability.Vagueness.instReprBorderlineContradictionDatum = { reprPrec := Phenomena.Gradability.Vagueness.instReprBorderlineContradictionDatum.repr }

def Phenomena.Gradability.Vagueness.instReprBorderlineContradictionDatum.repr : BorderlineContradictionDatum → Nat → Std.Format

Equations

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

def Phenomena.Gradability.Vagueness.alxatibPelletier2011Tall : BorderlineContradictionDatum

@cite{alxatib-pelletier-2011}: 5 men of different heights (visual). Man #2 (5'11", median size) shows peak contradiction/gap acceptance.

Equations

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

def Phenomena.Gradability.Vagueness.ripley2011Near : BorderlineContradictionDatum

@cite{ripley-2011}: 7 pairs (A-G) of decreasing nearness (visual). Pair C (median distance) shows peak contradiction acceptance.

Equations

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

def Phenomena.Gradability.Vagueness.serchukEtAl2011Rich : BorderlineContradictionDatum

@cite{serchuk-hargreaves-zach-2011}: scenario-based (Susan's wealth). Forced-choice with 6 options including "Both", "Neither", "Partially True".

Equations

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

def Phenomena.Gradability.Vagueness.borderlineContradictionData : List BorderlineContradictionDatum

Equations

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

theorem Phenomena.Gradability.Vagueness.all_borderline_peak : (borderlineContradictionData.all fun (d : BorderlineContradictionDatum) => d.borderlinePeaks) = true

All three studies find borderline-peaking: contradiction/gap acceptance is significantly higher for borderline cases than for clear cases. This is the key empirical finding that TCS accounts for and standard supervaluationism does not.