# Paraconsistent federation: an ActivityPub inbox that keeps contradictions instead of last-writer-wins

## Paraconsistent federation: an ActivityPub inbox that keeps contradictions instead of last-writer-wins

A conventional ActivityPub server applies each inbound activity as it arrives, so a later `Delete` erases an earlier `Create` and two peers that disagree fight until one lands last. The Red Cup ActivityPub provider instead treats every signature-verified inbound activity as a *witnessed claim*, with polarity "for" or "against" and the activity's id as evidence, and folds claims with the Belnap knowledge join. A thing that one peer created and another deleted is reported as **contradicted**, with both witnesses, and the result is identical whatever order the activities arrived in. We ran the module to confirm both properties; the output is below.

### What is wrong with last-writer-wins in the fediverse?

ActivityPub delivers activities to an inbox asynchronously, from multiple servers, with no global clock. A `Delete` from a moderator on one server and an `Update` from the author on another can arrive in either order at a third server. If the third server applies them in arrival order, its state depends on network timing, and two servers that received the same activities in different orders diverge permanently. The usual remedies add timestamps (which are claims by the sender), vector clocks (heavy), or an authority (which is the thing federation avoids).

A different remedy is to stop pretending the inbox is deciding anything. An inbox receives *testimony*. The testimony may conflict. The honest state of a record that was created by one account and deleted by another is not "deleted" or "exists" but "told both ways, by these two witnesses". That is exactly the fourth value in Belnap's logic, introduced in [Reading HTTP in four values](https://engineering.561.group/http-status-four-valued-belnap/), and the same algebra the market sells in [Belnap's logic as an API](https://engineering.561.group/belnap-four-valued-logic-api/).

### How does an activity become a claim?

The `./inbound` module of `@red-cup-engineering/activitypub-services-section` reads an already-verified activity. Signature and proof verification belong to Fedify, before this module sees the activity; the module is described as pure, with no clock and no network. It maps each activity to a subject, a polarity and claims, with the activity's own `id` as the citation:

| Activity | Polarity | Claim |
| --- | --- | --- |
| `Create`, `Update` | for | the object's fields (an `Update` is a fresh witness, "monotone, not overwrite") |
| `Delete` | against | the object's fields, or `exists: true` for a bare IRI or tombstone |
| `Follow`, `Accept`, `Like`, `Announce`, `Block`, `Dislike` | for | a membership cell on the actor (`follows`, `accepted`, `likes`, `announces`, ...) |
| `Undo` of a `Delete` | for | the object is back |
| `Undo` of anything else | against | the wrapped claim, inverted |
| `Reject` | against | the rejected activity's membership cell |

An activity that cannot be placed (no subject, an unhandled type) becomes a *refused* batch with its reason, never a silent drop. At the inbox boundary, `receiveInbound` returns `400` for a non-ActivityStreams body or an unplaceable activity, and `202` with the observation otherwise, which matches ActivityPub's rule that a successful inbox POST is `202 Accepted` with asynchronous processing.

### How are claims combined?

`settleObservations` turns each observation into a cell of subject, predicate and object, with its `for` and `against` witness sets, and hands them to the content-addressed cell set of the Group's evidence library, which performs the Belnap knowledge join: duplicate, concurrent and opposite tellings merge by union of witnesses. The module then partitions the cells:

```js
if (witnessed.for.length > 0 && witnessed.against.length > 0) {
  out.contradicted.push({ ...base, affirmedBy: citations(witnessed.for), deniedBy: citations(witnessed.against) });
} else if (witnessed.for.length > 0) {
  out.affirmed.push({ ...base, citation: citations(witnessed.for) });
} else {
  out.denied.push({ ...base, citation: citations(witnessed.against) });
}
```

(Excerpt from `inbound.mjs`, abridged.) A claim told only "for" is affirmed; only "against" is denied; both is contradicted with the lists `affirmedBy` and `deniedBy`. Nothing is overwritten and nothing is discarded. The module's own comment states the guarantee: the fold "is commutative, associative and idempotent so delivery order cannot matter."

### What does a run show?

We ran the module on 2026-10-22 with two activities about one note: a `Create` by an author at one origin and a `Delete` by a moderator at another.

```js
const note   = { id: 'https://a.example/notes/1', type: 'Note', content: 'hello' };
const create = { '@context': 'https://www.w3.org/ns/activitystreams', id: 'https://a.example/activities/1',
                 type: 'Create', actor: 'https://a.example/actors/alice', object: note };
const del    = { '@context': 'https://www.w3.org/ns/activitystreams', id: 'https://b.example/activities/9',
                 type: 'Delete', actor: 'https://b.example/actors/mod', object: note };
```

`receiveInbound(create)` returned status `202`. Settling `[create, del]` produced two contradicted cells, one for the note's `content` and one for its `type`:

```json
{ "affirmed": [], "denied": [],
  "contradicted": [
    { "subject": "https://a.example/notes/1", "predicate": "content", "object": "hello",
      "affirmedBy": ["https://a.example/activities/1"],
      "deniedBy":   ["https://b.example/activities/9"] },
    { "subject": "https://a.example/notes/1", "predicate": "type", "object": "Note",
      "affirmedBy": ["https://a.example/activities/1"],
      "deniedBy":   ["https://b.example/activities/9"] } ] }
```

We then settled `[del, create]` in the opposite order and compared the serialized results. They were identical. The output states what each peer told the inbox, preserves both activity ids as evidence, and does not claim to know whether the note "really" exists.

### What does the outbox do with a contradiction?

`./outbox-projection` is the mirror. A subject's settled algebra becomes a `Create` activity, flagged `_contested` when any of its cells is contradicted, and the actor's outbox is an `OrderedCollection`, newest first. A downstream reader sees that the claim is disputed instead of receiving a confident-looking state that depended on a race.

### Why would anyone want this?

Three reasons, in increasing order of strangeness.

1. **Moderation transparency.** If a deletion is a claim with a witness, a server can show "removed by X, contested by Y" rather than hiding the dispute. The decision procedure, whether a human or a policy resolves a contradiction, lives outside the inbox and can be audited against the preserved witnesses.
2. **Convergence without coordination.** Because the join is commutative, associative and idempotent, two servers that have received the same set of activities hold the same settled state, whatever order or duplication occurred. That is the property conflict-free replicated data types provide, obtained here by reading activities as evidence.
3. **A common substrate.** The same cell, evidence and join machinery reads HTTP probes, citation checks and federated activities. An agent that knows what `contested` means in one place knows it in all of them.

### What does this not do?

It does not decide anything. A contradicted cell stays contradicted until a policy outside this module acts, and it does not tell you whose claim should win. It does not verify activities, since Fedify does that first. It does not infer truth: the module only reads what was admitted. Its mapping from activity type to polarity is a modeling choice; for example an `Update` is treated as another affirmative witness, not an overwrite, so a corrected field appears as a second object value for the same predicate and is not merged into one.

### How does this relate to the wider transport design?

The provider is the protocol layer of a larger design the Group calls ActivityPub++, a specification draft whose idea is that one actor has one public ActivityPub face, and its activities carry a CloudEvents envelope whose data is an A2A agent message with a single content-addressed CBOR part. The market's own outbox (130 `Offer` activities whose objects are `application/sen+cbor` documents named by `ni:` addresses) is a read-only instance of the same shape ([One catalog, five machine faces](https://engineering.561.group/x402-one-catalog-machine-interfaces/)). That nesting is design-in-progress, not a ratified standard, and we say so.

For how the provider itself is assembled and what is live today, see [ActivityPub publication provider](https://engineering.561.group/activitypub-publication-provider/).