nLab
paraconsistent logic

Paraconsistent logic

Overview

A paraconsistent logic is a logic it which it can happen that a contradiction is true, in the sense that both AA and ¬A\neg A hold for some proposition AA, without the logic becoming trivial in the sense that all propositions are true. Put differently, a paraconsistent logic is one in which the schema ex contradictione quodlibet:

A,¬ABA,\, \neg{A} \;\vdash\; B

(for all formulas AA and BB) does not hold. Logics which are not paraconsistent are sometimes said to be explosive: a single contradiction explodes the entire system into triviality.

Two related schemata are ex falso quodlibet:

B\bot\; \vdash\; B

and the law of non-contradiction

A,¬A.A,\, \neg{A} \;\vdash\; \bot.

Either of these may hold in a paraconsistent logic, but of course (assuming transitivity of entailment) not both.

Another pair of schemata which cannot both hold in a paraconsistent logic are additivity

AAB A \;\vdash\; A \vee B

and the disjunctive syllogism:

¬A,ABB. \neg A ,\, A \vee B \;\vdash\; B.

The fact that the two of these together imply ex contradictione quodlibet is known the Lewis independent argument.

The rest of this page surveys some paraconsistent logics. In-depth development of particular paraconsistent logics should be done on separate individual pages.

Aristotelian syllogistic

Paraconsistent logic may seem bizarre to a modern mathematician, but the universal adoption of ex contradictione quodlibet is actually quite recent, dating roughly to the invention in the 19th century of what is now called (clearly inappropriately) classical logic.

One of the oldest formalizations of logic is Aristotelian syllogistic, which is not as expressive as modern predicate logic, but could be regarded as paraconsistent. A syllogistic analogue of ex contradictione quodlibet would be a “syllogism” such as

But this is not one of the valid forms of syllogism.

Minimal logic

In minimal logic, one simply omits ex falso quodlibet from any of the usual presentations of intuitionistic logic. The law of non-contradiction remains valid. Minimal logic satisfies the law

A,¬A¬B A,\, \neg A \;\vdash\; \neg B

for any AA and BB. This is a weaker form of ex contradictione quodlibet, which is still strong enough to be undesirable if one wants to do serious things with a paraconsistent logic.

Dual intuitionistic logic

In a certain sense, ex contradictione quodlibet is “dual” to the law of excluded middle. The former asserts that A¬AA \wedge \neg A is the least truth value (it implies everything else), while the latter asserts that A¬AA\vee \neg A is the greatest truth value (namely “true”).

In particular, just as intuitionistic logic is classical logic without LEM (but with ECQ), the formal dual of intuitionistic logic satisfies LEM but not ECQ. Specifically, here is the law of non-contradiction which fails: ex falso quodlibet is still valid because it is the dual of the intuitionistically valid sequent AA \vdash \top.

Dual intuitionistic logic may be presented as a sequent calculus with the restriction that the left-hand side of any sequent has at most one formula. It can be modeled by the closed subsets of any topological space, in which \wedge and \vee are intersection and union, and ¬\neg is the closure of the complement. Thus A¬AA \vee \neg A holds because AXA¯=XA \cup \overline{X\setminus A} = X, but the law of non-contradiction fails because AXA¯A\cap \overline{X\setminus A} need not be empty (it is one definition of the boundary of AA).

Linear logic

Linear logic is also paraconsistent, although the analysis becomes complicated because connectives such as \vee and \wedge, and even \top and \bot, bifurcate into positive and negative linear versions. With the usual definition of linear negation, we have the following.

Thus, both ways to deduce ex contradictione quodlibet founder precisely on the finer analysis of connectives provided by linearity. From a linear point of view, one could say that ex contradictione quodlibet arises from a failure to appreciate that \oplus is different from \parr, and that 00 is different from \bot.

Note that linear logic does include an alternative negation which is explosive, namely A0A\multimap 0. However, this “negation” does not satisfy some other desirable properties of negation. For instance, in “classical” linear logic the linear negation ¬A=A\neg A = A\multimap\bot is involutive, ¬¬AA\neg \neg A \dashv\vdash A, and satisfies excluded middle for the negative disjunction, A¬A\vdash A \parr \neg A, but neither of these hold for the explosive negation A0A\multimap 0.

Also worth noting is that ex contradictione quodlibet can alternatively be stated in terms of a conjuction as A¬ABA \wedge \neg A \vdash B. In linear logic, of course, the meaning of this depends on whether the conjunction \wedge is positive or negative. The comma separating multiple formulas in a linear sequent is equivalent to a positive conjunction \otimes, so in that case the same analysis above applies. But for the negative conjunction &\&, even the “explosive” negation is no longer explosive: A&(A0)A\& (A\multimap 0) doesn’t entail 00, since we can only extract AA or A0A\multimap 0 but not both.

Relevant logics

In some versions of relevance logic?, no sequent can be valid unless the hypothesis and conclusion have a variable in common. Thus, ex contradictione quodlibet is invalid in general, but special cases such as p,¬ppp, \neg{p} \vdash p or pq,¬pqprp \wedge q, \neg{p \wedge q} \vdash p \vee r are valid.

But why doesn't the Lewis independent argument work? Maybe it should be that every variable in the consequent appears somewhere in the antecedent? (In which case we can't have rr in that last example.)

Other paraconsistent logics

(There are many other paraconsistent logics one could discuss…)

Paraconsistent logics (among other topic related to inconsistency) are covered in the book

Revised on September 21, 2012 19:28:46 by Toby Bartels