The Adjoint Structure of Predication on Bilattice-Valued Fibers

The Adjoint Structure of Predication on Bilattice-Valued Fibers

Predication has an adjoint structure: combining a subject with a predicate (extending) has a right partner that tests and restricts. On the four-valued bilattice $\mathbf{2}\otimes\mathbf{2}$ this pair is the twist-product fusion $\odot$ and residual $\Rightarrow$, which satisfy $a\odot p\leq_t q \iff p\leq_t(a\Rightarrow q)$. The pair lifts to every predicate over a system of subject-predicate-object triples, yielding a bilattice-valued hyperdoctrine, a decidable modal calculus and a reading as multiplicative linear logic.

This is a 561 Group research paper. Its status is draft: the finite algebraic facts below are verified by exhaustive enumeration of a four-element algebra, the functoriality argument is a proof sketch, and the decidability and linear-logic statements depend on cited theorems by other authors.

What does it mean to say predication is a residuation?

Frege (Frege 1879)¹¹ Gottlob Frege. Begriffsschrift. Louis Nebert, 1879. treated a predicate as an unsaturated function: it takes a subject and returns a value. In a subject-predicate-object triple $\langle S,P,O\rangle$, the predicate $P$ combines $S$ and $O$ into an assertion.

Lambek (Lambek 1958)²² Joachim Lambek. "The mathematics of sentence structure." American Mathematical Monthly 65, no. 3 (1958): 154-170. formalized how such combination behaves. A product $\cdot$ on expressions admits exactly two residuals:

$$a\cdot b\leq c\iff b\leq a\backslash c\iff a\leq c/b.$$

The left residual $a\backslash c$ asks what must combine with $a$ on the right to land below $c$; the right residual $c/b$ asks the mirror question. The product has two argument positions, so there are exactly two residuals. Galatos, Jipsen, Kowalski and Ono (Galatos et al. 2007)³³ Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono. Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Elsevier, 2007. show that residuated lattices are the algebraic home of this calculus. In the commutative case the two residuals coincide into one implication $\Rightarrow$, but the adjunction keeps two sides: a combining, generating, extending side and a testing, constraining, restricting side.

Lawvere (Lawvere 1969)⁴⁴ F. William Lawvere. "Adjointness in foundations." Dialectica 23, no. 3-4 (1969): 281-296. found a related pattern in categorical logic: on a hyperdoctrine, $\exists_f\dashv f^\dashv\forall_f$, where $f^$ is substitution along a morphism $f$, $\exists$ extends a predicate to a larger context and $\forall$ restricts it to where it holds universally. The two adjunctions are not literally the same theorem. Lambek's is a pair of residuals for a (possibly non-commutative) monoidal product on a poset, and Lawvere's is a chain of adjoints to base change along a morphism. What they share is a pattern in which the generative side is left adjoint to a restriction side. The paper's contribution is to instantiate that pattern concretely on four-valued evidence.

What is the four-valued bilattice as a twist product?

Belnap (Belnap 1977)⁵⁵ Nuel D. Belnap. "A useful four-valued logic." In Modern Uses of Multiple-Valued Logic, ed. J. Michael Dunn and George Epstein, 5-37, D. Reidel, 1977. defined four epistemic states for a system receiving information from several sources: $\bot$ (no information), $t$ (told true), $f$ (told false), $\top$ (told both). Kalman (Kalman 1958)⁶⁶ J. A. Kalman. "Lattices with involution." Transactions of the American Mathematical Society 87, no. 2 (1958): 485-491. introduced the twist-product construction for bounded distributive lattices, and Fitting (Fitting 1991)⁷⁷ Melvin Fitting. "Bilattices and the semantics of logic programming." Journal of Logic Programming 11, no. 1-2 (1991): 91-116. extended it to bilattices. In this representation each value is a pair $(a,b)\in\{0,1\}^2$ with a positive and a negative coordinate:

