Fine (1975): Vagueness, truth and logic

Fine argues for the super-truth theory of vagueness. §1 treats Indefinite as a third truth-value: a partial specification assigns True, False or Indefinite to the atomic sentences, and a truth-functional valuation is constrained by Fidelity — classical on definite values — and Stability — definite values preserved under extension (the knowledge order SignType.toFlat). Those two conditions fix negation (neg_eq_of_faithful_stable) and leave a commutative conjunction exactly the minimizing and maximizing options of Kleene's weak and strong tables (conj_eq_inf_or_meetWeak). Yet no truth-functional account respects penumbral connection: with the blob on the border of pink and red, pink and red is false while pink and pink is indefinite, though every conjunct is indefinite (maximal_pink_and_red, conj_not_truthFunctional, and likewise for disjunction). §2 answers with specification spaces: points partially ordered by extension, complete points to which every point extends (Completability), and super-truth at a point as truth at all its complete extensions (SuperTrue), which satisfies Fidelity and Stability (superTrue_iff_of_isMax, SuperTrue.mono); the partial points are recovered from the complete ones as the sets of their completions, extension becoming inclusion (completions, completions_mono), and super-truth at a point is SignType.supervaluation over its completions (superTrue_completions). §3 argues that the theory is forced: an account satisfying Fidelity, Stability and Resolution is the super-truth account (Account.eq_superTruth_of_resolves), and the A-clauses — Resolution for atoms, the classical clauses for negation, and for conjunction the truth clause with the falsity clause that redeems its pledge — are equivalent to it (superTruth_aClauses, Account.eq_superTruth_of_aClauses). §4 draws the logic: validity and consequence are classical, since a classical model is a degenerate specification space (superValid_iff_classical, superConsequence_iff_classical), the law of excluded middle holds where bivalence fails (herbert_lem, herbert_indet), and the sorites' tolerance premise is false because a hair-splitting number exists in every complete specification (tolerance_superFalse). §5 adds the definitely-operator: on the truth-value approach it breaks Stability (metaAssert_not_stable); on specification spaces I A := ¬DA ∧ ¬D¬A, D is an S5 modality over the complete specifications (definitely_imp_valid, definitely_definitely_iff, not_definitely_definitely) whose falsity is not preserved into a more precise space (not_definitely_antitone), the Deduction Theorem fails, DA being a consequence of A while A ⊃ DA is indefinite where A is (superTrue_definitely_of_superTrue, superTrue_imp_definitely_of_indet), and consequence is validity of DA ⊃ B (superConsequence_iff_definitely_imp). Higher-order vagueness is truth relative to boundaries — nested admissible spaces — under an accessibility that is reflexive but not transitive, so that the logic of D is T (Boundary.R_refl, Boundary.definitely_self, Boundary.R_not_trans). The construction is van Fraassen's supervaluation, whose conservative and radical variants are the minimizing and maximizing options; Fine's note added in proof credits the same account of vagueness to Kamp and to Lewis.

Implementation notes

• A specification space is the class SpecificationSpace over a partial order: Completability, with the complete points the maximal ones. A complete point admits no proper extension when points are specifications (the extensional account of §2), and Fidelity needs it, since super-truth at a complete point with a further complete extension would not be classical; under Completability the maximal points are then exactly the complete ones. The §2 reduction takes a point to the finite set of its completions (completions); a reduced space is a Finset of complete specifications, more precise spaces being smaller sets.
• Partial specifications are Atom → Flat Bool with the pointwise knowledge order, so that extension is the order of Flat; they instantiate the class (isMax_iff). Connectives are evaluated on SignType, whose strong Kleene tables are the maximizing account and meetWeak the minimizing one; its logic with True designated (Trivalent.k3_no_tautologies) has no valid formulas, as §4 observes.
• The examples are Fine's: bald over hair counts with the admissible thresholds 40 to 60 of §5 (Herbert at 50 hairs, Yul Brynner at 0, the million-haired man), and the blob at hue 5 with colour boundaries 3 to 7; the intuitionistic and anticipatory accounts, the infinite- order truth-values and the hierarchy of truth-predicates are not formalized.
• Sentences in §3 are Trivalent.Formula without quantifiers, so the A-clause for ∀ is absent; they are classically evaluated at a point by Formula.evalBool on the point's atomic values, which is their K3 realization on that Boolean model (Formula.realize_ofBool).

