「‍」 Lingenic

Bilattice Logic

(⤓.md ≡ ◇.md); γ ≜ [2026-10-22T165042.936, 2026-10-23T055632.935] ∧ |γ| = 3

Bilattice Logic

Origin. Matthew L. Ginsberg, "Multivalued logics: a uniform approach to reasoning in artificial intelligence" (Computational Intelligence 4, 1988; conference version AAAI 1986), introduced bilattices as a single truth-value framework for first-order deduction, default logic, prioritized defaults, and assumption-based truth maintenance. Melvin Fitting made them a logic: "Bilattices and the theory of truth" (Journal of Philosophical Logic 18, 1989), "Kleene's logic, generalized" (Journal of Logic and Computation 1, 1991), and "Bilattices and the semantics of logic programming" (Journal of Logic Programming 11, 1991) located Kleene's three-valued and Belnap's four-valued logics inside bilattices. His logic-programming semantics on the knowledge order extended his "A Kripke-Kleene semantics for general logic programs" (Journal of Logic Programming 2, 1985). Ofer Arieli and Arnon Avron, "Reasoning with logical bilattices" (Journal of Logic, Language and Information 5, 1996; preliminary version LICS 1994), defined logical bilattices and gave sound and complete proof systems for their consequence relation, developed further in "The value of the four values" (Artificial Intelligence 102, 1998).

Models. One set of truth values carrying two lattice orders: ≤_t ranks how true a value is, ≤_k how much information it records, and the separation of the two is the content — a value can rise in information while staying incomparable in truth, which is what reasoning from several sources needs and what a single order cannot say. The smallest non-trivial interlaced bilattice is FOUR, Belnap's four values, with ⊤ (told both) and ⊥ (told neither) between f and t in the truth order and at the two poles of the knowledge order; its ≤_t fragment is first-degree entailment, so bilattice logic is FDE seen as the four-element instance of a general algebra of truth and information. Negation belongs to the truth order and leaves the knowledge order alone: being told that ¬A is as much information as being told that A.

Formalism.

Bilattice: A set B with two bounded lattice orders. ∧, ∨: meet and join in ≤_t. ⊗, ⊕: meet and join in ≤_k. Bounds: f, t for ≤_t; ⊥, ⊤ for ≤_k. Negation ¬: an involution inverting ≤_t and preserving ≤_k. Conflation −, where present: an involution inverting ≤_k and preserving ≤_t.

FOUR: ≤_t: f <_t ⊥, ⊤ <_t t, with ⊥ and ⊤ incomparable. ≤_k: ⊥ <_k f, t <_k ⊤, with f and t incomparable. ⊤ is Belnap's B (told both), ⊥ his N (told neither); FDE's designated set {T, B} is {t, ⊤} here. ¬ swaps t and f, fixes ⊥ and ⊤. − swaps ⊥ and ⊤, fixes t and f. Conflation picks out Kleene: the elements with a ≤_k −a are f, ⊥, t, and on them the truth-order operations are Kleene's strong three-valued logic (Fitting, "Kleene's logic, generalized", 1991).

Interlacing and distributivity: Interlaced: each of ∧, ∨, ⊗, ⊕ is monotone with respect to both orders (Fitting's class). Distributive: every distributive law among the four operations holds (Ginsberg's class). Distributive implies interlaced; FOUR is distributive.

The product construction: L₁ ⊙ L₂: carrier L₁ × L₂. (x₁, y₁) ≤_t (x₂, y₂) iff x₁ ≤ x₂ and y₂ ≤ y₁. (x₁, y₁) ≤_k (x₂, y₂) iff x₁ ≤ x₂ and y₁ ≤ y₂. Reading: x is the evidence for, y the evidence against. When L₁ = L₂ = L, negation is (x, y) ↦ (y, x). FOUR = 2 ⊙ 2.

Representation: Ginsberg (1988): every bounded distributive bilattice with negation is isomorphic to a product L ⊙ L. Avron, "The structure of interlaced bilattices" (1996): every bounded interlaced bilattice is isomorphic to some L₁ ⊙ L₂, and interlacing is necessary as well as sufficient — so the class is a finitely axiomatized variety. Bou and Rivieccio, "The logic of distributive bilattices" (Logic Journal of the IGPL 19, 2011): the unbounded case.

Logical bilattices and consequence: A logical bilattice is a pair (B, F) with F a prime bifilter: a filter in both orders, prime with respect to ∧, ∨, ⊗, ⊕. Designated values = F. Γ ⊨ ψ iff every valuation designating all of Γ designates ψ. On FOUR the only prime bifilter is {t, ⊤}.

