Kleene's three-valued logic as the consistent fragment of Belnap's FOUR

[Fit94]

[Fit94] ("Kleene's Three Valued Logics and Their Children") organizes Kleene's logics as fragments of [Bel77]'s four-valued bilattice FOUR, sliced by the conflation − (the knowledge-order involution): the strong Kleene values are exactly those x with x ≤_k −x — the consistent (non-glut) values.

FOUR and its two orders / negation / conflation are the shared substrate in Core.Order.Bilattice. Here we prove the slicing for linglib's Trivalent (Kleene's three-valued logic, [Kle52]): ofTruth embeds Trivalent onto the consistent fragment of FOUR, matching the truth order (Trivalent's ≤ vs FOUR's ≤), the knowledge order (Trivalent.toFlat, i.e. Flat Bool, vs FOUR's ≤ₖ), and negation. So the gap logic linglib uses for presupposition is the I-free slice; the glut I is what trivalence excludes. The bilattice route to natural-language entailment, implicature, and presupposition is [Sch96a] (see Studies.Schoter1996).

Main results

• Fitting1994.ofTruth — the embedding Trivalent → FOUR
• Fitting1994.ofTruth_consistent, consistent_range — its image is exactly the consistent fragment
• le_ofTruth, kLE_ofTruth, neg_ofTruth, inf_ofTruth/sup_ofTruth — Trivalent is the consistent fragment of FOUR as a bilattice logic: both orders, negation, and the strong-Kleene connectives ∧/∨ as restrictions of FOUR's truth meet/join

def Fitting1994.ofTruth : Trivalent → Bilattice.FOUR

The embedding of Trivalent (Kleene-3) into FOUR: indet ↦ ⊥, true ↦ T, false ↦ F. Its image is exactly the consistent fragment.

Equations

• Fitting1994.ofTruth Trivalent.indet = Bilattice.FOUR.U
• Fitting1994.ofTruth Trivalent.true = Bilattice.FOUR.T
• Fitting1994.ofTruth Trivalent.false = Bilattice.FOUR.F

theorem Fitting1994.ofTruth_injective : Function.Injective ofTruth

theorem Fitting1994.ofTruth_consistent (a : Trivalent) : (ofTruth a).Consistent

theorem Fitting1994.consistent_range {x : Bilattice.FOUR} (hx : x.Consistent) : ∃ (a : Trivalent), ofTruth a = x

The image of ofTruth is the whole consistent fragment.

theorem Fitting1994.le_ofTruth (a b : Trivalent) : a ≤ b ↔ ofTruth a ≤ ofTruth b

Trivalent-order match: Trivalent's truth order is FOUR's, on the fragment.

theorem Fitting1994.kLE_ofTruth (a b : Trivalent) : a.toFlat ≤ b.toFlat ↔ Bilattice.kLE (ofTruth a) (ofTruth b)

Knowledge-order match: Trivalent's knowledge order (Trivalent.toFlat, i.e. Flat Bool) is FOUR's knowledge order on the fragment.

theorem Fitting1994.neg_ofTruth (a : Trivalent) : ofTruth a.neg = Bilattice.Product.neg (ofTruth a)

Negation match: Kleene negation is FOUR-negation on the fragment.

theorem Fitting1994.inf_ofTruth (a b : Trivalent) : ofTruth (min a b) = ofTruth a ⊓ ofTruth b

Connective match, conjunction: strong-Kleene ∧ (Trivalent's ⊓ = min) is the restriction of FOUR's truth meet to the consistent fragment — the fragment is a fragment as a logic, not just as a pair of posets ([Fit94]).

theorem Fitting1994.sup_ofTruth (a b : Trivalent) : ofTruth (max a b) = ofTruth a ⊔ ofTruth b

Connective match, disjunction: strong-Kleene ∨ (Trivalent's ⊔ = max) is the restriction of FOUR's truth join to the consistent fragment.