References

• [Fin75]
• [Kle52]
• [vF66]
• [VF69]
• [Kam75]
• [Lew70]

The truth-value approach (§1)

def Fine1975.Faithful (f : SignType → SignType → SignType) (g : Bool → Bool → Bool) : Prop

A connective satisfies Fidelity when it is classical on definite values.

Equations

• Fine1975.Faithful f g = ∀ (x y : Bool), f (SignType.ofProp (x = true)) (SignType.ofProp (y = true)) = SignType.ofProp (g x y = true)

def Fine1975.Stable (f : SignType → SignType → SignType) : Prop

A connective satisfies Stability when it preserves definite values as its arguments are extended, that is, when it is monotone in the knowledge order.

Equations

• Fine1975.Stable f = ∀ (a a' b b' : SignType), a.toFlat ≤ a'.toFlat → b.toFlat ≤ b'.toFlat → (f a b).toFlat ≤ (f a' b').toFlat

theorem Fine1975.neg_eq_of_faithful_stable (n : SignType → SignType) (hF : ∀ (x : Bool), n (SignType.ofProp (x = true)) = SignType.ofProp ((!x) = true)) (hS : ∀ (a a' : SignType), a.toFlat ≤ a'.toFlat → (n a).toFlat ≤ (n a').toFlat) : n = Neg.neg

Fidelity and Stability determine negation as [Kle52]'s.

theorem Fine1975.conj_eq_inf_or_meetWeak (f : SignType → SignType → SignType) (hF : Faithful f fun (x1 x2 : Bool) => x1 && x2) (hS : Stable f) (hC : ∀ (a b : SignType), f a b = f b a) : (f = fun (x1 x2 : SignType) => min x1 x2) ∨ f = SignType.meetWeak

A commutative conjunction satisfying Fidelity and Stability is the maximizing strong Kleene ⊓ or the minimizing weak Kleene meetWeak, which differ only on an indefinite conjunct beside a false one.

The blob on the border of pink and red (§1, §3): a colour boundary between hue 3 and hue 7 is admissible, the blob has hue 5, and pink is above the boundary, red at or below it.

def Fine1975.colour : Finset ℕ

The admissible colour boundaries.

Equations

• Fine1975.colour = Finset.Icc 3 7

@[reducible, inline]

abbrev Fine1975.pink (hue θ : ℕ) : Prop

x is pink when its hue is above the boundary.

Equations

• Fine1975.pink hue θ = (θ < hue)

@[reducible, inline]

abbrev Fine1975.red (hue θ : ℕ) : Prop

x is red when its hue is at or below the boundary.

Equations

• Fine1975.red hue θ = (hue ≤ θ)

theorem Fine1975.pink_indet : SignType.supervaluation colour (pink 5) = 0

The blob is pink is indefinite.

theorem Fine1975.red_indet : SignType.supervaluation colour (red 5) = 0

The blob is red is indefinite.

theorem Fine1975.pink_and_red_false : (SignType.supervaluation colour fun (θ : ℕ) => pink 5 θ ∧ red 5 θ) = -1

The blob is pink and red is false, since the predicates are contraries.

theorem Fine1975.pink_or_red_true : (SignType.supervaluation colour fun (θ : ℕ) => pink 5 θ ∨ red 5 θ) = 1

The blob is pink or red is true, since the predicates are complementary over the range.

theorem Fine1975.pink_imp_not_red_true : (SignType.supervaluation colour fun (θ : ℕ) => pink 5 θ → ¬red 5 θ) = 1

If the blob is pink, it is not red is a penumbral truth, where if pink, not pink is not true.

theorem Fine1975.pink_imp_not_pink_indet : (SignType.supervaluation colour fun (θ : ℕ) => pink 5 θ → ¬pink 5 θ) = 0

theorem Fine1975.maximal_pink_and_red : min (SignType.supervaluation colour (pink 5)) (SignType.supervaluation colour (red 5)) = 0

Even the maximizing account makes pink and red indefinite, as both conjuncts are.

theorem Fine1975.conj_not_truthFunctional : ¬∃ (f : SignType → SignType → SignType), ∀ (P Q : ℕ → Prop) [inst : DecidablePred P] [inst_1 : DecidablePred Q], (SignType.supervaluation colour fun (θ : ℕ) => P θ ∧ Q θ) = f (SignType.supervaluation colour P) (SignType.supervaluation colour Q)

No truth-functional conjunction respects penumbral connection, since pink and pink and pink and red have indefinite conjuncts alike, but the first is indefinite and the second false.

theorem Fine1975.disj_not_truthFunctional : ¬∃ (f : SignType → SignType → SignType), ∀ (P Q : ℕ → Prop) [inst : DecidablePred P] [inst_1 : DecidablePred Q], (SignType.supervaluation colour fun (θ : ℕ) => P θ ∨ Q θ) = f (SignType.supervaluation colour P) (SignType.supervaluation colour Q)

Nor does any truth-functional disjunction, since pink or pink is indefinite and pink or red true.

Specification spaces (§2)

class Fine1975.SpecificationSpace (Point : Type u_1) [PartialOrder Point] : Prop

In a specification space the points are partially ordered by extension, every point extends to a complete point (Completability), and the complete points are the maximal ones.

• completable (t : Point) : ∃ (u : Point), t ≤ u ∧ IsMax u

  Every point extends to a complete point (Completability).

def Fine1975.SuperTrue {Point : Type u_1} [PartialOrder Point] (A : Point → Prop) (t : Point) : Prop

A sentence is super-true at a point when it is true at every complete extension.

Equations

• Fine1975.SuperTrue A t = ∀ (u : Point), t ≤ u → IsMax u → A u

def Fine1975.SuperFalse {Point : Type u_1} [PartialOrder Point] (A : Point → Prop) (t : Point) : Prop

A sentence is super-false at a point when it is false at every complete extension.

Equations

• Fine1975.SuperFalse A t = ∀ (u : Point), t ≤ u → IsMax u → ¬A u

theorem Fine1975.superTrue_iff_of_isMax {Point : Type u_1} [PartialOrder Point] {A : Point → Prop} {t : Point} (ht : IsMax t) : SuperTrue A t ↔ A t

At a complete point super-truth is classical truth (Fidelity).

theorem Fine1975.superFalse_iff_of_isMax {Point : Type u_1} [PartialOrder Point] {A : Point → Prop} {t : Point} (ht : IsMax t) : SuperFalse A t ↔ ¬A t

Fidelity for falsity.

theorem Fine1975.SuperTrue.mono {Point : Type u_1} [PartialOrder Point] {A : Point → Prop} {t u : Point} (h : SuperTrue A t) (htu : t ≤ u) : SuperTrue A u

Super-truth is preserved under extension (Stability).

theorem Fine1975.SuperFalse.mono {Point : Type u_1} [PartialOrder Point] {A : Point → Prop} {t u : Point} (h : SuperFalse A t) (htu : t ≤ u) : SuperFalse A u

Stability for falsity.

theorem Fine1975.exists_superFalse_of_not_superTrue {Point : Type u_1} [PartialOrder Point] {A : Point → Prop} {t : Point} (h : ¬SuperTrue A t) : ∃ (u : Point), t ≤ u ∧ SuperFalse A u

A sentence not super-true at a point is super-false at some extension (Resolution).

theorem Fine1975.exists_superTrue_of_not_superFalse {Point : Type u_1} [PartialOrder Point] {A : Point → Prop} {t : Point} (h : ¬SuperFalse A t) : ∃ (u : Point), t ≤ u ∧ SuperTrue A u

Resolution for falsity.

theorem Fine1975.superTrue_not_iff {Point : Type u_1} [PartialOrder Point] {A : Point → Prop} {t : Point} : SuperTrue (fun (u : Point) => ¬A u) t ↔ SuperFalse A t

Super-truth of ¬A is super-falsity of A.

theorem Fine1975.superFalse_not_iff {Point : Type u_1} [PartialOrder Point] {A : Point → Prop} {t : Point} : SuperFalse (fun (u : Point) => ¬A u) t ↔ SuperTrue A t

theorem Fine1975.superTrue_and_iff {Point : Type u_1} [PartialOrder Point] {A B : Point → Prop} {t : Point} : SuperTrue (fun (u : Point) => A u ∧ B u) t ↔ SuperTrue A t ∧ SuperTrue B t

A conjunction is super-true iff both conjuncts are.

def Fine1975.completions {Point : Type u_1} [PartialOrder Point] [Fintype Point] [DecidableLE Point] [DecidablePred IsMax] (t : Point) : Finset Point

The completions of a point are its complete extensions, Fine's reduced specification space.

Equations

• Fine1975.completions t = {u : Point | t ≤ u ∧ IsMax u}

theorem Fine1975.completions_nonempty {Point : Type u_1} [PartialOrder Point] [Fintype Point] [DecidableLE Point] [DecidablePred IsMax] [SpecificationSpace Point] (t : Point) : (completions t).Nonempty

theorem Fine1975.superTrue_completions {Point : Type u_1} [PartialOrder Point] {A : Point → Prop} {t : Point} [Fintype Point] [DecidableLE Point] [DecidablePred IsMax] [DecidablePred A] : SignType.supervaluation (completions t) A = 1 ↔ SuperTrue A t

Super-truth at a point is super-truth over its completions.

theorem Fine1975.completions_mono {Point : Type u_1} [PartialOrder Point] {t u : Point} [Fintype Point] [DecidableLE Point] [DecidablePred IsMax] (htu : t ≤ u) : completions u ⊆ completions t

Extension of points is reverse inclusion of completions.

theorem Fine1975.superFalse_and_iff {Point : Type u_1} [PartialOrder Point] {A B : Point → Prop} {t : Point} [SpecificationSpace Point] : SuperFalse (fun (u : Point) => A u ∧ B u) t ↔ ∀ (u : Point), t ≤ u → ∃ (v : Point), u ≤ v ∧ (SuperFalse A v ∨ SuperFalse B v)

A conjunction is super-false iff every extension has a further extension at which a conjunct is super-false, so that the falsehood pledge is redeemed.

Partial specifications

@[reducible, inline]

abbrev Fine1975.Specification (Atom : Type u_1) : Type u_1

A partial specification makes each atom True, False or undecided. It is ordered pointwise by the knowledge order, so that u extends t when it assigns every definite value t does.

Equations

• Fine1975.Specification Atom = (Atom → Flat Bool)

theorem Fine1975.isMax_iff {Atom : Type u_1} {t : Specification Atom} : IsMax t ↔ ∀ (a : Atom), t a ≠ ⊥

A specification is complete, maximal in the extension order, iff it decides every atom.

instance Fine1975.instSpecificationSpaceSpecification {Atom : Type u_1} : SpecificationSpace (Specification Atom)

The super-truth theory (§3)

structure Fine1975.Account (Point : Type u_3) (Sentence : Type u_4) : Type (max u_3 u_4)

An account of truth and falsity at points gives the relations ⊨ and ⊣.

• verifies : Point → Sentence → Prop
• falsifies : Point → Sentence → Prop

def Fine1975.Account.Faithful {Point : Type u_1} {Sentence : Type u_2} [PartialOrder Point] (V : Account Point Sentence) (c : Point → Sentence → Prop) : Prop

At complete points the account agrees with a classical valuation (Fidelity).

Equations

• V.Faithful c = ∀ (t : Point) (A : Sentence), IsMax t → (V.verifies t A ↔ c t A) ∧ (V.falsifies t A ↔ ¬c t A)

def Fine1975.Account.Stable {Point : Type u_1} {Sentence : Type u_2} [PartialOrder Point] (V : Account Point Sentence) : Prop

Truth and falsity are preserved under extension (Stability).

Equations

• V.Stable = ∀ (t u : Point) (A : Sentence), t ≤ u → (V.verifies t A → V.verifies u A) ∧ (V.falsifies t A → V.falsifies u A)

def Fine1975.Account.Resolves {Point : Type u_1} {Sentence : Type u_2} [PartialOrder Point] (V : Account Point Sentence) (A : Sentence) : Prop

Resolution holds at a sentence when what is not true is false at some extension, and what is not false is true at some extension.

Equations

• V.Resolves A = ∀ (t : Point), (¬V.verifies t A → ∃ (u : Point), t ≤ u ∧ V.falsifies u A) ∧ (¬V.falsifies t A → ∃ (u : Point), t ≤ u ∧ V.verifies u A)

def Fine1975.superTruth {Point : Type u_1} {Sentence : Type u_2} [PartialOrder Point] (c : Point → Sentence → Prop) : Account Point Sentence

The super-truth account over a classical valuation.

Equations

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

theorem Fine1975.superTruth_faithful {Point : Type u_1} {Sentence : Type u_2} [PartialOrder Point] (c : Point → Sentence → Prop) : (superTruth c).Faithful c

theorem Fine1975.superTruth_stable {Point : Type u_1} {Sentence : Type u_2} [PartialOrder Point] (c : Point → Sentence → Prop) : (superTruth c).Stable

theorem Fine1975.superTruth_resolves {Point : Type u_1} {Sentence : Type u_2} [PartialOrder Point] (c : Point → Sentence → Prop) (A : Sentence) : (superTruth c).Resolves A

theorem Fine1975.Account.verifies_iff {Point : Type u_1} {Sentence : Type u_2} [PartialOrder Point] [SpecificationSpace Point] {V : Account Point Sentence} {c : Point → Sentence → Prop} {A : Sentence} {t : Point} (hF : V.Faithful c) (hS : V.Stable) (hR : V.Resolves A) : V.verifies t A ↔ SuperTrue (fun (x : Point) => c x A) t

Under Fidelity, Stability and Resolution at A, truth at a point is super-truth. Stability carries truth up to every complete extension, and if some complete extension fails A while the point does not verify it, Resolution falsifies A at an extension, Completability and Stability at a complete one, where Fidelity contradicts.

theorem Fine1975.Account.falsifies_iff {Point : Type u_1} {Sentence : Type u_2} [PartialOrder Point] [SpecificationSpace Point] {V : Account Point Sentence} {c : Point → Sentence → Prop} {A : Sentence} {t : Point} (hF : V.Faithful c) (hS : V.Stable) (hR : V.Resolves A) : V.falsifies t A ↔ SuperFalse (fun (x : Point) => c x A) t

The falsity half of Account.verifies_iff.

theorem Fine1975.Account.eq_superTruth_of_resolves {Point : Type u_1} {Sentence : Type u_2} [PartialOrder Point] [SpecificationSpace Point] {V : Account Point Sentence} {c : Point → Sentence → Prop} (hF : V.Faithful c) (hS : V.Stable) (hR : ∀ (A : Sentence), V.Resolves A) : V = superTruth c

The super-truth account is the only one satisfying Fidelity, Completability, Stability and Resolution (§3).

def Fine1975.classical {Point : Type u_1} {Atom : Type u_2} (val : Point → Atom → Bool) (t : Point) (φ : Trivalent.Formula Atom) : Prop

Classical truth of a sentence at a point, on the point's atomic values.

Equations

• Fine1975.classical val t φ = (Trivalent.Formula.evalBool (val t) φ = true)

theorem Fine1975.classical_neg {Point : Type u_1} {Atom : Type u_2} (val : Point → Atom → Bool) (t : Point) (φ : Trivalent.Formula Atom) : classical val t φ.neg ↔ ¬classical val t φ

theorem Fine1975.classical_conj {Point : Type u_1} {Atom : Type u_2} (val : Point → Atom → Bool) (t : Point) (φ ψ : Trivalent.Formula Atom) : classical val t (φ.conj ψ) ↔ classical val t φ ∧ classical val t ψ

theorem Fine1975.classical_disj {Point : Type u_1} {Atom : Type u_2} (val : Point → Atom → Bool) (t : Point) (φ ψ : Trivalent.Formula Atom) : classical val t (φ.disj ψ) ↔ classical val t (φ.neg.conj ψ.neg).neg

Disjunction is classically the abbreviation ¬(¬φ ∧ ¬ψ).

theorem Fine1975.classical_cond {Point : Type u_1} {Atom : Type u_2} (val : Point → Atom → Bool) (t : Point) (φ ψ : Trivalent.Formula Atom) : classical val t (φ.cond ψ) ↔ classical val t (φ.conj ψ.neg).neg

The conditional is classically the abbreviation ¬(φ ∧ ¬ψ).

structure Fine1975.Account.AClauses {Point : Type u_1} {Atom : Type u_2} [PartialOrder Point] (V : Account Point (Trivalent.Formula Atom)) : Prop

The A-clauses of §3 are Resolution for atomic sentences, the classical clauses for negation, and for conjunction truth of both conjuncts and falsity that an extension falsifying a conjunct can always redeem; disjunction and the conditional are the abbreviations ¬(¬φ ∧ ¬ψ) and ¬(φ ∧ ¬ψ).

• resolves (a : Atom) : V.Resolves (Trivalent.Formula.atom a)
• verifies_neg (t : Point) (φ : Trivalent.Formula Atom) : V.verifies t φ.neg ↔ V.falsifies t φ
• falsifies_neg (t : Point) (φ : Trivalent.Formula Atom) : V.falsifies t φ.neg ↔ V.verifies t φ
• verifies_conj (t : Point) (φ ψ : Trivalent.Formula Atom) : V.verifies t (φ.conj ψ) ↔ V.verifies t φ ∧ V.verifies t ψ
• falsifies_conj (t : Point) (φ ψ : Trivalent.Formula Atom) : V.falsifies t (φ.conj ψ) ↔ ∀ (u : Point), t ≤ u → ∃ (v : Point), u ≤ v ∧ (V.falsifies v φ ∨ V.falsifies v ψ)
• verifies_disj (t : Point) (φ ψ : Trivalent.Formula Atom) : V.verifies t (φ.disj ψ) ↔ V.verifies t (φ.neg.conj ψ.neg).neg
• falsifies_disj (t : Point) (φ ψ : Trivalent.Formula Atom) : V.falsifies t (φ.disj ψ) ↔ V.falsifies t (φ.neg.conj ψ.neg).neg
• verifies_cond (t : Point) (φ ψ : Trivalent.Formula Atom) : V.verifies t (φ.cond ψ) ↔ V.verifies t (φ.conj ψ.neg).neg
• falsifies_cond (t : Point) (φ ψ : Trivalent.Formula Atom) : V.falsifies t (φ.cond ψ) ↔ V.falsifies t (φ.conj ψ.neg).neg

theorem Fine1975.superTruth_aClauses {Point : Type u_1} {Atom : Type u_2} [PartialOrder Point] [SpecificationSpace Point] (val : Point → Atom → Bool) : (superTruth (classical val)).AClauses

The super-truth account satisfies the A-clauses.

theorem Fine1975.Account.eq_superTruth_of_aClauses {Point : Type u_1} {Atom : Type u_2} [PartialOrder Point] {V : Account Point (Trivalent.Formula Atom)} {val : Point → Atom → Bool} [SpecificationSpace Point] (hF : V.Faithful (classical val)) (hS : V.Stable) (hA : V.AClauses) : V = superTruth (classical val)

Given Fidelity, Stability and Completability, the A-clauses force the super-truth account (§3), so the claims of penumbral connection force the favoured view.

The logic of vagueness (§4)

def Fine1975.SuperValid {Spec : Type u_1} (A : Spec → Prop) [DecidablePred A] : Prop

A sentence is valid when it is super-true in every specification space.

Equations

• Fine1975.SuperValid A = ∀ (S : Finset Spec), SignType.supervaluation S A = 1

def Fine1975.SuperConsequence {Spec : Type u_1} (A B : Spec → Prop) [DecidablePred A] [DecidablePred B] : Prop

B is a consequence of A when it is super-true in every specification space in which A is.

Equations

• Fine1975.SuperConsequence A B = ∀ (S : Finset Spec), SignType.supervaluation S A = 1 → SignType.supervaluation S B = 1

theorem Fine1975.superValid_iff_classical {Spec : Type u_1} (A : Spec → Prop) [DecidablePred A] : SuperValid A ↔ ∀ (s : Spec), A s

Validity is classical, since a classically valid sentence is true at every complete specification of every space, and a classical model is a degenerate space.

theorem Fine1975.superConsequence_iff_classical {Spec : Type u_1} (A B : Spec → Prop) [DecidablePred A] [DecidablePred B] : SuperConsequence A B ↔ ∀ (s : Spec), A s → B s

Consequence is classical, by the same argument.

bald

def Fine1975.baldness : Finset ℕ

The admissible thresholds for bald make a man bald with fewer than θ hairs, the borderline cases being those with 40 to 60 hairs (§5).

Equations

• Fine1975.baldness = Finset.Icc 40 60

@[reducible, inline]

abbrev Fine1975.bald (n θ : ℕ) : Prop

A man with n hairs is bald at threshold θ.

Equations

• Fine1975.bald n θ = (n < θ)

theorem Fine1975.yulBrynner_bald : SignType.supervaluation baldness (bald 0) = 1

Yul Brynner is bald.

theorem Fine1975.mickJagger_not_bald : SignType.supervaluation baldness (bald 100000) = -1

Mick Jagger is not.

theorem Fine1975.herbert_indet : SignType.supervaluation baldness (bald 50) = 0

Herbert, with fifty hairs, is a borderline case of a bald man.

theorem Fine1975.herbert_lem : (SignType.supervaluation baldness fun (θ : ℕ) => bald 50 θ ∨ ¬bald 50 θ) = 1

The law of excluded middle holds of Herbert though bivalence fails, Herbert is bald or not bald being true while neither disjunct is.

theorem Fine1975.bald_superConsequence {m n : ℕ} (h : m ≤ n) : SuperConsequence (bald n) (bald m)

By the internal penumbral connection, if Herbert is to be bald, so is the man with fewer hairs.

theorem Fine1975.tolerance_superFalse : (SignType.supervaluation baldness fun (θ : ℕ) => ∀ (n : ℕ), bald n θ → bald (n + 1) θ) = -1

The sorites' tolerance premise is false, since a hair-splitting number exists in every complete and admissible specification.

theorem Fine1975.sorites : SignType.supervaluation baldness (bald 0) = 1 ∧ (SignType.supervaluation baldness fun (θ : ℕ) => ∀ (n : ℕ), bald n θ → bald (n + 1) θ) = -1 ∧ SignType.supervaluation baldness (bald 1000000) = -1

In the sorites, the first premise is true, the tolerance premise false, and the conclusion false.

Higher-order vagueness (§5)

theorem Fine1975.metaAssert_not_stable : ¬∀ (a b : SignType), a.toFlat ≤ b.toFlat → (SignType.ofProp (a = 1)).toFlat ≤ (SignType.ofProp (b = 1)).toFlat

On the truth-value approach D is the assertion ofProp (a = 1), true of the true and false of the rest, and Stability fails, since DA is false for A indefinite but true for A true.

def Fine1975.definitely {Spec : Type u_1} (A : Spec → Prop) (S : Finset Spec) : Prop

Fine's D says that A holds at every admissible specification.

Equations

• Fine1975.definitely A S = ∀ s ∈ S, A s

theorem Fine1975.definitely_definitely_iff {Spec : Type u_1} (A : Spec → Prop) (S : Finset Spec) : definitely (fun (x : Spec) => definitely A S) S ↔ definitely A S

DA and DDA coincide (Axiom 4).

theorem Fine1975.not_definitely_definitely {Spec : Type u_1} (A : Spec → Prop) (S : Finset Spec) (h : ¬definitely A S) : definitely (fun (x : Spec) => ¬definitely A S) S

What is not definite is definitely not definite (Axiom 5).

@[instance_reducible]

instance Fine1975.instDecidableDefinitely {Spec : Type u_1} (A : Spec → Prop) (S : Finset Spec) [DecidablePred A] : Decidable (definitely A S)

Equations

• Fine1975.instDecidableDefinitely A S = { decide := decide (∀ a ∈ S.val.attach, (fun (s : Spec) (a : s ∈ S) => A s) ↑a ⋯), reflects_decide := ⋯ }

theorem Fine1975.definitely_imp_valid {Spec : Type u_1} (A : Spec → Prop) (S : Finset Spec) [DecidablePred A] : (SignType.supervaluation S fun (s : Spec) => ¬definitely A S ∨ A s) = 1

DA ⊃ A is valid (Axiom T).

theorem Fine1975.superTrue_definitely_of_superTrue {Spec : Type u_1} (A : Spec → Prop) (S : Finset Spec) [DecidablePred A] (h : SignType.supervaluation S A = 1) : (SignType.supervaluation S fun (x : Spec) => definitely A S) = 1

DA is a consequence of A, since to assert A is to assert DA.

theorem Fine1975.superTrue_imp_definitely_of_indet {Spec : Type u_1} (A : Spec → Prop) (S : Finset Spec) [DecidablePred A] (h : SignType.supervaluation S A = 0) : (SignType.supervaluation S fun (s : Spec) => ¬A s ∨ definitely A S) = 0

Yet A ⊃ DA is not valid, since where A is indefinite DA fails and A ⊃ DA inherits the indefiniteness of ¬A.

theorem Fine1975.herbert_not_imp_definitely : (SignType.supervaluation baldness fun (θ : ℕ) => ¬bald 50 θ ∨ definitely (bald 50) baldness) ≠ 1

So if Herbert is bald, he is definitely bald is not true, and the Deduction Theorem fails.

theorem Fine1975.superConsequence_iff_definitely_imp {Spec : Type u_1} (A : Spec → Prop) [DecidablePred A] {B : Spec → Prop} [DecidablePred B] : SuperConsequence A B ↔ ∀ (S : Finset Spec), (SignType.supervaluation S fun (s : Spec) => ¬definitely A S ∨ B s) = 1

B is a consequence of A iff DA ⊃ B is valid (§5), which relates consequence to validity once the Deduction Theorem fails.

theorem Fine1975.not_definitely_antitone : {60} ⊆ baldness ∧ ¬definitely (bald 50) baldness ∧ definitely (bald 50) {60}

External Stability fails for D, as definitely Herbert is bald is false over the admissible thresholds but true once the threshold is fixed at 60, a more precise space.

@[reducible, inline]

abbrev Fine1975.Space (Spec : Type u_1) : ℕ → Type u_1

A zero-order space is a complete specification, and an (n + 1)-order space is a set of n-order spaces.

Equations

• Fine1975.Space Spec 0 = Spec
• Fine1975.Space Spec n.succ = Set (Fine1975.Space Spec n)

structure Fine1975.Boundary (Spec : Type u_1) : Type u_1

An ω-order boundary is a sequence of spaces of every order, each a member of the next.

• s (n : ℕ) : Space Spec n
• mem (n : ℕ) : self.s n ∈ self.s (n + 1)

def Fine1975.Boundary.R {Spec : Type u_1} (b c : Boundary Spec) : Prop

A boundary c is admissible from b when each of its spaces is a member of the next space of b.

Equations

• b.R c = ∀ (i : ℕ), c.s i ∈ b.s (i + 1)

theorem Fine1975.Boundary.R_refl {Spec : Type u_1} (b : Boundary Spec) : b.R b

Accessibility is reflexive.

def Fine1975.Boundary.Definitely {Spec : Type u_1} (φ : Boundary Spec → Prop) (b : Boundary Spec) : Prop

D φ holds at a boundary when φ holds at every admissible boundary.

Equations

• Fine1975.Boundary.Definitely φ b = ∀ (c : Fine1975.Boundary Spec), b.R c → φ c

theorem Fine1975.Boundary.definitely_self {Spec : Type u_1} {φ : Boundary Spec → Prop} {b : Boundary Spec} (h : Definitely φ b) : φ b

What is definitely the case is the case (Axiom T).

theorem Fine1975.Boundary.R_not_trans : ¬∀ (b c d : Boundary Bool), b.R c → c.R d → b.R d

Accessibility is not transitive, so the logic of D is T and not S4. From the boundary that fixes true and {true}, the one fixing true and {true, false} is admissible, and from it the one fixing false and {true, false}, which is not admissible from the first.