The truth order $\leq_t$ puts $f$ at the bottom and $t$ at the top; the knowledge order $\leq_k$ puts $\bot$ at the bottom and $\top$ at the top. The draft, citing Fitting, identifies this four-element algebra with the free bounded distributive bilattice on one generator (Fitting 2002)⁸⁸ Melvin Fitting. "Bilattices are nice things." In Self-Reference, CSLI Publications, 2002.. For an introduction to the two orders, see What is a bilattice?.

What is the residuated pair?

Theorem 1 (Busaniche and Cignoli (Busaniche & Cignoli 2014)⁹⁹ Manuela Busaniche and Roberto Cignoli. "The subvariety of commutative residuated lattices represented by twist-products." Algebra Universalis 71 (2014): 5-22.; Chajda and Langer (Chajda & Langer 2021)¹⁰¹⁰ Ivan Chajda and Helmut Langer. "Adjoint operations in twist-products of lattices." Symmetry 13, no. 2 (2021).). On the twist product $L\otimes L$ of any integral commutative residuated lattice $L$ with product $\cdot$ and residual $\to$, the operations

$$(x,y)\odot(z,v)=\bigl(x\cdot z,\ (x\to v)\wedge(z\to y)\bigr),$$

$$(x,y)\Rightarrow(z,v)=\bigl((x\to z)\wedge(v\to y),\ x\cdot v\bigr)$$

form a residuated pair with respect to the truth order:

$$a\odot p\leq_t q\iff p\leq_t(a\Rightarrow q).$$

The product $\odot$ is extending: it fuses positive evidence and cross-references each side's positive evidence against the other's negative evidence. The implication $\Rightarrow$ is restricting: it tests implication in both truth directions and combines negative evidence.

On $L=\mathbf{2}$ the operations can be tabulated. The following tables were regenerated from the formulas above (row operand first):

The adjunction was checked on all 64 triples $(a,p,q)\in\{\bot,t,f,\top\}^3$, with zero violations.

What algebraic properties hold?

The following are finite facts, verifiable by inspection of the tables above.

1. $\top$ is the identity for $\odot$: $\top\odot a=a$.
2. $f$ is absorbing for $\odot$: $f\odot a=f$.
3. $t$, $f$, $\top$ are idempotent under $\odot$; $\bot$ is not, since $\bot\odot\bot=f$.
4. $a\Rightarrow a=t$ for $a\in\{\bot,t,f\}$, and $\top\Rightarrow\top=\top$.
5. Nelson identity. For all $x,y$ in the algebra, with $\sim$ swapping the two coordinates and $\wedge_k$ the knowledge-order meet, $$\bigl(x\Rightarrow(x\Rightarrow y)\bigr)\wedge_k\bigl(\sim y\Rightarrow(\sim y\Rightarrow\sim x)\bigr)=x\Rightarrow y.$$
6. Contrapositive fails. In general $\sim(a\odot b)\neq\ \sim b\Rightarrow\ \sim a$, and neither $\odot$ nor $\Rightarrow$ commutes with negation or with conflation (the operation swapping the roles of the two orders). For example, $\sim(t\odot t)=f$ but $\sim t\Rightarrow\sim t=f\Rightarrow f=t$.

Chajda and Langer also give a second adjoint pair on twist products, the Nelson implication $x\Rightarrow_N y=(x\supset y)\wedge(\sim y\supset\sim x)$. Property 5 says that negation-aware iterated implication is sound even though naive contrapositive is not. The identity is treated in The Nelson identity on four-valued truth.

How do the operations lift to predicate fibers?

Let $\mathcal{S}$ be a system of subject-predicate-object triples, each carrying a value in $\{\bot,t,f,\top\}$. For a predicate $p$ occurring in $\mathcal{S}$, its fiber collects all triples using $p$:

$$\mathrm{Fib}(p)=\{\langle s,o,v\rangle:\langle s,p,o\rangle\in\mathcal{S}\text{ with value }v\}.$$

