Documentation

Linglib.Core.Order.Bilattice.Kleene

The knowledge order: Flat Bool and the Kleene bilattice #

Trivalent's native order is the truth order false < indet < true; Flat Bool (equivFlatBool) carries the knowledge order ⊥ ⊑ true, ⊥ ⊑ false. Two orders on one carrier is a bilattice. Strong Kleene ∧/∨ are the truth-order lattice operations ⊓/⊔; what makes them canonical is interlacing — they are monotone for the knowledge order as well ([Kle52]'s regularity condition), while Weak Kleene is not (meetWeak_not_truthMono).

Flat Bool's SemilatticeInf meet ⊓ is the consensus ⊗; its partial join (PartialUnify) is the gullibility ⊕, partial because three values lack the ⊤ ("both") of a full four-valued bilattice — so Trivalent is the consistent fragment of that bilattice.

source
def Trivalent.toFlat :
Trivalent → Flat Bool

The carrier bijection Trivalent ≃ Flat Bool: indet ↔ ⊥, true ↔ some true, false ↔ some false. Flat Bool carries the knowledge order, distinct from the truth order — the two orders of the Kleene bilattice.

Equations
Instances For
    source
    def Trivalent.ofFlat :
    Flat Bool → Trivalent

    Inverse of toFlat.

    Equations
    Instances For
      source
      def Trivalent.equivFlatBool :
      Trivalent ≃ Flat Bool

      Trivalent and the flat domain Flat Bool share a carrier.

      Equations
      Instances For
        source
        theorem Trivalent.truthOrder_ne_knowledgeOrder :
        false ≤ indet ∧ ¬false.toFlat ≤ indet.toFlat

        The truth order and the knowledge order genuinely differ: in the truth order false ≤ indet, but in the knowledge order the committed value false is not below the uncommitted indet = ⊥.

        source
        theorem Trivalent.toFlat_neg_mono {a b : Trivalent} (h : a.toFlat ≤ b.toFlat) :
        a.neg.toFlat ≤ b.neg.toFlat

        Strong Kleene negation is regular (knowledge-monotone); being unary, it is in fact the unique monotone extension of Boolean not.

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

        Strong Kleene conjunction is regular (knowledge-monotone in each argument).

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

        Strong Kleene disjunction is regular (knowledge-monotone in each argument).

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

        Weak Kleene conjunction is not interlaced — it fails truth-order monotonicity (indet ≤ true, yet meetWeak .indet .false = .indet ≰ .false), so unlike Strong Kleene ⊓ it is not a bilattice operation.

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

        Weak Kleene disjunction is likewise not interlaced.