# 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) 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) 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) 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) 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) 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) introduced the twist-product construction for bounded distributive lattices, and Fitting (Fitting 1991) 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:

| Value | Pair | Reading |
| --- | --- | --- |
| $\bot$ | $(0,0)$ | no evidence |
| $t$ | $(1,0)$ | positive evidence only |
| $f$ | $(0,1)$ | negative evidence only |
| $\top$ | $(1,1)$ | both |

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). For an introduction to the two orders, see [What is a bilattice?](https://science.561.group/bilattices-and-belnap-dunn-logic/).

### What is the residuated pair?

**Theorem 1** (Busaniche and Cignoli (Busaniche & Cignoli 2014); Chajda and Langer (Chajda & Langer 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):

| $\odot$ | $\bot$ | $t$ | $f$ | $\top$ |
| --- | --- | --- | --- | --- |
| $\bot$ | f | ⊥ | f | ⊥ |
| $t$ | ⊥ | t | f | t |
| $f$ | f | f | f | f |
| $\top$ | ⊥ | t | f | ⊤ |

| $\Rightarrow$ | $\bot$ | $t$ | $f$ | $\top$ |
| --- | --- | --- | --- | --- |
| $\bot$ | t | t | ⊥ | ⊥ |
| $t$ | ⊥ | t | f | f |
| $f$ | t | t | t | t |
| $\top$ | ⊥ | t | f | ⊤ |

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](https://science.561.group/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), 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). 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), and instantiates Maruyama's fibred algebraic semantics (Maruyama 2021) 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) 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) 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)), $\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](https://science.561.group/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), 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](https://science.561.group/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](https://science.561.group/belnap-four-valued-logic/)
- [What is a bilattice?](https://science.561.group/bilattices-and-belnap-dunn-logic/)
- [Paraconsistent settling and comprehension](https://science.561.group/paraconsistent-settling-and-comprehension/)
- [The Nelson identity on four-valued truth](https://science.561.group/nelson-identity-on-four-valued-truth/)
- [Paraconsistent transfinite linear agent integration](https://science.561.group/paraconsistent-transfinite-linear-agent-integration/)
- [Obsmetrologia: formal mathematics in Lean 4](https://science.561.group/obsmetrologia-formal-mathematics-in-lean-4/)
- Sibling sites: [561.group](https://561.group/), [engineering.561.group](https://engineering.561.group/), [operations.561.group](https://operations.561.group/), [services.561.group](https://services.561.group/), [market.561.group](https://market.561.group/)