# Do you know of any mathematical theorem whose proof relies on the use of the principle of explosion (ECQ)?

Ex contradictione (sequitur) quodlibet (ECQ) is almost universally recognised in mathematical logic as a valid inference.

In symbolic logic, this inference is usually expressed in the following way:

A, ¬A ⊢ B.

This is usually referred to today as "the principle of explosion":

My question is a simple one: Is there any mathematical theorem whose proof relies on the use of ECQ?

If any, what are these theorems?

• You already posted the exact same question on Mathematics SE. Please do not post the same question across multiple sites. – lemontree May 1 at 12:16
• There are logics that do not include the principle of explosion, for example, relevance logics and paraconsistent logics. The consequence is: they do not explode. What other consequences were you expecting? – Bumble May 1 at 12:19
• I changed "falsifying" to "rejecting". If I misstated your intention please roll this back. – Frank Hubeny May 1 at 16:06
• @FrankHubeny Well, not quite. I'm not sure what "rejecting" would mean in this instance. By "falsifying", I meant that someone might prove that there isn't any "explosion" to begin with: A ∧ ¬A ⊬ B. – Speakpigeon May 1 at 16:31
• Your rephrasing does not eliminate your own confusion. People do not name explosion, it appears as a combination of proof by cases (disjunction introduction) with reductios of all but one (disjunctive syllogism), which is ubiquitous since Euclid, see e.g. I.6. Is a rose only rose when it is so named? – Conifold May 5 at 11:05

Here is the question:

Given that the principle only affects validity, not soundness, I would expect no consequence at all. Is that correct?

To reject the law of explosion means rejecting the law of contradiction. Paraconsistent logics attempt "to deal with contradictions in a discriminating way". They want "to formalize inconsistent but non-trivial theories". In classical logic a single inconsistency in a theory implies that the theory is trivial since every sentence of the theory is a theorem.

However, Wikipedia notes that there are consequences when comparing these logics with classical logic:

Paraconsistent logics are propositionally weaker than classical logic; that is, they deem fewer propositional inferences valid. The point is that a paraconsistent logic can never be a propositional extension of classical logic, that is, propositionally validate everything that classical logic does. In some sense, then, paraconsistent logic is more conservative or cautious than classical logic.

The consequences of rejecting explosion (and hence non-contradiction) result in a logic that is weaker than classical logic although it may be more expressive.

Here is the question after the revision:

Do you know of any mathematical theorem whose proof relies on the use of the principle of explosion (ECQ)?

One could look at theorems that rely on indirect proof (reductio ad absudrum) or which could be viewed as cases that one eliminates. The indirect proof makes an assumption, reaches a contradiction and then rejects the assumption. This can be viewed as a proof by cases using the principle of bivalence: Either the assumption is true or its negation is true.

Here is an example. Prove that there are infinitely many primes.

For the indirect proof approach, assume there are finitely many primes and let N be the largest prime. Multiply all of the finitely many primes together and add 1 to it. That number is either prime or it contains a prime divisor larger than N. That contradicts the assumption that N is the largest prime and so the assumption is rejected.

To see this as a proof by cases where explosion is used claim that either there is a largest prime or there is not a largest prime. Consider the case when there is a largest prime. Use the method above to reach a contradiction. Use explosion to get any result one wants. Choose the result that there is no largest prime. Now in both cases one gets the same result. Use disjunction elimination to conclude there is no largest prime.

Wikipedia contributors. (2019, April 6). Paraconsistent logic. In Wikipedia, The Free Encyclopedia. Retrieved 15:44, May 1, 2019, from https://en.wikipedia.org/w/index.php?title=Paraconsistent_logic&oldid=891268995