PaperlayerView exact revision on arXiv

Source-linked AI summary

Self-extensional logics of formal inconsistency: Decidability and limits for paraconsistency

Marcelo E. Coniglio, Héctor Federico Mallea

arXiv:2608.28443v1cs.LO

TL;DR

The paper asks how far self-extensional paraconsistency in RmbC can be extended axiomatically and whether the resulting logics are decidable. It uses BALFI algebraization, axiom-pair classification, algebraic filtration, and complexity analysis, proving finite-model and decidability results for RmbC and most principal extensions while establishing validity bounds.

  • Problem

    The paper investigates which axiomatic extensions of self-extensional RmbC preserve paraconsistency, which collapse classically, and whether these logics are decidable.

  • Method

    The paper combines BALFI algebraic classification with finite-model constructions based on algebraic filtration and transfers the construction to principal extensions.

  • Results

    The paper proves a finite model property for RmbC, transfers it to thirteen of fourteen principal extensions, identifies six explosive pairs, and establishes a 2-EXPTIME upper bound with a coNP-hardness lower bound for RmbC validity.

  • Takeaways & Limitations

    Self-extensional paraconsistency extends across a classified family of principal axioms, with decidability established for RmbC and thirteen principal extensions.

  • Takeaways & Limitations

    Whether RmbC(ce) is decidable remains open because the paper’s filtration technique does not extend to that logic; with (cf), no finite paraconsistent model exists.

Abstract

from arXiv · show

RmbC is a self-extensional paraconsistent logic in the family of Logics of Formal Inconsistency (LFIs). This system is obtained from mbC (the basic LFI) by adding the replacement property via two global inference rules. RmbC is characterized by a non-explosive negation $\neg$ and a consistency operator $\circ$, which recovers the principle of explosion in a controlled way. Together with its principal axiomatic extensions, RmbC admits a standard Lindenbaum--Tarski algebraization, with Boolean algebras with LFI operators (BALFIs) as its algebraic semantics. In this paper, we study how far this self-extensional paraconsistent behavior can be extended axiomatically, starting from RmbC. We classify pairs of very natural consistency axioms according to whether they preserve paraconsistency or force classical collapse; identify six algebraically equivalent explosive cores; and isolate a separate structural obstruction for the combination of excluded middle for $\neg$ with an involutive negation. We also investigate, for the first time, the decidability of this family of self-extensional LFIs. As a first result, we prove the finite model property for RmbC with respect to BALFI semantics via an algebraic filtration, which yields decidability, and transfer this result to several paraconsistent axiomatic extensions of RmbC. Finally, we establish a 2-EXPTIME upper bound for the validity problem of RmbC and a coNP-hardness lower bound.

1 Introduction

The paper examines how far the self-extensional paraconsistency of RmbC can be extended through axioms, decidability results, and complexity analysis.

  • Motivation: LFIs accommodate contradictions without triviality by combining non-explosive negation with object-language consistency and inconsistency notions.This permits controlled recovery of explosion.
  • Algebraic classification: The paper classifies pairs of fourteen principal consistency axioms by whether they preserve paraconsistency or force classical collapse.It identifies six minimal explosive pairs and finds finite paraconsistent witnesses for the remaining pairs except (ce, cf), which has an infinite paraconsistent model.
  • Algebraic classification: A weakening of the axioms defining C1 remains paraconsistent under replacement, whereas the self-extensional version of C1 collapses to classical logic.
  • Decidability: The paper proves the finite model property for RmbC via algebraic filtration and transfers it to thirteen of fourteen principal consistency extensions.These results address the previously unexplored decidability of this family.
  • Complexity: The validity problem for RmbC receives improved complexity bounds beyond those obtained directly from filtration.

2 Preliminaries

The preliminaries define LFIs, RmbC, BALFI semantics, principal extensions, and the finite-model route to decidability. RmbC gains self-extensionality by adding global replacement rules for negation and consistency.

  • LFIs: LFIs use non-explosive negation and a consistency operator to distinguish harmless contradictions from cases where explosion is controlled.
  • RmbC: RmbC extends mbC with global replacement rules for ¬ and ◦, making provable equivalence a congruence for all connectives.This supports standard Lindenbaum–Tarski algebraization.
  • Algebraic semantics: BALFIs are Boolean algebras expanded with unary operators interpreting the non-classical connectives ¬ and ◦.The class of all such structures is denoted BI.
  • Algebraic semantics: RmbC is sound and complete with respect to BI, and every nonempty principal extension is sound and complete with respect to its corresponding variety BI(Ax).
  • Decidability: The finite model property supplies finite countermodels for non-theorems, while finite axiomatization supplies effective proof enumeration, yielding decidability.The paper applies this route to RmbC and its principal extensions.

