Supervaluation Framework

@cite{fine-1975} @cite{kamp-1975}

General supervaluation theory for vague languages. A vague sentence is super-true iff true under all admissible precisifications, super-false iff false under all, and indefinite otherwise.

Key Results

• Classical biconditional: super-validity ↔ classical validity
• Consequence preservation: super-consequence = classical consequence
• Penumbral connections: logical relations preserved in borderline region
• D operator: satisfies T axiom (DA → A) but not converse (A → DA)
• Stability: restricting the specification space preserves definite truth
• Kamp's dilemma resolved: P ∧ P ≢ P ∧ ¬P under supervaluation, unlike any truth-functional three-valued logic

Architecture

This file provides the general supervaluation framework, parameterized by an abstract specification type Spec. Study files specialize Spec:

• Threshold max for gradable adjectives (@cite{fine-1975})
• ComparisonClass Entity for delineation (@cite{klein-1980})
• Product types for multi-predicate penumbral connections

Fine's full framework includes partial specifications with an extension relation, but he shows (p. 277) that partial points can be identified with sets of complete points, and extension = subset. We use this simplified complete-point-only representation.

structure Semantics.Supervaluation.SpecSpace (Spec : Type u_1) : Type u_1

A specification space: a non-empty finite set of admissible complete specifications. Each element represents one way of making all vague predicates precise simultaneously.

• admissible : Finset Spec
• nonempty : self.admissible.Nonempty

def Semantics.Supervaluation.SpecSpace.singleton {Spec : Type u_1} [DecidableEq Spec] (s : Spec) : SpecSpace Spec

Singleton specification space: a single admissible precisification. Classical models are degenerate specification spaces.

Equations

• Semantics.Supervaluation.SpecSpace.singleton s = { admissible := {s}, nonempty := ⋯ }

def Semantics.Supervaluation.superTrue {Spec : Type u_1} (eval : Spec → Bool) (S : SpecSpace Spec) : Core.Duality.Truth3

Supervaluation operator. Maps a Bool-valued predicate over specifications to a three-valued truth value:

• Truth3.true if true at ALL admissible specifications
• Truth3.false if false at ALL admissible specifications
• Truth3.indet otherwise (the borderline case)

Equations

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

def Semantics.Supervaluation.definitely {Spec : Type u_1} (eval : Spec → Bool) (S : SpecSpace Spec) : Bool

The D (definitely) operator. DA is true iff A is true at ALL admissible specifications — i.e., A is super-true. In modal logic terms, D is □ in S5 with universal access among specification points.

Equations

• Semantics.Supervaluation.definitely eval S = decide (∀ s ∈ S.admissible, eval s = true)

def Semantics.Supervaluation.indefinite {Spec : Type u_1} (eval : Spec → Bool) (S : SpecSpace Spec) : Bool

The I (indefinite) operator. IA ≡ ¬DA ∧ ¬D¬A: A is neither definitely true nor definitely false.

Equations

• Semantics.Supervaluation.indefinite eval S = (!Semantics.Supervaluation.definitely eval S && !Semantics.Supervaluation.definitely (fun (s : Spec) => !eval s) S)

theorem Semantics.Supervaluation.superTrue_true_iff {Spec : Type u_1} (eval : Spec → Bool) (S : SpecSpace Spec) : superTrue eval S = Core.Duality.Truth3.true ↔ ∀ s ∈ S.admissible, eval s = true

Super-truth ↔ universally true across the space.

theorem Semantics.Supervaluation.superTrue_false_iff {Spec : Type u_1} (eval : Spec → Bool) (S : SpecSpace Spec) : superTrue eval S = Core.Duality.Truth3.false ↔ ∀ s ∈ S.admissible, eval s = false

Super-falsity ↔ universally false across the space.

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

Indefiniteness ↔ witnesses on both sides.

theorem Semantics.Supervaluation.definitely_iff_superTrue {Spec : Type u_1} (eval : Spec → Bool) (S : SpecSpace Spec) : definitely eval S = true ↔ superTrue eval S = Core.Duality.Truth3.true

D = super-truth projected to Bool.

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

Excluded middle is super-true. P ∨ ¬P is true on every precisification, hence true on ALL. Classical tautologies survive.

theorem Semantics.Supervaluation.nonContradiction_superFalse {Spec : Type u_1} (eval : Spec → Bool) (S : SpecSpace Spec) : superTrue (fun (s : Spec) => eval s && !eval s) S = Core.Duality.Truth3.false

Non-contradiction is super-false. P ∧ ¬P is false on every precisification, hence false on ALL.

theorem Semantics.Supervaluation.complementary_superFalse {Spec : Type u_1} (P Q : Spec → Bool) (S : SpecSpace Spec) (hcomp : ∀ s ∈ S.admissible, (P s && Q s) = false) : superTrue (fun (s : Spec) => P s && Q s) S = Core.Duality.Truth3.false

Complementary predicates. If P and Q never hold simultaneously at any admissible specification, their conjunction is super-false.

This is Fine's "external penumbral connection": the relationship between "pink" and "red" across the color boundary (p. 270).

theorem Semantics.Supervaluation.conjunction_self {Spec : Type u_1} (eval : Spec → Bool) (S : SpecSpace Spec) : superTrue (fun (s : Spec) => eval s && eval s) S = superTrue eval S