Pointwise bilattice operations on functions from $\mathrm{Fib}(p)$ to the four values define a fiber algebra $A_p$. Since pointwise products of distributive bilattices are distributive (Fitting 2002)¹¹¹¹ Melvin Fitting. "Bilattices are nice things." In Self-Reference, CSLI Publications, 2002., each $A_p$ is a distributive bilattice.

Let $\mathcal{C}$ be the category whose objects are the predicates of $\mathcal{S}$, and whose morphisms are generated by three kinds of predicate relationship: specialization (one predicate restricts to another), inversion (one predicate is the converse-and-negation of another) and composition (one predicate is the pointwise conjunction of two others).

Theorem 2 (fiber functor; proof sketch). The assignment $p\mapsto A_p$ extends to a contravariant functor $\mathcal{F}:\mathcal{C}^{\mathrm{op}}\to\mathbf{BiLat}$ into bilattices and bilattice homomorphisms.

Sketch. Each generating morphism class must map to a bilattice homomorphism. Specialization induces restriction of valuations, which preserves pointwise operations. Inversion applies negation pointwise, a bilattice homomorphism (Fitting 1991)¹²¹² Melvin Fitting. "Bilattices and the semantics of logic programming." Journal of Logic Programming 11, no. 1-2 (1991): 91-116.. Composition applies the knowledge meet pointwise, which preserves bilattice structure because fibers are distributive. Identities map to identities; composites of specializations induce composed restrictions; two inversions compose to the identity. $\square$

This makes $\mathcal{S}$ a bilattice-valued hyperdoctrine in the sense of Lawvere (Lawvere 1970)¹³¹³ F. William Lawvere. "Equality in hyperdoctrines and comprehension schema as an adjoint functor." In Applications of Categorical Algebra, Proceedings of Symposia in Pure Mathematics, 1-14, American Mathematical Society, 1970., and instantiates Maruyama's fibred algebraic semantics (Maruyama 2021)¹⁴¹⁴ Yoshihiro Maruyama. "Fibred algebraic semantics for a variety of non-classical first-order logics and topological logical translation." Journal of Symbolic Logic 86, no. 3 (2021): 1189-1213. for the specific case $\mathbf{2}\otimes\mathbf{2}$ over predicate-structured data.

Corollary 1. The adjunction $\odot\dashv\Rightarrow$ lifts to fibers: for each predicate, extending and restricting on $A_p$ are adjoint fiberwise.

What follows from the structure?

Decidability

Rivieccio, Jung and Jansana (Rivieccio et al. 2017)¹⁵¹⁵ Umberto Rivieccio, Achim Jung, and Ramon Jansana. "Four-valued modal logic: Kripke semantics and duality." Journal of Logic and Computation 27, no. 1 (2017): 155-199. proved that modal operators on the four-valued bilattice decompose into pairs of classical modal operators on the twist components, $\Box(a^+,a^-)=(\Box_1(a^+),\Diamond_2(a^-))$, and that the resulting four-valued modal logic has the finite model property and is decidable. Because fiber algebras are distributive bilattices over $\mathbf{2}\otimes\mathbf{2}$, the modal calculus arising from the fiber functor is decidable (Corollary 2, a consequence of the cited theorem).

A linear-logic reading

Jakl (Jakl 2025)¹⁶¹⁶ Tomáš Jakl. Four imprints of Belnap's useful four-valued logic in computer science. arXiv, 2025. shows that the Chu construction $\mathrm{Chu}(H,0)$ over a Heyting algebra $H$ is the twist construction. Under that identification the tensor of linear logic corresponds to the fusion $\odot$ and linear implication $\multimap$ to $\Rightarrow$. Specializing to $H=\mathbf{2}$ gives $\mathbf{2}\otimes\mathbf{2}\cong\mathrm{Chu}(\mathbf{2},0)$ as residuated structures.

Corollary 3. The extend/restrict adjunction on predicate fibers is the $\otimes\dashv\multimap$ adjunction of linear logic at the algebraic level. Every bilattice-valued triple system is then a model of a fragment of linear logic in which the tracked resources are epistemic states.

