Reference Sheet 4: Paraconsistent Logic for Graceful Contradiction#

Target audience: Forge auditor who knows S5 modal logic, CEM, FOL, and basic game theory but needs paraconsistent logic for reasoning in the presence of contradictions between models or within proto-formal theorems.

1. Orientation#

In classical logic, a single contradiction destroys everything. From P ∧ ¬P you can derive any proposition Q (ex contradictione quodlibet, or “explosion”). This is catastrophic for model development: if PET and JUB make even one contradictory claim about the same domain, and you reason classically over their union, every statement becomes provable — which means nothing is informative. Paraconsistent logic rejects explosion. It permits localized contradictions without global collapse. This does not mean contradictions are welcome — it means the system can contain the damage while you investigate and repair. Think of it as fire containment for formal systems: the goal is still to extinguish the fire, but you need the building to survive long enough to find the source.

2. Key Concepts#

Explosion (ex contradictione quodlibet, ECQ). The classical inference: from P ∧ ¬P, derive any Q. Written as a rule: {P, ¬P} ⊢ Q for arbitrary Q. Paraconsistent logics are exactly those that reject this rule — not every Q follows from a contradiction. Matheology use: If PET’s ax12 (Revelation Reliability) and a HELL con-finding create a local contradiction, ECQ would make the entire PET+JUB system trivially provable. Paraconsistent logic blocks this while you resolve the specific issue.

Trivialism. A system is trivial if every sentence is a theorem. Classical logic becomes trivial from one contradiction. The entire point of paraconsistency is to prevent trivialism: some things remain unprovable even in the presence of contradictions. Matheology use: During model development, proto-formal theorems (th5–th11) have incomplete semantic definitions. Temporary inconsistencies are likely. Paraconsistent containment ensures the formalized parts (th1–th4) remain non-trivial.

LP (Logic of Paradox). Priest’s LP is a minimal paraconsistent logic. It has three truth values: t (true only), f (false only), and b (both true and false). Conjunction, disjunction, and negation are defined by standard truth tables extended to include b. Crucially: P and ¬P can both have value b, and from this, LP does not derive arbitrary Q.

Entailment in LP: Γ ⊨_LP Q iff every LP-valuation that makes all of Γ at least designated (t or b) also makes Q designated.

Matheology use: When two models assign contradictory properties to an overlapping domain entity, assigning truth value b to the contested proposition preserves reasoning about everything else. LP is the “minimal cost” paraconsistent system.

Relevant logic. A family of logics (R, E, T) that restrict entailment to cases where premises are relevant to the conclusion. In relevant logics, P ∧ ¬P ⊢ Q fails not only because of paraconsistency but because P has no relevance connection to arbitrary Q. Formally, the variable- sharing property: A ⊢ B only if A and B share at least one propositional variable. Matheology use: HELL findings should be relevant to the axioms they attack. A con-finding about ax25 (economic mechanism) should not propagate to th3 (no isolated creation) — there is no shared variable. Relevant logic enforces this boundary formally.

Dialetheism. The philosophical position that some contradictions are true — not merely tolerated as temporary failures but genuine features of reality. The Liar Paradox (“this sentence is false”) is the paradigm case.

When useful: If the matheology system encounters self-referential structures (a model that models itself) or boundary cases where two domains genuinely overlap with incompatible predicates.

When dangerous: If used as an excuse to avoid repairing genuine errors. The matheology system’s HELL methodology exists to find and fix contradictions. Dialetheism should be a last resort for structurally irresolvable tensions, not a first response to any inconsistency.

Chunk-and-permeate. A strategy (Brown and Priest, 2004) for reasoning with inconsistent information: divide the knowledge base into consistent chunks, reason classically within each chunk, then permeate conclusions between chunks only when safe (no contradiction propagation). Matheology use: PET and JUB are natural chunks. Reason classically within each model. Permeate conclusions between them only when they do not introduce contradictions. This is exactly what the SISYF compiler should enforce.

Preservation of classicality. In LP: any classically valid inference whose premises are all classically valued (no b values) remains valid. Paraconsistent logic is a conservative extension of classical logic when no contradictions are present. Matheology use: All existing proofs (th1–th4, which are fully formalized and presumably consistent) remain valid under LP. The paraconsistent machinery only activates where contradictions actually occur.

Degree of inconsistency. Not all contradictions are equal. A system where one proposition has value b is less inconsistent than one where fifty do. Measuring the set of contradictory propositions gives a metric of system health. Matheology use: Track which axiom-theorem pairs are in b status during development. A model where {P₁} is contradictory is salvageable; a model where half the axioms are in b is in crisis.

3. Critical Theorems#

LP preserves classical theorems in consistent fragments. If Γ is a classically consistent set of sentences, then: Γ ⊨_CL Q implies Γ ⊨_LP Q. Paraconsistency costs nothing when there are no contradictions. Why it matters: Adopting LP as the background logic for the forge does not invalidate any existing classical proof. It is a pure safety net, not a change of foundations.

LP is decidable for finite propositional bases. For a finite set of propositional variables, LP-entailment is decidable (check all 3-valued valuations). The complexity is the same as classical satisfiability, modulo the third value. Why it matters: For the finite axiom/theorem system (25 axioms, 11 theorems), automated checking of LP-entailment is computationally feasible. A forge tool could flag b-valued propositions automatically.

