The knowledge order on three-valued truth

The order of SignType is the truth order -1 < 0 < 1. The flat domain Flat Bool orders the same three values by information instead, with the undefined value 0 below both 1 and -1. Kleene's strong connectives are monotone for this knowledge order, which is Kleene's regularity condition, while the Weak Kleene connectives are not even monotone for the truth order. Flat Bool has a knowledge meet but only a partial knowledge join: the three values lack the glut of Belnap's four values, of which they are the consistent part.

Main definitions

• SignType.toFlat, SignType.equivFlatBool: 0 ↦ ⊥, 1 ↦ true, -1 ↦ false.

Main results

• SignType.truthOrder_ne_knowledgeOrder: the two orders differ.
• SignType.toFlat_neg_mono, SignType.toFlat_inf_mono_left, SignType.toFlat_sup_mono_left: the Strong Kleene connectives are knowledge-monotone.
• SignType.meetWeak_not_truthMono, SignType.joinWeak_not_truthMono: the Weak Kleene ones are not truth-monotone.
• SignType.toFlat_supervaluation: over a nonempty family, the supervaluation is the knowledge meet of the classical values, so shrinking the family can only add information (SignType.toFlat_supervaluation_mono).

References

• [Kle52]

def SignType.toFlat : SignType → Flat Bool

The value in the flat domain sends 0 to ⊥, and 1 and -1 to true and false.

Equations

• SignType.zero.toFlat = none
• SignType.pos.toFlat = some true
• SignType.neg.toFlat = some false

def SignType.ofFlat : Flat Bool → SignType

The inverse of toFlat.

Equations

• SignType.ofFlat none = 0
• SignType.ofFlat (some true) = 1
• SignType.ofFlat (some false) = -1

def SignType.equivFlatBool : SignType ≃ Flat Bool

SignType and the flat domain Flat Bool are the same three values.

Equations

• SignType.equivFlatBool = { toFun := SignType.toFlat, invFun := SignType.ofFlat, left_inv := ⋯, right_inv := ⋯ }

theorem SignType.truthOrder_ne_knowledgeOrder : -1 ≤ 0 ∧ ¬(-1).toFlat ≤ toFlat 0

The truth order and the knowledge order differ, since -1 ≤ 0 in the truth order but the defined value -1 is not below the undefined 0 = ⊥ in the knowledge order.

theorem SignType.toFlat_neg_mono {a b : SignType} (h : a.toFlat ≤ b.toFlat) : (-a).toFlat ≤ (-b).toFlat

Strong Kleene negation is regular; being unary, it is the unique monotone extension of Boolean not.

theorem SignType.toFlat_inf_mono_left {a a' : SignType} (b : SignType) (h : a.toFlat ≤ a'.toFlat) : (min a b).toFlat ≤ (min a' b).toFlat

Strong Kleene conjunction is regular in each argument.

theorem SignType.toFlat_sup_mono_left {a a' : SignType} (b : SignType) (h : a.toFlat ≤ a'.toFlat) : (max a b).toFlat ≤ (max a' b).toFlat

Strong Kleene disjunction is regular in each argument.

theorem SignType.meetWeak_not_truthMono : ¬∀ (a a' b : SignType), a ≤ a' → a.meetWeak b ≤ a'.meetWeak b

Weak Kleene conjunction is not truth-monotone, since 0 ≤ 1 but meetWeak 0 (-1) = 0 is not below meetWeak 1 (-1) = -1; unlike ⊓ it is no bilattice operation.

theorem SignType.joinWeak_not_truthMono : ¬∀ (a a' b : SignType), a ≤ a' → a.joinWeak b ≤ a'.joinWeak b

Weak Kleene disjunction is not truth-monotone either.

theorem SignType.toFlat_supervaluation {α : Type u_1} {s : Finset α} (P : α → Prop) [DecidablePred P] (hs : s.Nonempty) : (supervaluation s P).toFlat = s.inf' hs fun (a : α) => ↑(decide (P a))

Over a nonempty family, the supervaluation is the knowledge meet of the classical values.

theorem SignType.toFlat_supervaluation_mono {α : Type u_1} {s t : Finset α} (P : α → Prop) [DecidablePred P] (h : s ⊆ t) (hs : s.Nonempty) : (supervaluation t P).toFlat ≤ (supervaluation s P).toFlat

Shrinking a family to a nonempty subfamily can only add information. Nonemptiness is needed, since the empty family's 1 is a convention rather than a meet and a family whose members all fail P has the incomparable value -1.