Paraconsistent logic

Paraconsistent logic is a logical system that accepts the existence of contradictions.
In classical logic, the necessary falseness of a contradiction is considered axiomatic. The principle of explosion or ex contradictione sequitur quodlibet (Latin, "from a contradiction, anything follows") holds that refusing to accept this axiom leads to a significant problem, expressed thusly:
1	P & ¬P	Premise 	Premise
2	P 	Conjunctive elimination 	from 1
3	P & A	Disjunction introduction	from 2
4	¬P 	Conjunctive elimination 	from 1
5	A 	Disjunctive syllogism 	from 3 and 4
Which means: if P and its negation ¬P are both assumed to be true, then P is assumed to be true, from which it follows that at least one of the claims P and some other (arbitrary) claim A is true. However, if we know that either P or A is true, and also that P is not true (that ¬P is true) we can conclude that A, which could be anything, is true. Thus if a theory contains a single inconsistency, it is trivial—that is, it has every sentence as a theorem.
The characteristic or defining feature of a paraconsistent logic is that it rejects the principle of explosion The motivation for paraconsistent logic is the conviction that it ought to be possible to reason with inconsistent information. In non-paraconsistent logics, there is only one inconsistent theory: the trivial theory that has every sentence as a theorem. Paraconsistent logic makes it possible to distinguish between inconsistent theories and to reason with them.
Research into paraconsistent logic has also led to the establishment of the philosophical school of dialetheism (most notably advocated by Graham Priest), which asserts that true contradictions exist in reality, for example groups of people holding opposing views on various moral issues. Being a dialetheist rationally commits one to some form of paraconsistent logic, on pain of otherwise embracing trivialism, i.e. accepting that all contradictions (and equivalently all statements) are true. However, the study of paraconsistent logics does not necessarily entail a dialetheist viewpoint. For example, one need not commit to either the existence of true theories or true contradictions, but would rather prefer a weaker standard like empirical adequacy. 
In classical logic Aristotle's three laws, namely, the excluded middle (p or ¬p), non-contradiction ¬ (p ∧ ¬p) and identity (p iff p), are regarded as the same, due to the inter-definition of the connectives. Moreover, traditionally contradictoriness (the presence of contradictions in a theory or in a body of knowledge) and triviality (the fact that such a theory entails all possible consequences) are assumed inseparable, granted that negation is available. These views may be philosophically challenged, precisely on the grounds that they fail to distinguish between contradictoriness and other forms of inconsistency.
On the other hand, it is possible to derive triviality from the 'conflict' between consistency and contradictions, once these notions have been properly distinguished. The very notions of consistency and inconsistency may be furthermore internalized at the object language level.
Paraconsistency involves tradeoffs. In particular, abandoning the principle of explosion requires one to abandon at least one of the following two principles:[7]
Disjunction introduction	
Disjunctive syllogism 	
Both of these principles have been challenged.
One approach is to reject disjunction introduction but keep disjunctive syllogism and transitivity. In this approach, rules of natural deduction hold, except for disjunction introduction and excluded middle; moreover, inference A⊢B does not necessarily mean entailment A⇒B. Also, the following usual Boolean properties hold: double negation as well as associativity, commutativity, distributivity, De Morgan, and idempotence inferences (for conjunction and disjunction). Furthermore, inconsistency-robust proof by contradiction holds for entailment (A⇒(B∧¬B))⊢¬A.
Another approach is to reject disjunctive syllogism. From the perspective of dialetheism, it makes perfect sense that disjunctive syllogism should fail. The idea behind this syllogism is that, if ¬ A, then A is excluded and B can be inferred from A ∨ B. However, if A may hold as well as ¬A, then the argument for the inference is weakened.
Yet another approach is to do both simultaneously. In many systems of relevant logic, as well as linear logic, there are two separate disjunctive connectives. One allows disjunction introduction, and one allows disjunctive syllogism. Of course, this has the disadvantages entailed by separate disjunctive connectives including confusion between them and complexity in relating them.
Furthermore, the rule of proof by contradiction (below) just by itself is inconsistency non-robust in the sense that the negation of every proposition can be proved from a contradiction.
Proof by contradiction	If , then 
Strictly speaking, having just the rule above is paraconsistent because it is not the case that every proposition can be proved from a contradiction. However, if the rule double negation elimination () is added as well, then every proposition can be proved from a contradiction. Double negation elimination does not hold for intuitionistic logic.