A paraconsistent logic is one in which inconsistent assertions can be tolerated in that unrelated assertions can be handled in a reliable fashion. This contrasts classical logic, where inconsistency leads to insanity: from a single contradiction, any statement can derived by the principle known as ex falso quodlibet. This is why Russell's Paradox dealt such a hammer blow to the naive approach to set theory- one seemingly harmless idea, the set of all sets, gives rise to a single contradiction - but that's enough for everything else to come tumbling down too. Fortunately, in that case, the paradox can be resolved - be it by additional ideas such as Russell's notion of classes, or a more careful treatment of the basic idea of a set, such as ZF set theory - and thus the structure is placed once again on a secure footing.
Yet in practice, most mathematicians don't worry themselves about such distinctions in their day-to-day workings, and tend to think along the lines of naive set theory. In my own undergraduate career, we had a three paragraph treatment of classes in an introductory set theory course, immediately followed by the statement "In practice, we'll ignore Russell's Paradox and hope it goes away"- and indeed, this policy caused no problems for the rest of my studies. Essentially, the attitude is that the paradox is an issue only out at the weird extremes of theory- keep away from the idea of "a set of all sets" and all should be well (even if formally this isn't the case).
Moving away from the abstract purity of mathematics, the case for a more subtle handling of inconsistency is even more compelling. In massive software systems, inconsistency may well be the norm - but one should be able to at least reason confidently about components unconnected to the area of uncertainty. Sprawling databases may contain conflicting information about Alice (witness the periodic news stories about customers bemused to be told they've died), but that shouldn't let us conclude anything we like about Bob. Nor does it seem particularly appropriate to throw our hands up and declare that two people's common beliefs are completely undiscernable simply because they differ on a minor issue.
Explosion
To reason about such systems, then, one must abandon ex falso quodlibet, arriving instead at what are described as paraconsistent logics. In essence, a logical system (at least, adopting a proof-theoretic approach) consists of a fixed collection of rules of inference, into which are fed axioms - "truths" or articles of faith.These core rules tend to be compelling when examined individually, but their interaction can give behaviours which lead to fierce debates over their validity- perhaps the most famous example being the intuitionist objection to proof by contradiction.
Explosion via disjunction
The argument of interest, ex falso quodlibet is not a rule of inference but instead arises from simpler rules:
- Suppose (A AND NOT A).
- Then from (A AND NOT A) one has (A).
- Then from (A), one has (A OR B) by disjunction introduction.
- From (A AND NOT A) one has (NOT A).
- Then from (A OR B) and (NOT A) one has (B) by disjunctive syllogism.
- Thus, from (A AND NOT A) we have (B) for any B.
Steps 1-6 as a whole give us ex falso quodlibet and the explosion of 'truth'- armed with A and NOT A, we can get any B we like ("I am the pope", "The Moon is made of green cheese" etc.). Worse, we can get the negation of B as well by exactly the same argument! Thus one contradiction breeds endlessly more, yet we are certain of nothing.
If we wish to live with the contradictory statements about A, our paraconsistent logic must therefore either reject either step 3, disjunction introduction, or step 5, disjunctive syllogism; or dig deeper still and reject transitivity (that if P implies Q and Q implies R, then P implies R) to dismiss their combination into a larger rule.
The typical approach is to reject disjunctive syllogism- in particular, in the most extreme form of paraconsistency, dialetheism, where contradictions are accepted as the literal state of affairs (rather than a side effect of limited or flawed knowledge). Indeed, if one simultaneously asserts A, NOT A and NOT B then (A OR B) evaluates to true, as does (NOT A); but B does not; so the syllogism (A OR B) AND (NOT A) ⇒ B isn't valid.
However, disjunction introduction can also be attacked on the grounds that it introduces concepts unrelated to the axioms, yet their validity is then asserted by manipulation of those axioms. Hewitt2 argues that it is preferable to reject this rule of inference in the context of computer systems.
Explosion via full indirect inference
A paraconsistent logic is further constrained to reject one of proof by contradiction, the rule of weakening or double negation elimination- provided one accepted such ideas in the first place! Otherwise, there is an alternative source of explosion, full indirect inference, (P ⇒ Q) AND NOT Q) implies NOT P. In detail, this works as follows:
- (A AND NOT A) ⇒ ( NOT B ⇒ (A AND NOT A) ) by the rule of weakening ( P ⇒ (Q ⇒ P)).
- From ( NOT B ⇒ (A AND NOT A) ) we obtain NOT (NOT B) from reductio ad absurdum.
- Thus by double negation elimination on NOT (NOT B) we conclude B.
Full indirect inference essentially asks us to reject any statement that leads to both a statement and its negation, but this is an acceptable situation if we tolerate inconsistency! Here the obvious rule to exclude is reductio ad absurdum.
Limitations
It is worth noting that omitting such rules generally leaves a paraconsistent logic weaker than a consistent classical one used as source, in that less results can be derived -obviously, it is weaker than an inconsistent classical logic, where anything can be derived. Ideally, one seeks paraconsistent logics which cause minimal damage to, say, natural deduction in this way, but some trade-off is inevitable.
References
- MA10004 Sets and Sequences and CM30071 Logic and its Applications; University of Bath.
- Carl Hewitt Common Sense for paraconsistency and concurrency using unstratified inference and reflection Preprint obtained at his talk The Logical Necessity of Inconsistency, University of Edinburgh, September 2007.
For easier reading, a LaTeX-rendered version of this writeup is available here.