Vagueness Theory Comparison

@cite{keefe-2000} @cite{williamson-1994}

Theory-comparative infrastructure for vagueness: characterizes what each major theoretical position (epistemicism, supervaluationism, degree theory, contextualism) predicts about borderline cases, sorites, higher-order vagueness, and classical logic.

This is cross-theory comparison, not empirical data — hence lives in Comparisons/ rather than Phenomena/.

inductive Comparisons.VaguenessTheories.VaguenessTheoryType : Type

Major theoretical positions on vagueness.

This is a theory-neutral characterization of what each position claims.

Source: @cite{keefe-2000}, @cite{williamson-1994}

• epistemicism : VaguenessTheoryType
• supervaluationism : VaguenessTheoryType
• degreeTheory : VaguenessTheoryType
• contextualism : VaguenessTheoryType
• nihilism : VaguenessTheoryType

def Comparisons.VaguenessTheories.instReprVaguenessTheoryType.repr : VaguenessTheoryType → Nat → Std.Format

Equations

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

instance Comparisons.VaguenessTheories.instReprVaguenessTheoryType : Repr VaguenessTheoryType

Equations

• Comparisons.VaguenessTheories.instReprVaguenessTheoryType = { reprPrec := Comparisons.VaguenessTheories.instReprVaguenessTheoryType.repr }

instance Comparisons.VaguenessTheories.instDecidableEqVaguenessTheoryType : DecidableEq VaguenessTheoryType

Equations

• Comparisons.VaguenessTheories.instDecidableEqVaguenessTheoryType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Comparisons.VaguenessTheories.instBEqVaguenessTheoryType.beq : VaguenessTheoryType → VaguenessTheoryType → Bool

Equations

• Comparisons.VaguenessTheories.instBEqVaguenessTheoryType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Comparisons.VaguenessTheories.instBEqVaguenessTheoryType : BEq VaguenessTheoryType

Equations

• Comparisons.VaguenessTheories.instBEqVaguenessTheoryType = { beq := Comparisons.VaguenessTheories.instBEqVaguenessTheoryType.beq }

structure Comparisons.VaguenessTheories.TheoryPredictionProfile : Type

Data characterizing what each theory says about key phenomena.

This allows us to track which theories predict which patterns.

Source: @cite{keefe-2000}

• theory : VaguenessTheoryType
• hasSharpBoundaries : Bool
• preservesClassicalLogic : Bool
• allowsTruthValueGaps : Bool
• allowsDegreesOfTruth : Bool
• soritesResolution : String
• higherOrderResponse : String

def Comparisons.VaguenessTheories.instReprTheoryPredictionProfile.repr : TheoryPredictionProfile → Nat → Std.Format

Equations

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

instance Comparisons.VaguenessTheories.instReprTheoryPredictionProfile : Repr TheoryPredictionProfile

Equations

• Comparisons.VaguenessTheories.instReprTheoryPredictionProfile = { reprPrec := Comparisons.VaguenessTheories.instReprTheoryPredictionProfile.repr }

def Comparisons.VaguenessTheories.epistemicismProfile : TheoryPredictionProfile

Equations

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

def Comparisons.VaguenessTheories.supervaluationismProfile : TheoryPredictionProfile

Equations

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

def Comparisons.VaguenessTheories.degreeTheoryProfile : TheoryPredictionProfile

Equations

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

def Comparisons.VaguenessTheories.contextualismProfile : TheoryPredictionProfile

Equations

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

def Comparisons.VaguenessTheories.theoryProfiles : List TheoryPredictionProfile

Equations

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