Three-valued truth as sets of classical values

import Linglib.Logic.Trivalent.Powerset · namespace SignType

A three-valued truth value can be read as the set of classical values it leaves open: 1 is {true}, -1 is {false} and the undefined 0 is {true, false}. These are the values of its two bivalent readings, its designation at K3 and at LP, so the set of a value is the supervaluation reading of Linglib.Logic.Trivalent.Supervaluation at a single occurrence.

Lifting a Boolean operation pointwise to these sets computes every classical result compatible with its inputs, and for negation, conjunction, disjunction and the biconditional the lift is Kleene's strong table; Trivalent.Formula.eval_strongKleene_eq_supervaluation extends this to whole formulas. The Weak Kleene connectives are the lift of no Boolean operation. The knowledge order of Linglib.Logic.Trivalent.Flat is reverse inclusion, so a lifted operation is monotone for it, which is Kleene's regularity (Kleene 1952).

Main definitions

SignType.toFinset, SignType.ofFinset, SignType.equivNonemptyFinsetBool: a value as the nonempty set of classical values it leaves open.

Main results

SignType.toFinset_eq_image_threshold_le: the set of a value is the set of its designations at the two standards.
SignType.toFinset_supervaluation: over a nonempty family, the supervaluation is the set of classical values (van Fraassen 1966).
SignType.toFinset_neg, SignType.toFinset_inf, SignType.toFinset_sup, SignType.toFinset_mul: the Strong Kleene connectives are the pointwise lifts of !, &&, || and ==.
SignType.meetWeak_not_lift, SignType.joinWeak_not_lift: the Weak Kleene connectives are the lift of no Boolean operation.
SignType.toFlat_le_toFlat_iff_toFinset_subset: the knowledge order is reverse inclusion.

References

Kleene 1952, Introduction to Metamathematics
van Fraassen 1966, Singular Terms, Truth-Value Gaps, and Free Logic

Values as sets of classical values

The classical values a value leaves open: {true}, {false}, or both when undefined.

def toFinset L57–61

SignType → Finset Bool

pos.toFinset = {true}
neg.toFinset = {false}
zero.toFinset = {true, false}

Used by toFinset_one, toFinset_neg_one, toFinset_zero, toFinset_nonempty, toFinset_injective, toFinset_inj, ofFinset_toFinset, toFinset_ofFinset, toFinset_eq_image_threshold_le, toFinset_supervaluation, toFinset_neg, toFinset_inf, toFinset_sup, toFinset_mul, meetWeak_not_lift, joinWeak_not_lift, toFlat_le_toFlat_iff_toFinset_subset

Used in Logic/Trivalent/Deployment

The value leaving open the classical values of a set, sending the empty set, which no value leaves open, to 0.

def ofFinset L78–81

(s : Finset Bool) :

SignType

ofFinset s = if s = {true} then 1 else if s = {false} then -1 else 0

Used by ofFinset_toFinset, toFinset_ofFinset

L83–84

L86–87

The values are the nonempty sets of classical values.

def equivNonemptyFinsetBool L89–94

SignType ≃ { s : Finset Bool // s.Nonempty }

The definition is too large to print here; read it in the source.

The set of a value is the set of its two bivalent readings, its designations at K3 and LP.

theorem toFinset_eq_image_threshold_le L96–99

(a : SignType) :

a.toFinset = Finset.image (fun (d : Trivalent.Designation) => decide (d.threshold ≤ a)) Finset.univ

Built from

Over a nonempty family, the supervaluation of P leaves open exactly the classical values P takes on the family.

theorem toFinset_supervaluation L101–116

{α : Type u_1} {s : Finset α} (P : α → Prop) [DecidablePred P] (hs : s.Nonempty) :

(supervaluation s P).toFinset = Finset.image (fun (a : α) => decide (P a)) s

Built from

Connectives as pointwise lifts

Strong Kleene negation is the lift of !.

@[simp] theorem toFinset_neg L120–122

(a : SignType) :

(-a).toFinset = Finset.image (fun (x : Bool) => !x) a.toFinset

Built from

Strong Kleene conjunction is the lift of &&.

@[simp] theorem toFinset_inf L124–127

(a b : SignType) :

(min a b).toFinset = Finset.image₂ (fun (x1 x2 : Bool) => x1 && x2) a.toFinset b.toFinset

Built from

Strong Kleene disjunction is the lift of ||.

@[simp] theorem toFinset_sup L129–132

(a b : SignType) :

(max a b).toFinset = Finset.image₂ (fun (x1 x2 : Bool) => x1 || x2) a.toFinset b.toFinset

Built from

The Strong Kleene biconditional, multiplication, is the lift of ==.

@[simp] theorem toFinset_mul L134–137

(a b : SignType) :

(a * b).toFinset = Finset.image₂ (fun (x1 x2 : Bool) => x1 == x2) a.toFinset b.toFinset

Built from

Weak Kleene conjunction is the lift of no Boolean operation, since an undefined operand makes it undefined even where the lift is settled.

theorem meetWeak_not_lift L139–143

¬∃ (f : Bool → Bool → Bool), ∀ (a b : SignType), (a.meetWeak b).toFinset = Finset.image₂ f a.toFinset b.toFinset

Built from

Weak Kleene disjunction is the lift of no Boolean operation.

theorem joinWeak_not_lift L145–148

¬∃ (f : Bool → Bool → Bool), ∀ (a b : SignType), (a.joinWeak b).toFinset = Finset.image₂ f a.toFinset b.toFinset

Built from

The knowledge order

The knowledge order is reverse inclusion: a value is more informative when it leaves fewer classical values open.

theorem toFlat_le_toFlat_iff_toFinset_subset L152–156

{a b : SignType} :

a.toFlat ≤ b.toFlat ↔ b.toFinset ⊆ a.toFinset

Built from