Belnap's four values

Belnap's four values are the diagonal product Bool ⊙ Bool: a value records whether a proposition has been told true and whether it has been told false. Arieli and Avron develop their logic as a bilattice, and FOUR is the literature's name for it. The consistent values, those without a glut, are Kleene's three: SignType.orderIsoConsistent identifies SignType with them, carrying Strong Kleene negation, conjunction and disjunction to FOUR's negation and truth meet and join, and the knowledge order of SignType.toFlat to FOUR's.

Main definitions

• Bilattice.FOUR: Bool ⊙ Bool, with the values U (neither), T, F and I (both).
• SignType.toFour: Kleene's values inside FOUR.

Main results

• Bilattice.FOUR.isConsistent_iff, Bilattice.FOUR.isExact_iff: the consistent values are those other than I, and the exact values are F and T.
• SignType.orderIsoConsistent: SignType is the consistent part of FOUR.
• SignType.toFour_neg, SignType.toFour_inf, SignType.toFour_sup, SignType.toFour_kLE_toFour: the identification respects the connectives and both orders.

References

• [Bel77]
• [AA96]
• [Fit94]

@[reducible, inline]

abbrev Bilattice.FOUR : Type

Belnap's four-valued bilattice FOUR = Bool ⊙ Bool records whether a proposition has been told true and whether it has been told false ([Bel77]).

Equations

• Bilattice.FOUR = Bilattice.Product Bool Bool

def Bilattice.FOUR.U : FOUR

The gap ⊥, told neither true nor false.

Equations

• Bilattice.FOUR.U = Bilattice.Product.mk false false

def Bilattice.FOUR.T : FOUR

true.

Equations

• Bilattice.FOUR.T = Bilattice.Product.mk true false

def Bilattice.FOUR.F : FOUR

false.

Equations

• Bilattice.FOUR.F = Bilattice.Product.mk false true

def Bilattice.FOUR.I : FOUR

The glut ⊤, told both true and false.

Equations

• Bilattice.FOUR.I = Bilattice.Product.mk true true

@[simp]

theorem Bilattice.FOUR.isConsistent_iff (x : FOUR) : IsConsistent x ↔ x ≠ I

The consistent values of FOUR are those other than the glut I.

@[simp]

theorem Bilattice.FOUR.isExact_iff (x : FOUR) : IsExact x ↔ x = F ∨ x = T

The exact values of FOUR are the classical values F and T ([Fit94]).

def SignType.toFour : SignType → Bilattice.FOUR

Kleene's three values inside FOUR, sending 0, 1 and -1 to U, T and F.

Equations

• SignType.zero.toFour = Bilattice.FOUR.U
• SignType.pos.toFour = Bilattice.FOUR.T
• SignType.neg.toFour = Bilattice.FOUR.F

theorem SignType.toFour_injective : Function.Injective toFour

@[simp]

theorem SignType.toFour_le_toFour {a b : SignType} : a.toFour ≤ b.toFour ↔ a ≤ b

theorem SignType.range_toFour : Set.range toFour = {x : Bilattice.FOUR | Bilattice.IsConsistent x}

Kleene's values are exactly the consistent values of FOUR ([Fit94] §3).

def SignType.orderIsoConsistent : SignType ≃o ↑{x : Bilattice.FOUR | Bilattice.IsConsistent x}

SignType is the consistent part of FOUR ([Fit94] §3).

Equations

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

theorem SignType.isExact_toFour (a : SignType) : Bilattice.IsExact a.toFour ↔ a ≠ 0

The exact values among Kleene's are the defined ones ([Fit94] §3).

theorem SignType.toFour_kLE_toFour {a b : SignType} : Bilattice.kLE a.toFour b.toFour ↔ a.toFlat ≤ b.toFlat

The knowledge order of SignType is FOUR's on Kleene's values.

@[simp]

theorem SignType.toFour_neg (a : SignType) : (-a).toFour = a.toFourᶜ

Strong Kleene negation is FOUR's negation on Kleene's values.

@[simp]

theorem SignType.toFour_inf (a b : SignType) : (min a b).toFour = a.toFour ⊓ b.toFour

Strong Kleene conjunction is FOUR's truth meet on Kleene's values ([Fit94] §3).

@[simp]

theorem SignType.toFour_sup (a b : SignType) : (max a b).toFour = a.toFour ⊔ b.toFour

Strong Kleene disjunction is FOUR's truth join on Kleene's values ([Fit94] §3).