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 maxfor gradable adjectives (@cite{fine-1975})ComparisonClass Entityfor 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.
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
Instances For
Specification spaces ordered by reverse inclusion on admissible
sets: S ≤ T iff T.admissible ⊆ S.admissible. A "larger" spec
space in this ordering has fewer admissible specs — it is more
precise. This is the information ordering: more precision = more
information = higher in the order.
Fine's Stability condition (§ 7) says super-truth is Antitone
under this ordering: making the language more precise (restricting
admissible specs) preserves definite truth values.
Equations
- Semantics.Supervaluation.instPreorderSpecSpace = { le := fun (S T : Semantics.Supervaluation.SpecSpace Spec) => T.admissible ⊆ S.admissible, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
Singleton specification space: a single admissible precisification. Classical models are degenerate specification spaces.
Equations
- Semantics.Supervaluation.SpecSpace.singleton s = { admissible := {s}, nonempty := ⋯ }
Instances For
Supervaluation operator. Maps a Prop-valued predicate over specifications to a three-valued truth value:
Truth3.trueif the predicate holds at ALL admissible specificationsTruth3.falseif the predicate fails at ALL admissible specificationsTruth3.indetotherwise (the borderline case)
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 = ∀ s ∈ S.admissible, eval s
Instances For
Equations
- Semantics.Supervaluation.definitely.instDecidable eval S = id inferInstance
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)
Instances For
Equations
- Semantics.Supervaluation.indefinite.instDecidable eval S = id inferInstance
Super-truth ↔ universally true across the space.
Super-falsity ↔ universally false across the space.
Indefiniteness ↔ witnesses on both sides.
superTrue is Core.Duality.dist on the admissible Finset.
The bridge between Fine 1975 supervaluation (this file) and the
canonical trivalent classifier (Core.Duality.dist in
Linglib/Core/Logic/Duality.lean). Both are van Fraassen 1966's
supervaluation construction; dist is the more general form
parameterized over an arbitrary Finset α + (α → Prop), while
superTrue adds the SpecSpace wrapper (admissible Finset +
nonemptiness witness) and Fine's specification-space ordering.
On the empty case the two agree definitionally (both give .true
vacuously), but SpecSpace rules out empty admissible sets by
construction so the empty case never arises here.
D = super-truth projected to its Prop characterization.
Excluded middle is super-true. P ∨ ¬P is true on every precisification, hence true on ALL. Classical tautologies survive.
Non-contradiction is super-false. P ∧ ¬P is false on every precisification, hence false on ALL.
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).
Conjunction with self. P ∧ P has the same super-truth value as P.
This is trivial (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.
Forward: classical tautology → super-valid.
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 holds.
Super-validity ↔ classical validity. This is the deepest logical result in @cite{fine-1975}: supervaluationism makes a difference to truth but not to logic.
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.
Instances For
Forward: classical consequence → super-consequence.
Converse: super-consequence → classical consequence.
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.
Restricting the specification space preserves super-truth.
Restricting the specification space preserves super-falsity.
Restriction can resolve indefiniteness but never create it. If A is definite (true or false) in S, it stays definite in T ⊆ S.
Stability as antitonicity: super-truth is preserved under
the information ordering on spec spaces (= reverse inclusion on
admissible sets). Making the language more precise (S ≤ T, i.e.,
T.admissible ⊆ S.admissible) preserves super-truth.
This is Mathlib's Antitone applied to superTrue eval with
the codomain ordered by Truth3.true ≤ · ≤ Truth3.true (super-truth
entails super-truth). The theorem says: if superTrue eval S = .true
and S ≤ T (T is more precise), then superTrue eval T = .true.
The full antitonicity on Truth3's lattice ordering does NOT hold
(restriction can turn indet into true), but this weaker
preservation-of-definiteness property is what matters for Fine.
Dual: super-falsity is also preserved under the information ordering.
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).
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.
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.
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.
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.