3.1 The variety landscape: subvarieties and inclusion relations

The section maps inclusion and incomparability relations among principal subvarieties of BI. It shows that several individually distinct consistency axioms do not imply one another, while their intersections create structured containment.

  • Relations among d-axioms: BI(d1) and BI(d2) are incomparable, as witnessed by separate finite BALFIs satisfying one axiom but not the other.
  • Relations among i-axioms: BI(i1) and BI(i2) are incomparable, and each is also incomparable with BI(ciw).
  • Diagrammatic structure: BI(ci) is contained in BI(i1), BI(i2), and BI(ciw), but the three larger varieties are pairwise incomparable.Thus neither i1 nor i2 individually implies (ciw), and (ciw) implies neither i1 nor i2.
  • Relations among propagation axioms: BI(ci) and BI(cl) are incomparable, while BI(cf) and BI(ciw) are incomparable.
  • Relations involving ce: BI(ce) is incomparable with BI(ciw), BI(ci), BI(cl), and BI(cf).
  • Diagrammatic structure: The two inclusion diagrams connect at BI(ciw), which is the infimum of the upper diamond in Figure 1 and a proper subvariety of BI in Figure 2.

3.2 Paraconsistency under axiomatic extensions

The fourteen principal axiom pairs are completely classified: six pairs force classical collapse, while the remaining pairs generally admit paraconsistent BALFIs, except (ce, cf) in the finite case.

  • Complete classification: The classification identifies six explosive pairs among the fourteen principal axioms, with the remaining pairwise behavior determined algebraically or by finite-model search.Finite paraconsistent witnesses exist for every other pair except (ce, cf), although an infinite paraconsistent model exists for that combination.
  • Base explosive cases: Every algebra in BI(cl, ca∨) and BI(d1, ca→) satisfies a ∧¬a = 0, eliminating paraconsistency.These are the two base explosive cases from which the other explosive combinations are derived.
  • Unification of explosive pairs: The six explosive varieties coincide with K, where ¬a = ∼a and ◦a = 1 for every algebra element.Thus all six combinations share one classical algebraic configuration rather than six distinct collapse mechanisms.
  • Explosive pairs: The six explosive pairs are (cl, ca∨), (d1, ca→), (cl, ca→), (ciw, ca→), (ci, ca→), and (i1, ca→).The remaining four cases follow by inclusion relations among the corresponding varieties.
  • Structural obstruction: The combination (ce, cf) creates a separate finite obstruction: no finite paraconsistent BALFI satisfies both axioms, independently of ◦.Involutive negation on a finite Boolean algebra collapses to Boolean complementation, whereas infinite paraconsistent BALFIs satisfying both axioms exist.

3.3 RCila: explosion and a paraconsistent refinement

RCila is explosive under replacement because (ci) combines with (ca→), but removing (ci) and (i1) yields the paraconsistent C1-like system RCi2_1 while retaining consistency propagation.

  • Cila and C1: Cila extends positive classical logic with paraconsistent negation, gentle explosion, double negation elimination, and propagation of consistency through Boolean connectives.These propagation axioms support the hierarchical construction of da Costa’s systems Cn.
  • RCila: RCila is not paraconsistent because its axioms include the explosive pair (ci, ca→).The algebraic classification shows that every BALFI model of RCila satisfies a ∧¬a = 0.
  • Paraconsistent refinement: RCi2_1 removes (ci) and (i1), retains (i2), and replaces (cl) with (a◦) and (a¬) while preserving the propagation axioms.The weakening is designed to retain structural features of Cila without the interaction responsible for explosion.
  • Paraconsistent witness: The finite BALFI B4 satisfies the axioms of RCi2_1 and is paraconsistent because its negation is not Boolean complementation and its consistency operator is not constantly 1.B4 also demonstrates that (i1) cannot be added without losing paraconsistency.
  • Significance and outlook: RCi2_1 remains self-extensional and algebraizable while retaining full consistency propagation, suggesting a possible self-extensional analogue of da Costa’s hierarchy.Whether such a hierarchy can be developed and how far it preserves paraconsistency remain open directions.

