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 Phenomena.Gradability.Compare.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
• tcs : VaguenessTheoryType

def Phenomena.Gradability.Compare.instReprVaguenessTheoryType.repr : VaguenessTheoryType → ℕ → Std.Format

Equations

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

instance Phenomena.Gradability.Compare.instReprVaguenessTheoryType : Repr VaguenessTheoryType

Equations

• Phenomena.Gradability.Compare.instReprVaguenessTheoryType = { reprPrec := Phenomena.Gradability.Compare.instReprVaguenessTheoryType.repr }

instance Phenomena.Gradability.Compare.instDecidableEqVaguenessTheoryType : DecidableEq VaguenessTheoryType

Equations

• Phenomena.Gradability.Compare.instDecidableEqVaguenessTheoryType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Gradability.Compare.instBEqVaguenessTheoryType.beq : VaguenessTheoryType → VaguenessTheoryType → Bool

Equations

• Phenomena.Gradability.Compare.instBEqVaguenessTheoryType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Gradability.Compare.instBEqVaguenessTheoryType : BEq VaguenessTheoryType

Equations

• Phenomena.Gradability.Compare.instBEqVaguenessTheoryType = { beq := Phenomena.Gradability.Compare.instBEqVaguenessTheoryType.beq }

structure Phenomena.Gradability.Compare.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 Phenomena.Gradability.Compare.instReprTheoryPredictionProfile.repr : TheoryPredictionProfile → ℕ → Std.Format

Equations

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

instance Phenomena.Gradability.Compare.instReprTheoryPredictionProfile : Repr TheoryPredictionProfile

Equations

• Phenomena.Gradability.Compare.instReprTheoryPredictionProfile = { reprPrec := Phenomena.Gradability.Compare.instReprTheoryPredictionProfile.repr }

def Phenomena.Gradability.Compare.epistemicismProfile : TheoryPredictionProfile

Equations

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

def Phenomena.Gradability.Compare.supervaluationismProfile : TheoryPredictionProfile

Equations

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

def Phenomena.Gradability.Compare.degreeTheoryProfile : TheoryPredictionProfile

Equations

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

def Phenomena.Gradability.Compare.contextualismProfile : TheoryPredictionProfile

Equations

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

def Phenomena.Gradability.Compare.tcsProfile : TheoryPredictionProfile

TCS (@cite{cobreros-etal-2012}): similarity-based semantics with three notions of truth (tolerant, classical, strict) and non-transitive st-consequence. Distinct from supervaluationism: allows borderline contradictions (Pa ∧ ¬Pa tolerantly true).

Equations

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

def Phenomena.Gradability.Compare.theoryProfiles : List TheoryPredictionProfile

Equations

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

The supervaluationism profile's claims are backed by formal proofs in Theories/Semantics/Supervaluation/Basic.lean:

- `preservesClassicalLogic = true`: super-validity ↔ classical validity
- `allowsTruthValueGaps = true`: indefiniteness ↔ witnesses on both sides
- `soritesResolution`: tolerance premise fails at every threshold boundary

These verification theorems re-export the key results, making the
connection between the comparison profile and the proved framework
explicit and machine-checkable. 

theorem Phenomena.Gradability.Compare.supervaluationism_classical_verified {Spec : Type u_1} [DecidableEq Spec] (eval : Spec → Bool) : (∀ (S : Semantics.Supervaluation.SpecSpace Spec), Semantics.Supervaluation.superTrue eval S = Core.Duality.Truth3.true) ↔ ∀ (s : Spec), eval s = true

Classical logic preservation: super-validity ↔ classical validity. The supervaluationism profile claims preservesClassicalLogic = true; this theorem proves the claim.

theorem Phenomena.Gradability.Compare.supervaluationism_gaps_verified {Spec : Type u_1} (eval : Spec → Bool) (S : Semantics.Supervaluation.SpecSpace Spec) : Semantics.Supervaluation.superTrue eval S = Core.Duality.Truth3.indet ↔ (∃ s ∈ S.admissible, eval s = true) ∧ ∃ s ∈ S.admissible, eval s = false

