Fine (1975): Vagueness, Truth and Logic @cite{fine-1975}

@cite{kamp-1975}

Supervaluationism applied to gradable predicates: a vague sentence is true iff true on ALL admissible precisifications, false iff false on ALL, and indefinite otherwise.

Architecture

The general supervaluation framework (specification spaces, super-truth, D operator, classical validity biconditional) lives in Theories/Semantics/Supervaluation/Basic.lean. This study file specializes that framework to threshold-based precisifications for gradable adjectives, and proves results specific to degree semantics:

• § 1: Threshold specification spaces
• § 2: Comparative entailment (monotonicity of positive predicate)
• § 3: Sorites resolution
• § 4: External penumbral connections (pink/red — multi-predicate)
• § 5: Bridge — inGapRegion ↔ Truth3.indet
• § 6: Higher-order D operator
• § 7: Verification of Vagueness.lean data

Connection to Kamp (1975)

@cite{fine-1975} and @cite{kamp-1975} appeared in the same volume. Kamp's dilemma (truth-functional three-valued logic cannot distinguish P ∧ P from P ∧ ¬P) is resolved by supervaluation — see Supervaluation.Basic.conjunction_self and Supervaluation.Basic.nonContradiction_superFalse.

Connection to Klein (1980)

@cite{klein-1980}'s comparative — "∃ C where tall(a,C) ∧ ¬tall(b,C)" — is the existential dual of supervaluation. See Theories/Semantics/Comparison/Delineation.lean.

def Phenomena.Gradability.Studies.Fine1975.mkSpec {max : ℕ} (S : Finset (Core.Scale.Threshold max)) (hne : S.Nonempty) : Semantics.Supervaluation.SpecSpace (Core.Scale.Threshold max)

Construct a specification space from a non-empty set of thresholds.

Equations

• Phenomena.Gradability.Studies.Fine1975.mkSpec S hne = { admissible := S, nonempty := hne }

def Phenomena.Gradability.Studies.Fine1975.superTrueAt {max : ℕ} (meaning : Core.Scale.Degree max → Core.Scale.Threshold max → Bool) (d : Core.Scale.Degree max) (S : Semantics.Supervaluation.SpecSpace (Core.Scale.Threshold max)) : Core.Duality.Truth3

Supervaluation of a degree predicate: fix a degree, vary the threshold.

Equations

• Phenomena.Gradability.Studies.Fine1975.superTrueAt meaning d S = Semantics.Supervaluation.superTrue (meaning d) S

theorem Phenomena.Gradability.Studies.Fine1975.comparative_entailment {max : ℕ} (d₁ d₂ : Core.Scale.Degree max) (S : Semantics.Supervaluation.SpecSpace (Core.Scale.Threshold max)) (hgt : d₂.toNat < d₁.toNat) (hd₂ : superTrueAt (fun (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) => decide (d.toNat > θ.toNat)) d₂ S = Core.Duality.Truth3.true) : superTrueAt (fun (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) => decide (d.toNat > θ.toNat)) d₁ S = Core.Duality.Truth3.true

Comparative entailment. If d₁ > d₂ and d₂ is super-true for a positive (upward) predicate, then d₁ is also super-true.

This captures Fine's internal penumbral connection: if Herbert is to be bald, then so is the man with fewer hairs (p. 276).

Fine's resolution: the tolerance premise "if n hairs is bald, then n+1 hairs is bald" is SUPER-FALSE. For every admissible threshold θ, there exists an n (= θ) where n is below θ but n+1 is above. The premise fails at every precisification.

theorem Phenomena.Gradability.Studies.Fine1975.tolerance_fails_at_boundary {max : ℕ} (d d' : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) (hd : d.toNat > θ.toNat) (hd' : ¬d'.toNat > θ.toNat) : ¬(d.toNat > θ.toNat → d'.toNat > θ.toNat)

The tolerance premise fails at any threshold separating d from d'.

Fine's most distinctive examples involve external penumbral connections between different predicates. A blob on the border of pink and red is borderline pink and borderline red. Yet "the blob is pink AND red" is super-false, because no admissible specification makes something both pink and red.

We model this with a single threshold governing both: "pink" = above
threshold, "red" = at or below threshold. The same threshold
determines both predicates, creating the penumbral connection. 

