nLab paraconsistent logic

Redirected from "dual intuitionistic logic".
Paraconsistent logic

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Paraconsistent logic

Overview

A paraconsistent logic is a logic in 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.

Examples

Here we survey 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

  • All men are mortal.
  • Some men are not mortal.
  • Therefore, some pigs can fly.

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.

  • Ex falso quodlibet holds for the positive false, 0B0\vdash B, essentially by definition. But it fails for the negative false \bot.

  • The law of non-contradiction holds for the negative false, A,¬AA,\, \neg A \;\vdash\; \bot. Since ¬A\neg A is equivalent to AA\multimap \bot, we can regard this as an instance of modus ponens for the linear implication. However, LNC fails for the positive false.

  • The additivity property holds for the positive disjunction, AABA \vdash A\oplus B, but fails for the negative disjunction \parr.

  • The disjunctive syllogism holds for the negative disjunction, ¬A,ABB\neg A,\, A \parr B \;\vdash\; B. Since ¬AB\neg A \parr B is equivalent to ABA\multimap B, this can also be regarded as an instance of modus ponens for the linear implication. However, DS fails for the positive disjunction \oplus.

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.

Relevance logics

One goal of relevance logic is to ensure that 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. Many relevance logics turn out to also be paraconsistent (although this is not a proof).

Other paraconsistent logics

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

Applications

Paraconsistent set theory

One potential application of paraconsistent logic would be to give a set theory in which the unrestricted comprehension rule is valid, but which is nontrivial. For instance, if R={xxx}R = \{ x \mid x\notin x \} is the set from Russell's paradox, then a paraconsistent logic could admit that both RRR\in R and RRR\notin R without trivializing.

It should be noted, however, that not all paraconsistent logics remain nontrivial in the presence of full comprehension. If the contraction rule is permitted (as it is in many relevance logics, then it seems hard to avoid Curry's paradox in the following form. For any statement PP, consider the Curry-Russell set C={x(xx)P}C = \{ x \mid (x\in x) \to P \}. Suppose CCC\in C; then by definition of CC we have (CC)P(C\in C)\to P, and so (using CCC\in C again, by contraction) we have PP. Therefore, (CC)P(C\in C) \to P. But then by definition of CC we have CCC\in C, and hence by modus ponens we have PP. Note that this argument does not require ECQ.

See also

  • English Wikipedia

  • Stanford Encyclopedia of Philosophy

  • Slater, B. H. (1995). “Paraconsistent Logics?”. Journal of Philosophical Logic. 24 (4): 451–454. doi:10.1007/BF01048355. S2CID 12125719.

  • Béziau, Jean-Yves (2000). “What is Paraconsistent Logic?”. In D. Batens; et al. (eds.). Frontiers of Paraconsistent Logic. Baldock: Research Studies Press. pp. 95–111. ISBN 0-86380-253-2.

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

  • Chris Mortensen, Inconsistent Mathematics, Kluwer Mathematics and Its Applications Series, Vol 312 (1995)

Last revised on June 4, 2022 at 05:16:50. See the history of this page for a list of all contributions to it.