# The Nelson Identity on Four-Valued Truth: A Corrected Contrapositive

## The Nelson Identity on Four-Valued Truth: A Corrected Contrapositive

The Nelson identity says that on the four-valued algebra FOUR, a doubly iterated implication and its negation-reversed counterpart, combined by the information-order meet, give back the single implication $x\Rightarrow y$. It is the repair for a failure: the naive contrapositive law does not hold on FOUR, because the implication and the bilattice negation do not commute. The identity is proved by checking all 16 pairs of values, and it is not known to extend to residuated lattices whose product is not idempotent.

### What is the Nelson identity?

Let FOUR be the four-element bilattice with values $\bot$ (no information), $\mathbf{t}$, $\mathbf{f}$ and $\top$ (both), as in [What is a bilattice?](https://science.561.group/bilattices-and-belnap-dunn-logic/). Let $\Rightarrow$ be the right residual of the twist-product fusion described in [The adjoint structure of predication on bilattice fibers](https://science.561.group/adjoint-structure-of-predication-on-bilattice-fibers/). Let $\sim\langle a,b\rangle=\langle b,a\rangle$ be negation, which swaps the positive and negative coordinates, and $\wedge_k$ be the meet in the information order. Then for all $x,y\in\mathbf{FOUR}$:

$$\bigl(x\Rightarrow(x\Rightarrow y)\bigr)\ \wedge_k\ \bigl(\sim y\Rightarrow(\sim y\Rightarrow\sim x)\bigr)=x\Rightarrow y.$$

The left term takes two implication-direction steps from $x$. The right term takes two negation-reversed steps, starting from $\sim y$ and ending at $\sim x$, which is the contrapositive direction. Their information-order meet is the single-step implication.

#### The proof

The source's status for this result is *proved*. The proof is direct enumeration: there are $|\mathbf{FOUR}|^2=16$ pairs $(x,y)$. For each, compute both sides from the twist-product residual formula,

$$\langle x_+,x_-\rangle\Rightarrow\langle z_+,z_-\rangle=\bigl\langle (x_+\to z_+)\wedge(z_-\to x_-),\ x_+\cdot z_-\bigr\rangle,$$

and from negation. The information-order meet then combines the two iterated implications cell by cell. The research record notes a formalization of the theorem in a Lean 4 development. As an independent sanity check for this article, the identity was also recomputed by a short script over all 16 pairs, with no counterexample.

### Why does naive contrapositive fail on FOUR?

In classical logic, $x\to y$ and $\neg y\to\neg x$ coincide. On a twist product, implication is a residual of a fusion, and the negation swaps the two coordinates; the two operations interact nontrivially and do not commute. A concrete witness, checked from the formulas: $\sim(\mathbf{t}\odot\mathbf{t})=\sim\mathbf{t}=\mathbf{f}$, while $\sim\mathbf{t}\Rightarrow\sim\mathbf{t}=\mathbf{f}\Rightarrow\mathbf{f}=\mathbf{t}$. So the contrapositive form $\sim(a\odot b)=\sim b\Rightarrow\sim a$ is violated at $a=b=\mathbf{t}$. The failure is structural, not an accident of one value.

The Nelson identity records what symmetry survives. One step of residuation does not respect negation, but two steps in each direction, met in the information order, do. So the identity is a *corrected contrapositive principle*: it is not a claim that the naive form commutes with twist-product negation.

### Where does the name come from?

The name connects to a line of work on negation that begins with David Nelson's logic of constructible falsity (Nelson 1949), which treats falsity as something constructively established, independently of truth. The twist-product literature on residuated lattices, in the work of Busaniche and Cignoli (Busaniche & Cignoli 2014) and Chajda and Langer (Chajda & Langer 2021), studies implications built from a lattice implication and a negation in the pattern $(x\supset y)\wedge(\sim y\supset\sim x)$, which Chajda and Langer call a Nelson implication. The identity in this article is a statement about the single-step residual on FOUR and the iterations of it; the connection to Nelson's own logic is by name and shared motivation, and should not be read as a claim that the two systems coincide. A reader who wants the precise algebraic relationship should consult the cited papers directly.

The four values themselves are those of Belnap's useful four-valued logic (Belnap 1977).

### In what sense is it a conservation law?

The identity has the shape of a conservation law: an invariant that relates two different algebraic paths. One path is two forward steps; the other is two negation-reversed steps. Their information-order meet equals the one-step implication, whichever $x$ and $y$ are chosen. The source is careful that this is a conservation law only in the sense of an invariant relating two paths, and not a conservation law of Hamiltonian mechanics. There is no energy, time evolution or physical claim in it.

### Does it generalize beyond FOUR?

Not directly, and this is where the story stays open.

The algebraic reduction used in the proof depends on idempotence, $x\cdot x=x$. The Boolean lattice $\mathbf{2}$ is idempotent. In a non-idempotent lattice, terms such as $x_+\cdot x_+$ stay distinct from $x_+$, and the collapse that makes the iterated implication equal the single one does not occur.

Łukasiewicz MV-algebras are a standard non-idempotent test case, with implication $x\to y=\min(1,1-x+y)$ on the unit interval. The source records the obstruction: iterating gives

$$x\to(x\to y)=\min\bigl(1,\ 2(1-x)+y\bigr),$$

which is generally different from $x\to y=\min(1,1-x+y)$. A numeric instance, computed for this article: at $x=0.5$, $y=0$ the single implication is $0.5$ while the iterated one is $1$. So the Boolean form of the argument does not carry over, and the Nelson identity is not established for arbitrary integral commutative residuated lattices.

#### What questions does this leave?

The research record retains five open questions:

1. **Multi-valued residuation.** What defect or symmetrization replaces the Boolean identity in the Łukasiewicz case? (The source proposes studying the gap between the iterated and single implications as an exploratory object, explicitly not a proved replacement.)
2. **Iteration tower.** Repeated application of $x\to-$ gives a descending chain $x\to y\geq_t x\to(x\to y)\geq_t\cdots$. When it stabilizes, is its limit a natural Nelson analogue, and is the stabilization index an invariant?
3. **Negation choice.** A non-Boolean twist product can have several involutions. Does a generalization depend on a specified negation, or hold for any involution-equipped residuated lattice?
4. **Symmetry versus algebra.** The twist product has a dihedral symmetry that might generalize beyond Boolean algebras even when the identity does not. Can the symmetry content be separated from the algebraic identity?
5. **Parameterization.** If no analogue exists, the identity marks an intrinsically Boolean stratum within an otherwise uniform theory. Sorting which results lift over a general lattice and which are specific to $\mathbf{2}$ would itself be a structural result.

Two readings of the identity are on the table, a symmetric one (the meet combines an implication with its negation-twisted form) and a dynamic one (iteration approaches a fixed point). Neither should be promoted to a theorem until the non-idempotent case is settled. The practical stake is a stratification: structural classifications and the hyperdoctrinal apparatus may lift uniformly, while the Nelson identity may be intrinsically $\mathbf{2}$-specific.

### Limits and open problems

- **Scope.** Proved only on $\mathbf{FOUR}$ (the Boolean parameter lattice), by finite enumeration.
- **No generalization.** Not established for arbitrary integral commutative residuated lattices; the idempotence assumption is essential to the argument given.
- **No claim of conservation in physics.** The conservation-law phrasing is an analogy for an invariant.
- **Relation to Nelson's logic.** The connection to Nelson's constructible-falsity systems and Nelson algebras is by name and by the shared implication pattern; this article does not prove an equivalence.
- **Draft ecosystem.** The surrounding apparatus (fiber functors, hyperdoctrines) is described as draft in [the adjoint-structure paper](https://science.561.group/adjoint-structure-of-predication-on-bilattice-fibers/).

### 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/)
- [The adjoint structure of predication on bilattice fibers](https://science.561.group/adjoint-structure-of-predication-on-bilattice-fibers/)
- [Paraconsistent settling and comprehension](https://science.561.group/paraconsistent-settling-and-comprehension/)
- [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/)