Da Costa's Paraconsistent Logics (Cₙ)

Origin. Newton da Costa (1963). Brazilian school. Hierarchy of paraconsistent logics. Controlled contradiction. Foundation of South American paraconsistency.

Models. Contradiction doesn't explode. Hierarchy C₁ ⊋ C₂ ⊋ ... ⊋ C_ω of strictly decreasing strength. Consistency operator. Gradual weakening away from classical logic. Controlled inconsistency.

Formalism.

Paraconsistency: A, ¬A ⊬ B (explosion fails). Contradictions contained. Non-trivial inconsistent theories. Controlled reasoning.

Hierarchy Cₙ: C₁ ⊋ C₂ ⊋ ... ⊋ C_ω, strictly decreasing in theorems. C₁: the strongest, closest to classical. Cₙ₊₁: weaker — its consistency requirement is harder to meet, so fewer formulas behave classically. C_ω: defined directly, without the consistency operator; contained in every Cₙ.

Consistency operator (°): A° ("A is consistent"). A° ∧ A ∧ ¬A ⊢ B (if A consistent, explosion for A). Marks "safe" formulas. Classical behavior when consistent.

C₁ axioms: Positive classical core, plus A ∨ ¬A and ¬¬A → A. A° defined as ¬(A ∧ ¬A). A → (¬A → B) fails in general. But A° → (A → (¬A → B)). Conditional explosion.

Propagation of consistency: (A₁° ∧ ... ∧ Aₙ°) → (A₁ ∧ ... ∧ Aₙ)°, and likewise for ∨ and →. Consistency of the parts propagates to the compound. Higher Cₙ iterate the consistency requirement (A⁽ⁿ⁾), which is harder to satisfy, so each level has fewer theorems than the last.

Semantics: Valuation semantics. v(A) ∈ {0, 1}. v(¬A) = 1 doesn't require v(A) = 0. Non-truth-functional negation.

Applications: Inconsistent databases. Naive set theory. Dialectical reasoning. Information fusion.

Symbols.

Symbol	Unicode	Name	Meaning
¬	U+00AC	Not sign	Paraconsistent negation; ¬A does not exclude A
°	U+00B0	Degree sign	Consistency operator; A° abbreviates ¬(A ∧ ¬A)
∧	U+2227	Logical and	Conjunction
∨	U+2228	Logical or	Disjunction
→	U+2192	Rightwards arrow	Implication of the positive classical core
⊢	U+22A2	Right tack	Derivability in Cₙ
⊬	U+22AC	Does not prove	Failure of derivability, as in A, ¬A ⊬ B
⊋	U+228B	Superset of with not equal to	Strict decrease of the hierarchy in theorems
ω	U+03C9	Omega	Index of the limit system C_ω
Cₙ	—	da Costa's n-th system	Paraconsistent logic at level n
A°	—	Consistency of A	"A is well behaved"; licenses classical negation for A
A⁽ⁿ⁾	—	n-th consistency	The iterated requirement defining Cₙ
LFI	—	Logic of Formal Inconsistency	Carnielli and Marcos's generalization

Metatheory. da Costa (1963, 1974) built C₁ on positive classical propositional logic together with excluded middle and double-negation elimination, defined A° as ¬(A ∧ ¬A), and added the conditional explosion schema A° → (A → (¬A → B)) with propagation clauses carrying ° through the connectives; the higher Cₙ iterate the requirement, and the hierarchy is strictly decreasing in theorems. The systems admit no finite characteristic matrix, so they are not many-valued logics in the matrix sense. da Costa and Alves (1977) supplied instead a two-valued but non-truth-functional valuation semantics for C₁, proved it sound and complete, and extracted a quasi-matrix decision procedure, so C₁ is decidable. Algebraically the family resists treatment: Mortensen (1980) showed that every quotient algebra of C₁ by provable equivalence is trivial, which follows from the failure of replacement — A ↔ B does not license ¬A ↔ ¬B, so provable equivalence is not a congruence. Carnielli and Marcos (2002) recast the Cₙ as Logics of Formal Inconsistency with consistency taken as primitive, where a derivability adjustment theorem recovers classical consequence by adding consistency assumptions to the premises.

Applies to. Inconsistent theories. Database reasoning. Philosophy. Information systems.

Limitations. Replacement fails, so provable equivalence is not a congruence: equivalent formulas cannot be substituted inside a negation, the Lindenbaum–Tarski construction collapses to a trivial algebra, and none of the standard algebraic machinery applies. The systems have no finite characteristic matrix either, so neither truth tables nor finite-model arguments are available and the semantics has to be non-truth-functional. Negation is weak — De Morgan laws and contraposition fail for ¬, and ¬ behaves classically only where consistency has been assumed. The consistency operator is defined rather than primitive and is not itself well behaved, so A° does not deliver (A°)°, which is precisely why the levels weaken instead of refining one another; C_ω has no ° at all and so no mechanism of classical recapture. And nothing internal marks which contradictions are tolerable: the ° assumptions must be supplied from outside the logic.