4 Finite Model Property and Decidability of RmbC

RmbC has the finite model property with respect to BALFIs, despite the BALFI variety not being locally finite. The result yields decidability through an algebraic filtration construction.

  • Finite Model Property and Decidability: The filtration isolates subformula values, closes them under ¬ and ◦, and generates a finite BALFI preserving the relevant interpretations.The construction starts from a finite support and extends the non-classical operators on the generated Boolean subalgebra.
  • Finite Model Property and Decidability: The BALFI variety BI is not locally finite, so local-finiteness arguments alone cannot establish RmbC decidability.A finitely generated subalgebra may nevertheless be infinite.
  • Finite Model Property and Decidability: If φ is not derivable in RmbC, a finite BALFI A and valuation v refute it, with v(φ) ≠ 1.The valuation agrees with the original countermodel on every subformula of φ.
  • Finite Model Property and Decidability: RmbC is decidable because its finite model property combines with finite axiomatizability.Theoremhood can be decided by searching finite BALFIs of bounded size for a refuting model.

5 Transfer of the Finite Model Property to the Main Consistency Extensions

The algebraic filtration transfers the finite model property from RmbC to several principal axiomatic extensions. The construction uses support regions and controlled off-support defaults for the consistency operator.

  • Transfer of the Finite Model Property: The transfer construction applies to fourteen principal extensions, except for (ce), by closing finite supports and extending operators canonically outside them.The support and default-function parameters are isolated in a general lemma.
  • Transfer of the Finite Model Property: The general construction preserves BALFI equations by retaining original operator values on the support and using defaults outside it.The default for ◦ may be constant 1, constant 0, or the identity, depending on the extension.
  • Transfer of the Finite Model Property: The auxiliary lemmas establish operator behavior needed by extensions such as (ci), (d1), (d2), and (a◦).For example, BI(ci) entails ¬1 = 0 and ◦0 = 1.
  • Transfer of the Finite Model Property: For (ciw), (ci), (cl), (cf), (d1), (d2), and (a◦), nonderivable formulas have finite BALFI countermodels validating the corresponding extension.The result is stated uniformly for these seven extensions.
  • Transfer of the Finite Model Property: The (cf) case enlarges the support to include Boolean complements because verifying ¬A¬Aa ≤ a requires control at ¬Ba.The enlarged support is finite and closed under Boolean complementation.

