Editing Paraconsistent logic (section)

==Tradeoffs==
Paraconsistency involves tradeoffs. In particular, abandoning the principle of explosion requires one to abandon at least one of the following two principles:<ref>See the article on the [[principle of explosion]] for more on this.</ref>
{| class="wikitable" style="margin: auto;"
![[Disjunction introduction]]
|<math>A \vdash A \lor B</math>
|-
![[Disjunctive syllogism]]
|<math>A \lor B, \neg A \vdash B</math>
|}

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's laws|De Morgan]], and [[idempotence]] inferences (for conjunction and disjunction).  Furthermore, inconsistency-robust proof of negation 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 of negation (below) just by itself is inconsistency non-robust in the sense that the negation of every proposition can be proved from a contradiction.

{| class="wikitable" style="margin: auto;"
![[Negation#Rules of inference|Proof of Negation]]
|If <math> A \vdash B \land \neg B</math>, then <math> \vdash \neg A</math>
|}
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]] (<math>\neg \neg A \vdash A</math>) is added as well, then every proposition can be proved from a contradiction. Double negation elimination does not hold for [[intuitionistic logic]].