Documentation

Linglib.Phenomena.Gradability.Compare

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/.

source
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}

Instances For
    source
    @[implicit_reducible]
    instance Phenomena.Gradability.Compare.instReprVaguenessTheoryType :
    Repr VaguenessTheoryType
    Equations
    source
    def Phenomena.Gradability.Compare.instReprVaguenessTheoryType.repr :
    VaguenessTheoryType → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Phenomena.Gradability.Compare.instDecidableEqVaguenessTheoryType :
      DecidableEq VaguenessTheoryType
      Equations
      source
      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
      Instances For
        source
        def Phenomena.Gradability.Compare.instReprTheoryPredictionProfile.repr :
        TheoryPredictionProfile → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance Phenomena.Gradability.Compare.instReprTheoryPredictionProfile :
          Repr TheoryPredictionProfile
          Equations
          source
          def Phenomena.Gradability.Compare.epistemicismProfile :
          TheoryPredictionProfile
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Phenomena.Gradability.Compare.supervaluationismProfile :
            TheoryPredictionProfile
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Phenomena.Gradability.Compare.degreeTheoryProfile :
              TheoryPredictionProfile
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Phenomena.Gradability.Compare.contextualismProfile :
                TheoryPredictionProfile
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  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.
                  Instances For
                    source
                    def Phenomena.Gradability.Compare.theoryProfiles :
                    List TheoryPredictionProfile
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      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.
                      source
                      theorem Phenomena.Gradability.Compare.supervaluationism_classical_verified {Spec : Type u_1} [DecidableEq Spec] (eval : Spec → Prop) [DecidablePred eval] :
                      (∀ (S : Semantics.Supervaluation.SpecSpace Spec), Semantics.Supervaluation.superTrue eval S = Core.Duality.Truth3.true) ↔ ∀ (s : Spec), eval s

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

                      source
                      theorem Phenomena.Gradability.Compare.supervaluationism_gaps_verified {Spec : Type u_1} (eval : Spec → Prop) [DecidablePred eval] (S : Semantics.Supervaluation.SpecSpace Spec) :
                      Semantics.Supervaluation.superTrue eval S = Core.Duality.Truth3.indet ↔ (∃ s ∈ S.admissible, eval s) ∧ ∃ s ∈ S.admissible, ¬eval s

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

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

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

                      source
                      theorem Phenomena.Gradability.Compare.supervaluationism_D_verified {Spec : Type u_1} (eval : Spec → Prop) [DecidablePred eval] (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 (substrate) + Phenomena/Gradability/Studies/CobrerosEtAl2012.lean (worked 4-element example):

                      - `allowsTruthValueGaps = true`: borderline cases exist and
  tolerantly satisfy contradictions (`b_is_borderline`,
  `b_tolerant_contradiction`)
- `soritesResolution`: st-consequence blocks sorites chaining
  (`st_three_step_invalid` — actual non-transitivity using
  similarity atoms, paper §3.4.1 + footnote 14)
- `preservesClassicalLogic = false`: borderline contradictions
  diverge from supervaluation
  (`tcs_supervaluation_disagree_concrete`)

These verification theorems re-export the key results.
                      source
                      theorem Phenomena.Gradability.Compare.tcs_borderline_contradiction_verified :
                      Semantics.Supervaluation.TCS.IsBorderline Studies.CobrerosEtAl2012.soritesModel Studies.CobrerosEtAl2012.VPred.tall Studies.CobrerosEtAl2012.Elt.b ∧ Semantics.Supervaluation.TCS.IsBorderline Studies.CobrerosEtAl2012.soritesModel Studies.CobrerosEtAl2012.VPred.tall Studies.CobrerosEtAl2012.Elt.c

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

                      source
                      theorem Phenomena.Gradability.Compare.tcs_sorites_resolution_verified :
                      ¬Semantics.Supervaluation.TCS.tcsConsequence Semantics.Supervaluation.TCS.SatMode.strict Semantics.Supervaluation.TCS.SatMode.tolerant [Core.Logic.ThreeValuedLogic.PropFormula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred Studies.CobrerosEtAl2012.VPred.tall Studies.CobrerosEtAl2012.Elt.a)] (Core.Logic.ThreeValuedLogic.PropFormula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred Studies.CobrerosEtAl2012.VPred.tall Studies.CobrerosEtAl2012.Elt.d))

                      TCS resolves the sorites: the single-premise chain Pa ⊨ˢᵗ Pd is invalid. The Studies file's st_three_step_invalid provides the stronger statement (non-transitivity proper, with similarity atoms in the chain).

                      source
                      theorem Phenomena.Gradability.Compare.tcs_hierarchy_verified (M : Semantics.Supervaluation.TCS.TModel Studies.CobrerosEtAl2012.Elt Studies.CobrerosEtAl2012.VPred) (φ : Semantics.Supervaluation.TCS.TCSFormula Studies.CobrerosEtAl2012.VPred Studies.CobrerosEtAl2012.Elt) :
                      (Semantics.Supervaluation.TCS.Sat M Semantics.Supervaluation.TCS.SatMode.strict φ → Semantics.Supervaluation.TCS.Sat M Semantics.Supervaluation.TCS.SatMode.classical φ) ∧ (Semantics.Supervaluation.TCS.Sat M Semantics.Supervaluation.TCS.SatMode.classical φ → Semantics.Supervaluation.TCS.Sat M Semantics.Supervaluation.TCS.SatMode.tolerant φ)

                      TCS validates tolerance: the extension hierarchy s ⊆ c ⊆ t at the formula level (Lemma 1 of @cite{cobreros-etal-2012}, p. 357).