Conjunction with self. P ∧ P has the same super-truth value as P. This is trivial (Bool.and_self), but combined with nonContradiction_superFalse, it resolves Kamp's dilemma: supervaluation distinguishes P ∧ P from P ∧ ¬P, while Strong Kleene three-valued logic maps both to indet when P is borderline.

Fine's central logical result (§ 4): the super-truth theory yields classical logic. A formula is super-valid (super-true in every specification space) iff it is classically valid (true in every classical model). Each direction has a clean proof.

theorem Semantics.Supervaluation.classical_implies_superValid {Spec : Type u_1} (eval : Spec → Bool) (htaut : ∀ (s : Spec), eval s = true) (S : SpecSpace Spec) : superTrue eval S = Core.Duality.Truth3.true

Forward: classical tautology → super-valid.

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

Converse: super-valid → classical tautology. The key step: each classical model is a singleton specification space. If eval is super-true in the singleton {s}, then eval s = true.

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

Super-validity ↔ classical validity. This is the deepest logical result in @cite{fine-1975}: supervaluationism makes a difference to truth but not to logic.

def Semantics.Supervaluation.superConsequence {Spec : Type u_1} (evalA evalB : Spec → Bool) : Prop

Super-consequence: B follows from A iff B is super-true whenever A is, across all specification spaces.

Equations

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

theorem Semantics.Supervaluation.classical_implies_superConsequence {Spec : Type u_1} (evalA evalB : Spec → Bool) (h : ∀ (s : Spec), evalA s = true → evalB s = true) : superConsequence evalA evalB

Forward: classical consequence → super-consequence.

theorem Semantics.Supervaluation.superConsequence_implies_classical {Spec : Type u_1} [DecidableEq Spec] (evalA evalB : Spec → Bool) (h : superConsequence evalA evalB) (s : Spec) : evalA s = true → evalB s = true

Converse: super-consequence → classical consequence.

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

Super-consequence ↔ classical consequence.

Fine's Stability condition (S): definite truth values are preserved under extension. In our complete-point-only representation, "extension" = restricting the set of admissible specifications (making the language more precise by ruling out some precisifications). Stability says super-truth is preserved under restriction — i.e., it is monotone with respect to the subset ordering on specification spaces.

theorem Semantics.Supervaluation.stability_superTrue {Spec : Type u_1} (eval : Spec → Bool) (S T : SpecSpace Spec) (hsub : T.admissible ⊆ S.admissible) (hst : superTrue eval S = Core.Duality.Truth3.true) : superTrue eval T = Core.Duality.Truth3.true

Restricting the specification space preserves super-truth.

theorem Semantics.Supervaluation.stability_superFalse {Spec : Type u_1} (eval : Spec → Bool) (S T : SpecSpace Spec) (hsub : T.admissible ⊆ S.admissible) (hsf : superTrue eval S = Core.Duality.Truth3.false) : superTrue eval T = Core.Duality.Truth3.false

Restricting the specification space preserves super-falsity.

theorem Semantics.Supervaluation.stability_definite {Spec : Type u_1} (eval : Spec → Bool) (S T : SpecSpace Spec) (hsub : T.admissible ⊆ S.admissible) (hdef : superTrue eval S ≠ Core.Duality.Truth3.indet) : superTrue eval T ≠ Core.Duality.Truth3.indet

Restriction can resolve indefiniteness but never create it. If A is definite (true or false) in S, it stays definite in T ⊆ S.

Fine's D operator (§ 5) is the modal necessity operator □ on specification spaces. DA is true at a specification point iff A is true at ALL specification points (S5 with universal access). Since D is constant across points, DA → A is super-valid (the T axiom), but A → DA is not (A may hold at this point but fail at another).

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

T axiom: DA → A is super-valid. Material implication ¬(DA) ∨ A is true at every specification point: either D is false (the disjunction holds) or D is true and A holds at all points.

theorem Semantics.Supervaluation.A_not_implies_DA : ∃ (eval : Bool → Bool) (S : SpecSpace Bool), superTrue (fun (s : Bool) => !eval s || definitely eval S) S ≠ Core.Duality.Truth3.true

Converse fails: A → DA is NOT super-valid. Counterexample: two specification points, eval = id, space = {true, false}. At point true: A is true but DA is false (A fails at false). So A → DA is false at true, hence not super-true.

theorem Semantics.Supervaluation.DA_consequence_of_A {Spec : Type u_1} (eval : Spec → Bool) (S : SpecSpace Spec) : superTrue eval S = Core.Duality.Truth3.true → superTrue (fun (x : Spec) => definitely eval S) S = Core.Duality.Truth3.true

DA is a consequence of A. If A is super-true, then DA is super-true (since DA just says "A is true at all specs"). Combined with A_not_implies_DA, this shows the asymmetry characteristic of supervaluationism (Fine § 5, p. 290): asserting A commits one to DA, but A → DA is not a logical truth.

theorem Semantics.Supervaluation.fidelity {Spec : Type u_1} [DecidableEq Spec] (eval : Spec → Bool) (s : Spec) : superTrue eval (SpecSpace.singleton s) ≠ Core.Duality.Truth3.indet

Fidelity: at a singleton specification space (a complete specification / classical model), every sentence is either true or false — never indefinite. Supervaluation reduces to classical evaluation.