Implication: The ≤_t operations yield no detachable conditional, exactly as in FDE. Arieli–Avron's ⊃: a ⊃ b = b if a is designated, t otherwise. ⊃ restores modus ponens and the deduction theorem; ¬A ∨ B does neither.

Symbols.

SymbolUnicodeNameMeaning
∧U+2227Logical andMeet in the truth order
∨U+2228Logical orJoin in the truth order
⊗U+2297Circled times / ConsensusMeet in the knowledge order
⊕U+2295Circled plus / GullibilityJoin in the knowledge order
¬U+00ACNot signInvolution inverting ≤_t, fixing ≤_k
−U+2212Minus sign / ConflationInvolution inverting ≤_k, fixing ≤_t
⊤U+22A4Down tack / TopGreatest information: told both
⊥U+22A5Up tack / BottomLeast information: told neither
⊃U+2283Superset of / Weak implicationArieli–Avron's detachable conditional
⊙U+2299Circled dot operatorThe product bilattice construction
⊨U+22A8SatisfactionDesignation-preserving consequence
≤U+2264Less-than or equal toBase of both order signs
↦U+21A6Maps toNegation on a product, (x, y) ↦ (y, x)
≤_t—Truth orderf at the bottom, t at the top
≤_k—Knowledge order⊥ at the bottom, ⊤ at the top
t, f—True, falseThe bounds of the truth order
FOUR—Belnap's four-element bilatticeThe smallest non-trivial interlaced bilattice
F—Prime bifilterThe designated values of a logical bilattice
GBL—Gentzen system for logical bilatticesArieli–Avron's sound and complete sequent calculus

Metatheory. Arieli and Avron (1996) proved that consequence is four-valued no matter how large the bilattice: for every logical bilattice (B, F), the consequence relation coincides with that of (FOUR, {t, ⊤}), so the general semantics adds generality to the models and none to the logic. They gave the sequent calculus GBL and a Hilbert-style counterpart, sound and complete for this consequence, and with ⊃ added the deduction theorem holds; decidability is immediate from the four-element matrix. The structure theory is Avron's 1996 representation — bounded interlaced bilattices are exactly the products L₁ ⊙ L₂, generalizing Ginsberg's theorem for the distributive case, with the unbounded case by Bou and Rivieccio (2011). On the logic-programming side, Fitting (1991) showed that a program over any bilattice has a ≤_k-monotone immediate-consequence operator, so the Knaster–Tarski least fixpoint exists and generalizes the Kripke–Kleene semantics of his 1985 paper, with conflation carving the consistent valuations out of the bilattice. The truth-order fragment on FOUR is first-degree entailment, so the base logic inherits FDE's profile: paraconsistent and paracomplete, with no valid formulas and no unsatisfiable ones in the {∧, ∨, ¬} fragment; theorems enter only with ⊃ and the constants.

Applies to. Logic programming semantics, where Kripke–Kleene, stable, and well-founded constructions are fixpoints over bilattices. Databases and information integration that must store conflicting and missing values without collapse. Default reasoning and truth maintenance, Ginsberg's original targets. Inconsistency-tolerant inference from possibly contradictory knowledge bases, the Arieli–Avron application incorporating Kifer and Lozinskii's annotated framework. Theories of truth, through Fitting's bilattice reading of Kripke's construction.

Limitations. Bilattice negation is a De Morgan involution, so the consequence relation is nowhere negation-complete in the classical sense: A ∨ ¬A is not valid, A ∧ ¬A is not unsatisfiable, and these are commitments of the semantics — a reasoner that must discharge contradictions needs machinery from outside the bilattice. There is no implication in the pure bilattice language: ∧, ∨, ¬ give nothing detachable, and Arieli–Avron's ⊃ must be added, defined through designation rather than through either order. The knowledge-order operations are not free either — as the First-Degree Entailment entry records, ⊗ and ⊕ are not connectives of FDE, and adding them changes the logic. "Bilattice logic" is moreover a family and not a system: the choices of class (distributive, interlaced, logical), of language (with or without ⊗, ⊕, conflation, the four constants, ⊃), and of consequence (truth-order preservation against knowledge-order preservation) yield non-equivalent logics. Umberto Rivieccio's "An Algebraic Study of Bilattice-based Logics" (doctoral thesis, 2010) maps the family. Conflation exists only where the bilattice admits it and interacts with negation only under an added commutation assumption. And the values record what the reasoner has been told, not by whom or how often, so one contradictory source and two conflicting ones are indistinguishable, as in FDE.

© 2026 Lingenic LLC