Truth-value gaps: indefiniteness ↔ witnesses exist on both sides. The supervaluationism profile claims allowsTruthValueGaps = true; this theorem proves gap existence is well-defined.

theorem Phenomena.Gradability.Compare.supervaluationism_consequence_verified {Spec : Type u_1} [DecidableEq Spec] (evalA evalB : Spec → Bool) : Semantics.Supervaluation.superConsequence evalA evalB ↔ ∀ (s : Spec), evalA s = true → evalB s = true

Consequence preservation: super-consequence ↔ classical consequence. Supervaluationism makes a difference to truth but not to logic.

theorem Phenomena.Gradability.Compare.supervaluationism_D_verified {Spec : Type u_1} (eval : Spec → Bool) (S : Semantics.Supervaluation.SpecSpace Spec) : Semantics.Supervaluation.superTrue (fun (s : Spec) => !Semantics.Supervaluation.definitely eval S || eval s) S = Core.Duality.Truth3.true

The D operator eliminates borderline cases: DA → A is super-valid (T axiom), but A → DA is not.

The TCS profile's claims are backed by formal proofs in Theories/Semantics/Supervaluation/TCS.lean:

- `allowsTruthValueGaps = true`: borderline cases exist and
  tolerantly satisfy contradictions
- `soritesResolution`: st-consequence blocks sorites chaining
  (non-transitivity demonstrated on concrete model)
- `preservesClassicalLogic = false`: st-consequence is non-transitive

These verification theorems re-export the key results. 

theorem Phenomena.Gradability.Compare.tcs_borderline_contradiction_verified : Semantics.Supervaluation.TCS.isBorderline Semantics.Supervaluation.TCS.soritesModel Semantics.Supervaluation.TCS.VPred.tall Semantics.Supervaluation.TCS.Elt.b = true ∧ Semantics.Supervaluation.TCS.isBorderline Semantics.Supervaluation.TCS.soritesModel Semantics.Supervaluation.TCS.VPred.tall Semantics.Supervaluation.TCS.Elt.c = true

TCS allows borderline contradictions: in the 4-element sorites model, borderline individuals tolerantly satisfy P ∧ ¬P.

theorem Phenomena.Gradability.Compare.tcs_sorites_resolution_verified : ¬Semantics.Supervaluation.TCS.tcsConsequence Semantics.Supervaluation.TCS.SatMode.strict Semantics.Supervaluation.TCS.SatMode.tolerant [Semantics.Supervaluation.TCS.TCSFormula.atom Semantics.Supervaluation.TCS.VPred.tall Semantics.Supervaluation.TCS.Elt.a] (Semantics.Supervaluation.TCS.TCSFormula.atom Semantics.Supervaluation.TCS.VPred.tall Semantics.Supervaluation.TCS.Elt.d)

TCS resolves the sorites: the full chain is st-invalid.

theorem Phenomena.Gradability.Compare.tcs_hierarchy_verified (M : Semantics.Supervaluation.TCS.TModel Semantics.Supervaluation.TCS.Elt Semantics.Supervaluation.TCS.VPred) (φ : Semantics.Supervaluation.TCS.TCSFormula Semantics.Supervaluation.TCS.VPred Semantics.Supervaluation.TCS.Elt) : (Semantics.Supervaluation.TCS.sat M Semantics.Supervaluation.TCS.SatMode.strict φ = true → Semantics.Supervaluation.TCS.sat M Semantics.Supervaluation.TCS.SatMode.classical φ = true) ∧ (Semantics.Supervaluation.TCS.sat M Semantics.Supervaluation.TCS.SatMode.classical φ = true → Semantics.Supervaluation.TCS.sat M Semantics.Supervaluation.TCS.SatMode.tolerant φ = true)

TCS validates tolerance: the extension hierarchy s ⊆ c ⊆ t.