Quarantine, don't explode — isolation as paraconsistency

Parent: recursive-harness

Classical logic has a landmine for any belief store: ex falso quodlibet — from one contradiction, EVERYTHING follows. This is fine for mathematics (where consistency is sacred and a contradiction means start over), but fatal for a store fed by a fallible solver. An LLM-asserted constraint set WILL contain contradictions somewhere (llm-as-fallible-theory-solver), and under classical logic, a single contradiction means the entire store collapses into proving anything — a logical explosion that makes reasoning useless.

The softening: paraconsistent logic

Paraconsistent logics block explosion: a contradiction stays local; inference continues normally in unaffected regions. The consistency requirement softens from global (one poison pill kills the store) to scoped. A contradiction in one domain doesn't metastasize through the whole belief lattice. This is not inconsistency as a feature (which would be incoherent), but inconsistency as a containable event — the same way a sandboxed process can crash without crashing the kernel.

The harness operationalization — scoped by provenance

The no-good/belief store must be scoped by provenance: a contradiction discovered in region R invalidates only conclusions whose provenance passes through R. The coordinator's provenance graph computes that cone mechanically. Beliefs from different sources or worlds coexist; a clash triggers quarantine of the cone, not global panic.

Concretely: when an LLM asserts a fact f and later asserts ¬f, both assertions are recorded with their provenance (which reasoning step, which input set, which world). A contradiction is not an inconsistency in the store; it is a localized collision that invalidates downstream conclusions that depend on the collision cone, and prompts conflict-learning.

Two kinds of contradiction, two responses

Within a pinned world: a genuine conflict — analyze it, learn the no-good, backjump (conflict-learning-and-backjumping). Contradiction as fuel for search acceleration.

Between worlds, or between soft beliefs in the meta-store: NOT a conflict at all (world-choice and consistency-gate: different worlds may disagree on facts). Among unsound LLM-asserted beliefs, disagreement is expected background noise — a feature of working with fallible \varepsilon oracles, not a bug. Paraconsistency is the logic of living with the second kind while still exploding (usefully) on the first.

Isolation gets a logical identity

Control #5 (isolation/sandboxing, control-methods) has so far been an engineering practice; paraconsistency is its logic-side name: sandboxing beliefs = blocking ex falso by construction. Scoped stores, per-world constraint sets, transaction-confined side effects — all one move: keep the blast radius of a contradiction proportional to its provenance cone, never global. The SAT kernel's implication graph (recorded provenance) is the tool that makes this mechanical.

The one-liner

A fallible solver guarantees contradictions; the choice is not whether to have them but whether one of them can kill the whole store. Quarantine by provenance, explode only inside a pinned world.