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 Belnap'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.Logic.Bilattice. Here we prove the slicing for linglib's Truth3 (Kleene's three-valued logic, [Kle52]): ofTruth3 embeds Truth3 onto the consistent fragment of FOUR, matching the truth order (Truth3's ≤), the knowledge order (Truth3.toFlat, i.e. Flat Bool), 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.ofTruth3 — the embedding Truth3 → FOUR
• Fitting1994.ofTruth3_consistent, consistent_range — its image is exactly the consistent fragment
• tLE_ofTruth3, kLE_ofTruth3, neg_ofTruth3 — Truth3 is the consistent fragment of FOUR as a bilattice (both orders + negation)

def Fitting1994.ofTruth3 : Core.Duality.Truth3 → Bilattice.FOUR

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

Equations

• Fitting1994.ofTruth3 Core.Duality.Truth3.indet = Bilattice.FOUR.U
• Fitting1994.ofTruth3 Core.Duality.Truth3.true = Bilattice.FOUR.T
• Fitting1994.ofTruth3 Core.Duality.Truth3.false = Bilattice.FOUR.F

theorem Fitting1994.ofTruth3_injective : Function.Injective ofTruth3

theorem Fitting1994.ofTruth3_consistent (a : Core.Duality.Truth3) : (ofTruth3 a).Consistent

theorem Fitting1994.consistent_range {x : Bilattice.FOUR} (hx : x.Consistent) : ∃ (a : Core.Duality.Truth3), ofTruth3 a = x

The image of ofTruth3 is the whole consistent fragment.

theorem Fitting1994.tLE_ofTruth3 (a b : Core.Duality.Truth3) : a ≤ b ↔ Bilattice.Evidential.tLE (ofTruth3 a) (ofTruth3 b)

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

theorem Fitting1994.kLE_ofTruth3 (a b : Core.Duality.Truth3) : a.toFlat ≤ b.toFlat ↔ Bilattice.Evidential.kLE (ofTruth3 a) (ofTruth3 b)

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

theorem Fitting1994.neg_ofTruth3 (a : Core.Duality.Truth3) : ofTruth3 a.neg = Bilattice.Evidential.neg (ofTruth3 a)

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