The draft names the resulting object a predication modal geometry (a predicate-indexed Chu space over $(\mathbf{2},0)$, with the fiber functor factoring through the Chu category). It also states that every bilattice-valued triple system is one, by the same argument. That naming theorem depends on the cited identification above and on the sketch of Theorem 2, and should be read at that level of rigor.

Behaviour after closure

Under closure (iterating inference rules to a fixed point, in the sense of Fitting (Fitting 1991)¹⁷¹⁷ Melvin Fitting. "Bilattices and the semantics of logic programming." Journal of Logic Programming 11, no. 1-2 (1991): 91-116.), $\bot$-valued assertions within scope are pushed upward in the knowledge order, so the effective algebra is $\{t,f,\top\}$.

Theorem 3. The set $\{t,f,\top\}$ is closed under both $\odot$ and $\Rightarrow$, contains the identity $\top$, and satisfies the adjunction with zero violations (exhaustive check on 27 triples).

So the extend/restrict structure persists after closure. For how closure behaves as a process, see Paraconsistent settling and comprehension.

Dynamics of iteration

By exhaustive computation on the four-element algebra: all orbits under iterated left-$\odot$ or left-$\Rightarrow$ reach fixed points in at most two steps (Proposition 8). The only oscillation is period 2: alternating $\odot$-by-$\bot$ and $\Rightarrow$-by-$\bot$ gives $\bot\to f\to\bot\to f\to\cdots$ (Proposition 9). All other alternating dynamics converge.

Geometry

The Priestley dual of $\mathbf{2}\otimes\mathbf{2}$ as a distributive bilattice is a discrete two-point space with a swap involution encoding negation (Jung & Rivieccio 2012)¹⁸¹⁸ Achim Jung and Umberto Rivieccio. "Priestley duality for bilattices." Studia Logica 100, no. 1-2 (2012): 223-252., and in general the duals of bilattices are pairs of Priestley spaces linked by continuous order-preserving maps. The modal calculus of predication lives in these paired spaces.

Why does it matter?

For a system that stores assertions with four-valued evidence, extend and restrict are the two ways to move between predicates: one builds, one checks. That they are adjoint means that checking a condition and building toward a goal are two descriptions of the same constraint, and that the usual machinery of weakest preconditions and refinement carries over to evidence that may be missing or conflicting. The cited linear-logic correspondence gives a resource-sensitive reading of the same operations. For the logic of the underlying values see Belnap four-valued logic.

Limits and open problems

• Draft status. The manuscript's own status is draft. Nothing here has been peer reviewed.
• Finite checks versus general theorems. Properties 1 through 6, Theorem 3 and the dynamics results are statements about a four-element (or three-element) algebra and are established by enumeration. Theorem 1 is cited from the literature for arbitrary integral commutative residuated lattices.
• Theorem 2 is a sketch. The functoriality argument checks the generating morphism classes but is not a full formal proof.
• Dependence on cited results. Decidability and the Chu/linear-logic identification are inherited from other authors' theorems and apply only so far as the fiber algebras satisfy their hypotheses.
• Contrapositive. The naive contrapositive fails; the only recovered symmetry here is the Nelson identity, proved on $\mathbf{2}\otimes\mathbf{2}$ and open for non-idempotent lattices.
• Beyond $\mathbf{2}$. The paper's concrete computations are for the two-element parameter lattice. Which results lift to larger residuated lattices is not settled.
• Fusion and Frobenius. In related work on the full hyperdoctrine, Frobenius reciprocity for the fusion $\odot$ fails because $\odot$ is non-integral (its unit $\top$ is not the truth-order top); fusion and residual therefore live at the fiber-algebra layer, beneath the hyperdoctrine's own adjoints.

Related

• Belnap four-valued logic
• What is a bilattice?
• Paraconsistent settling and comprehension
• The Nelson identity on four-valued truth
• Paraconsistent transfinite linear agent integration
• Obsmetrologia: formal mathematics in Lean 4
• Sibling sites: 561.group, engineering.561.group, operations.561.group, services.561.group, market.561.group