5.3 Transfer for (ca#), # ∈{∧, ∨, →}

For the consistency axioms (ca#), the filtration enlarges the support because ◦ is applied to Boolean combinations. This yields finite countermodels for all three connectives.

  • Transfer for (ca#): The (ca#) axioms require a larger support because ◦ is applied to Boolean combinations of two elements.The Boolean subalgebra is first generated from the initial support and then closed under ◦ on that subalgebra.
  • Transfer for (ca#): For # ∈ {∧, ∨, →}, every nonderivable formula has a finite BALFI countermodel in BI(ca#).The construction uses default ◦ value 0 outside the enlarged support.
  • Transfer for (ca#): The (ca#) equation holds trivially whenever an argument lies outside the support because the default consistency value makes ◦Aa ∧ ◦Ab equal to 0.Inside the support, preservation follows from the corresponding equation in the original BALFI.

5.4 Transfer for (i1) and (i2)

The finite model property also transfers to the extensions (i1) and (i2), but their proofs require different operator defaults. The distinction reflects different algebraic mechanisms.

  • Transfer for (i1) and (i2): Both (i1) and (i2) have finite BALFI countermodels obtained by extending a Boolean subalgebra generated from a finite support.Theorems 5.7 and 5.8 state the finite-model result for each extension.
  • Transfer for (i1) and (i2): The (i1) construction uses the default ◦A(a) = 1 outside the enlarged support and relies on ¬1 = 0.The needed top-element fact follows from the algebraic properties of BI(i1).
  • Transfer for (i1) and (i2): The (i2) construction uses the identity default ◦A(a) = a outside the support, making its axiom hold by idempotence of conjunction.This avoids relying on ¬1 = 0, which fails in BI(i2).
  • Transfer for (i1) and (i2): The proofs for (i1) and (i2) are not interchangeable despite their syntactic parallelism.The paper contrasts a structural top-element fact for (i1) with an idempotence argument for (i2).

5.6 The case of (ce)

The axiom (ce) is the sole principal extension for which this paper does not establish finite model property or decidability. Combining (ce) with (cf) is definitively impossible for finite paraconsistent BALFIs, whereas (ce) alone remains open.

  • (ce) is the only one of fourteen principal axioms for which transfer of the finite model property is not established.The paper treats this as a distinct case with two logically different explanations.
  • No finite BALFI satisfying both (ce) and (cf) can remain paraconsistent, although this impossibility does not apply to infinite models.The obstruction is mathematical rather than a limitation of the filtration technique.
  • For (ce) alone, the axiom yields only a ≤ ¬¬a, so it does not force involutive negation and the finite-model obstruction for (ce, cf) does not apply.Accordingly, the existence of finite paraconsistent models for RmbC(ce) remains unresolved.
  • The filtration fails for (ce) because verifying the axiom requires support closure under repeated applications of ¬B, which may generate infinitely many values.A finite support may omit elements in the relevant orbit, preventing construction of the required finite Boolean subalgebra.
  • Alternative off-support definitions of ¬A either lose the required inequality or violate a basic BALFI identity.Thus, the paper’s filtration establishes neither the finite model property nor decidability for RmbC(ce).

6 Computational Complexity of RmbC

The validity problem for RmbC is coNP-hard and belongs to 2-EXPTIME. The upper bound follows from atom-level certificates enabled by the finite countermodel construction and the Absorption Lemma, while a substantial complexity gap remains.

  • coNP-hardness holds for Val(RmbC) via the identity reduction from classical propositional validity.The reduction uses the equivalence of classical and RmbC theoremhood for formulas over the classical signature.
  • 2-EXPTIME is an upper bound for Val(RmbC), obtained by first placing NonVal(RmbC) in NEXPTIME.This improves the naive 3-EXPTIME estimate based on enumerating full algebraic structures.
  • The certificate uses a finite BALFI represented as a powerset of m atoms, with m singly exponential in the formula size.Each subformula receives a bitstring, while auxiliary bitstrings encode the non-classical operators and enforce coherence, BALFI equations, functionality, and refutation.
  • 2^O(n) verification time suffices for the certificate procedure.The construction defines operators on the subformula support and extends them by Boolean complement and 1 outside that support; the Absorption Lemma guarantees a BALFI.
  • The known bounds leave a considerable gap between coNP-hardness and the coNEXPTIME, hence 2-EXPTIME, upper bound.Membership in PSPACE is conjectured but not proved.

7 Conclusion

The paper maps the paraconsistent and explosive extensions of RmbC, proves decidability for RmbC and thirteen principal extensions, and bounds RmbC validity between coNP-hardness and 2-EXPTIME. The (ce) extension remains the principal unresolved case.

  • Classification: Six minimal explosive axiom pairs are identified, and self-extensional C1 is shown to collapse to classical logic.A weaker C1-like extension remains genuinely paraconsistent under replacement.
  • Classification: The C1-like logic RCi2_1 remains paraconsistent while retaining full propagation of consistency under Boolean connectives.It is obtained by replacing stronger axioms with (i2), (a◦), and (a¬).
  • Classification: The pair (ce, cf) has no finite paraconsistent BALFI models because its structural obstruction forces classical collapse, although infinite paraconsistent models exist.The obstruction is independent of the consistency operator ◦ and is specifically finitary.
  • Decidability: The finite model property is proved for RmbC by algebraic filtration and transferred to thirteen of the fourteen principal extensions, yielding decidability.The method is non-trivial because the underlying variety BI is not locally finite.
  • Open problems: For (ce) alone, the filtration does not establish the finite model property because support closure under ¬B may require an infinite orbit, leaving decidability open.This is distinct from the definitive impossibility of finite paraconsistent models for (ce, cf).
  • Complexity: RmbC validity is placed between coNP-hardness and 2-EXPTIME, with the upper bound obtained from atom-level certificates rather than full algebra enumeration.The gap remains open, and PSPACE membership is conjectured without proof.
  • Future directions: The filtration suggests a general finite-model strategy when added axioms can be absorbed outside subformula support, but it breaks under unbounded non-classical-negation orbits.Extending the method and resolving RmbC(ce) are identified as future directions.
Loading 2608.28443v1…