def Phenomena.Gradability.Studies.Fine1975.isPink {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : Bool

Pink: degree above the boundary (on a single color dimension).

Equations

• Phenomena.Gradability.Studies.Fine1975.isPink d θ = decide (d.toNat > θ.toNat)

def Phenomena.Gradability.Studies.Fine1975.isRed {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : Bool

Red: degree at or below the boundary (complementary to pink).

Equations

• Phenomena.Gradability.Studies.Fine1975.isRed d θ = decide (d.toNat ≤ θ.toNat)

theorem Phenomena.Gradability.Studies.Fine1975.pink_red_complementary {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : (isPink d θ && isRed d θ) = false

Pink and red are complementary: nothing can be both.

theorem Phenomena.Gradability.Studies.Fine1975.pink_and_red_superFalse {max : ℕ} (d : Core.Scale.Degree max) (S : Semantics.Supervaluation.SpecSpace (Core.Scale.Threshold max)) : Semantics.Supervaluation.superTrue (fun (θ : Core.Scale.Threshold max) => isPink d θ && isRed d θ) S = Core.Duality.Truth3.false

"The blob is pink and red" is super-false. Even when both conjuncts are individually indefinite, their conjunction is false on every precisification, hence super-false.

This is Fine's central argument for supervaluationism over truth-functional three-valued logic (p. 269-270). In Strong Kleene logic, indet ∧ indet = indet; supervaluation gives false.

theorem Phenomena.Gradability.Studies.Fine1975.pink_indefinite_example : Semantics.Supervaluation.superTrue (isPink { value := ⟨5, ⋯⟩ }) { admissible := {{ value := ⟨3, ⋯⟩ }, { value := ⟨7, ⋯⟩ }}, nonempty := ⋯ } = Core.Duality.Truth3.indet

Both "pink" and "red" can individually be indefinite (borderline).

The inGapRegion function in Adjective.Theory computes whether a degree falls between two thresholds (the "borderline" zone for contrary antonyms). A ThresholdPair with neg ≤ pos is a two-element specification space, and the gap region is exactly the set of degrees that receive Truth3.indet under supervaluation.

def Phenomena.Gradability.Studies.Fine1975.specOfPair {max : ℕ} (tp : Semantics.Lexical.Adjective.ThresholdPair max) : Semantics.Supervaluation.SpecSpace (Core.Scale.Threshold max)

The specification space induced by a threshold pair.

Equations

• Phenomena.Gradability.Studies.Fine1975.specOfPair tp = { admissible := {tp.neg, tp.pos}, nonempty := ⋯ }

theorem Phenomena.Gradability.Studies.Fine1975.inGapRegion_le_pos {max : ℕ} (d : Core.Scale.Degree max) (tp : Semantics.Lexical.Adjective.ThresholdPair max) (h : Semantics.Lexical.Adjective.inGapRegion d tp = true) : d.toNat ≤ tp.pos.toNat

Extract Nat-level upper bound from inGapRegion.

theorem Phenomena.Gradability.Studies.Fine1975.inGapRegion_ge_neg {max : ℕ} (d : Core.Scale.Degree max) (tp : Semantics.Lexical.Adjective.ThresholdPair max) (h : Semantics.Lexical.Adjective.inGapRegion d tp = true) : tp.neg.toNat ≤ d.toNat

Extract Nat-level lower bound from inGapRegion.

theorem Phenomena.Gradability.Studies.Fine1975.gap_implies_disagreement {max : ℕ} (d : Core.Scale.Degree max) (tp : Semantics.Lexical.Adjective.ThresholdPair max) (h_in : Semantics.Lexical.Adjective.inGapRegion d tp = true) (h_strict : tp.neg.toNat < d.toNat) : decide (d.toNat > tp.neg.toNat) = true ∧ decide (d.toNat > tp.pos.toNat) = false

When a degree is strictly inside the gap, the positive-meaning predicate disagrees across the two thresholds: true at the negative threshold, false at the positive.

Fine's D operator (§ 5) applied to threshold semantics. DA is true iff A is true at ALL thresholds in the space. Iterated application (DDA, DDDA, ...) collapses: since D is constant across specification points, DD = D. Higher-order vagueness in Fine's framework arises not from iterating D within a fixed space, but from the specification space itself being vague — requiring nested spaces (boundaries of boundaries). We do not formalize nested spaces here.

theorem Phenomena.Gradability.Studies.Fine1975.D_idempotent {Spec : Type u_1} (eval : Spec → Bool) (S : Semantics.Supervaluation.SpecSpace Spec) : Semantics.Supervaluation.definitely (fun (x : Spec) => Semantics.Supervaluation.definitely eval S) S = Semantics.Supervaluation.definitely eval S

D collapses under iteration: DD = D. Since definitely eval S is a constant Bool (independent of the specification point), applying D again yields the same value.

theorem Phenomena.Gradability.Studies.Fine1975.excludedMiddle_captured : Vagueness.excludedMiddle.supervaluationismCaptures = true

Excluded middle data says supervaluationism captures it; Supervaluation.Basic.excludedMiddle_superTrue proves this.

theorem Phenomena.Gradability.Studies.Fine1975.nonContradiction_captured : Vagueness.nonContradiction.supervaluationismCaptures = true

Non-contradiction data says supervaluationism captures it; Supervaluation.Basic.nonContradiction_superFalse proves this.

theorem Phenomena.Gradability.Studies.Fine1975.comparativeEntailment_captured : Vagueness.comparativeEntailment.supervaluationismCaptures = true

Comparative entailment data says supervaluationism captures it; comparative_entailment proves this.

theorem Phenomena.Gradability.Studies.Fine1975.definitelyOperator_eliminates : Vagueness.definitelyOperator.eliminatesBorderline = true

The D operator data says it eliminates borderline cases; Supervaluation.Basic.definitely_iff_superTrue shows D = super-truth.