Relevant logics have the variable-sharing property. If A ⊢_R B in the relevant logic R, then A and B share at least one propositional variable. (Due to Anderson and Belnap, 1975.) Why it matters: This provides a formal firewall between model domains. A contradiction in economic axioms (ax25-related) cannot infect metaphysical theorems (th1–th4) because they share no propositional variables — the relevant logic literally cannot derive cross-domain consequences from the contradiction.

No finite-valued logic is fully paraconsistent and fully classical. (Proved by various authors in the 1990s.) Any logic that is paraconsistent, has a finite truth-value set, and agrees with classical logic on the two-valued fragment must either lose some classical tautologies or gain some non-classical ones. Why it matters: LP sacrifices modus ponens in contradictory contexts (if both P and ¬P are b, and P → Q is b, LP does not guarantee Q is designated). This is the price of paraconsistency. The auditor must be aware that LP weakens inference in exactly the contradictory zones — by design, but with real consequences.

Priest’s theorem on LP and set theory. LP can accommodate a naive set theory (with unrestricted comprehension) without triviality. Russell’s paradox exists as a dialetheia (both true and false) but does not collapse the system. Why it matters: If the matheology system ever needs self-referential set definitions (e.g., “the set of all models that do not model themselves”), LP provides a framework where this does not destroy everything. Whether such self-reference arises in practice depends on how far the meta-logical ambitions extend.

4. Common Pitfalls#

Treating paraconsistency as permission to be sloppy. Paraconsistency means the system survives contradictions; it does not mean contradictions are acceptable. Every b-valued proposition is a bug that should be investigated and, ideally, resolved. The HELL methodology (SIN → root-cause LIE) remains the primary response. Paraconsistent logic is the safety net, not the trampoline.

Losing modus ponens. In LP, if P has value b and P → Q has value b, then Q can have value f — modus ponens fails. This is often surprising to classically trained reasoners. In contradictory contexts, you cannot chain implications freely. Alternative inference rules (e.g., the relevant conditional →_R) are needed.

Assuming all paraconsistent logics are interchangeable. LP, relevant logics (R, E, T), Belnap’s four-valued logic, and da Costa’s C-systems all reject explosion but differ in what else they accept. LP is minimal; relevant logics add relevance constraints; C₁ is closer to classical logic but more complex. Choose the system that matches your needs, and do not mix inference rules from different systems.

Ignoring the “both” value’s semantics. In LP, a proposition with value b is both true and false. It is designated (counts as true for entailment) AND its negation is also designated. This means both P and ¬P are “assertable” when P is b. Do not assert both without flagging the contradiction.

Forgetting that classical logic is fine when consistent. If your current model fragment has no contradictions, use classical logic — it is simpler, has modus ponens, and all its rules work. Switch to paraconsistent reasoning only in the specific zones where contradictions exist or are suspected.

5. Bridge to Matheology#

Cross-model contradiction containment. PET asserts ax10 (Asymmetric Dependence: ¬S(W, G) — the world does not sustain God). JUB asserts ax22 (Divine Preference for Genuine Love: Gₙ-valuation(Gₓ(w)) — divine nature evaluates contingent experience). A strong reading of ax22 might imply that God’s evaluative activity depends on the world’s content — prima facie tension with ax10. Under classical logic, this tension (if it reaches formal contradiction) would trivialize the combined system. Under LP, the contested proposition gets value b, and reasoning continues normally in all other domains.

HELL findings as inconsistency management. The HELL database (66+ findings) is, in paraconsistent terms, a catalog of b-valued zones. Each con-finding identifies a proposition that is arguably both true (from one derivation) and false (from a counter- argument). Each pro-finding attempts to resolve the b back to t or f. The auditor can track the system’s degree of inconsistency by counting unresolved b propositions.

Chunk-and-permeate for PET+JUB compilation. Treat PET (ax1–ax14, th1–th4) and JUB (ax15–ax25, th5–th11) as chunks. Within each chunk, reason classically (both are intended to be internally consistent). When combining: permeate only those conclusions that do not introduce b values. This matches SISYF’s design — it assembles views but should refuse to propagate contradictions.

Proto-formal theorems and controlled inconsistency. th5–th11 have incomplete formal semantics (predicates like Stable(i) lack full definitions). Incomplete semantics can generate spurious contradictions: a predicate without a fixed interpretation can be “proved” true by one reading and false by another. Paraconsistent logic provides a formal status for these: they are b-valued until semantic definitions are completed, at which point they should resolve to t or f.

New questions paraconsistent logic enables:

  • What is the current degree of inconsistency of PET+JUB combined? How many propositions are b-valued?

  • Are the cross-model tensions (like ax10 vs. ax22 above) genuine contradictions or merely apparent ones resolvable by clarifying predicates?

  • Can the HELL database be formalized as a non-monotonic update system, where adding a new finding can change propositions from t to b or from b to t?

  • Should the forge adopt LP as its default reasoning logic, with classical logic as an optimization for consistent fragments — or classical logic as default with LP as a fallback for flagged zones?