Why does the Principle of Explosion not make Mathematical Logic inconsistent?

In Reductio ad Absurdum (RAA), we determine that a proposition P is false when it derives a contradiction. If we use this same derived contradiction as the premises to the Principle of Explosion (POE), we now prove this same proposition P is true. How does that not make Mathematical Logic inconsistent?

(P → (A ∧ ¬A)) ⊢ ¬P

Principle of Explosion
(1) P → (A ∧ ¬A)
(2) (A ∧ ¬A) ⊢ P
(3) ∴ P

The above seems to show that we can correctly derive both P and ¬P thus making mathematical logic inconsistent. I always thought that the principle of explosion is ridiculous.

The answer to this question seems to be that we can't ever derive the kind of contradiction that POE needs from RAA so inconsistency is never derived.

===

Why is the Principle of Explosion (that starts with a contradiction) allowed when it is common knowledge that inference stops when reaching a contradiction?

It seems to me that a contradiction in inference is essentially the same thing as dividing by zero in computation. This makes it seem quite foolish to proceed onward with inference to explosion. Why is POE not abolished?

In the (Frank Hubeny) example of disjunction elimination there was no actual need for POE
(1) (P v Q)
(2) ¬Q
(3) ∴ P

Why can't we simply get rid of the Principle of Explosion?
The updated rule would be that inference halts at after contradiction in exactly the same way that computation halts when divide by zero occurs. POE is simply not the way that human reasoning really works. In courtroom testimony a contradiction indicates perjury.

@DanielPrendergast says:
"Well, you'll have to get rid of one of the following: Distjunction introduction A ⊢ A V B"

Yes that one seems to be a good one to get rid of.
A="I like ice cream", B="Donald Trump ate an office building".

The answer to this question seems to be that getting rid of POE requires us to get rid of disjunction introduction which seems like an utterly useless appendage.

WILL LOGIC STILL WORK WITHOUT DISJUNCTION INTRODUCTION?

• Comments are not for extended discussion; this conversation has been moved to chat. – Geoffrey Thomas Sep 13 at 8:44
• No, logic will not work without disjunction elimination. It is part of 'introduction/removal harmony' which most folks would not discard. If I must turn left, then I must turn either right or left, and that is not negotiable to normal humans. Intuitionist reject his #3, because it leads to proofs where you get a result without a path. A combing of a hairy ball either does or does not exist. A ball with no such combing can't exist. Therefore every ball has such a combing -- but we can't construct it because it fell out of a rule, and was not the result of a reasoning process. – jobermark Sep 13 at 19:49

Explosion is a property of logical consequence relations, and thus of logics, that is not trivial: Some logics have it, some don't. So there is simply no sense asking

Why can't we simply get rid of the Principle of Explosion?

If the logic you start with, say classical propostional logic, is explosive, then you cannot get rid of explosiveness and at the same time retain all properties of the intial logic. Rather what you do is change your logic. Whether that change is justified of course is determined by the field your logic is to be applied to. If your field of application is classical math, classical logic is fine and explosiveness a price worth paying, since it doesn't interfere with mathematical practice. On the other hand, if your logic is supposed to model data bases, where inconsistencies are likely to occur, explosiveness is no good. There you should choose some fragment of relevant logic like FDE.

That classical logic is explosive crucially depends on the following properties of its consequence relation:

1. Simplification: A & B ⊢ A
2. Disjunctive Weakening: A ⊢ A v B
3. Disjunctive Syllogism: A v B, ~ A ⊢ B
4. Cut rule: If M ⊢ A and N, A ⊢ B, then M, N ⊢ B

(Here M, N are sets of formulas and commas mean set union.) So, if you want to avoid explosion you must reject one of these properties. Most of the options have been played through in the literature. Parry's logic of analytic implication rejects (2), many relevant logics reject (3), Tennant's intuitionistic relevant logic rejects (4) so that logical implication is no longer transitive. But whatever option you choose, the resulting system is non-classical and that may also be a price to pay for some applications.

If you're interested in these matters of relevance you should read John Burgess's delightful piece 'No Requirement of Relevance', which appeared in the Oxford Handbook of Phil of Math and Logic.

• I would get rid of (2). A = "I like ice cream" B = "Donald Trump ate an office building". I see no need for (2). – polcott Sep 12 at 21:45
• Then you're surely interested in Parry systems, i.e. logical systems, where logical consequence requires that premises and conclusion overlap in content. Thomas Ferguson recently published his dissertation on this subject. Chapter 4 particularly adresses the failure of disjunctive weakening in Parry systems. pdfs.semanticscholar.org/7627/… – sequitur Sep 13 at 15:17
• It just seems to me that if there is no relevance connection between the premises and the conclusion that mathematical logic would be defined as a mere artifice that does not actually formalize the way that correct reasoning actually works. – polcott Sep 13 at 15:20
• @polcott But with the case of (2), the inference is "I know something, so therefore I know the thing i know and given that one or both of what i know and something else, must be true" isn't that intuitive? I'm not saying you shouldn't reject it, but it's not a surprising or counter-intuitive inference surely? – Daniel Prendergast Sep 13 at 16:47
• @EIiran It depends on how you look at it. A proof of something false does not prove an arbitrary fact. It holds officially in Heyting's formalism, but that ist not the standard of proof. Having a proof is the standard of proof. Any proof that actually used explosion would not be constructive. It is classically true that all elephants will be pink when pigs fly, but there is not a constructive proof leading from flying pigs to pink elephants. – jobermark Sep 13 at 19:33

Here is the question:

How is it that POE [the principle of explosion] does not make mathematical logic inconsistent?

If the axioms of mathematical logic were inconsistent then the principle of explosion would reduce mathematical logic to trivilism where all propositions are true since they can all be derived from that inconsistency.

However, having the principle of explosion does not make the axioms inconsistent. That would require a separate step. To show that the axioms are inconsistent one has to derive some proposition P and its negation ~P from those axioms (not from some other assumptions) prior to using that principle to derive all propositions.

Here is how Wikipedia represents that symbolically:

P, ¬PQ

The important thing to note is that we have to first derive both P and ~P. Then we can use explosion to derive Q.

Reductio ad absurdum is a way to derive the negation of an assumption should that assumption lead to a contradiction. Here is Wikipedia's description of it:

In logic, reductio ad absurdum (Latin for "reduction to absurdity"), also known as argumentum ad absurdum (Latin for "argument to absurdity"), apagogical arguments or the appeal to extremes, is a form of argument that attempts either to disprove a statement by showing it inevitably leads to a ridiculous, absurd, or impractical conclusion, or to prove one by showing that if it were not true, the result would be absurd or impossible.

That assumption is not one of the axioms. It is only tentatively assumed. That one can derive a contradiction from that assumption and other propositions is often what one desires to do so one can derive the negation of that assumption.

The OP adds this question:

Why is the Principle of Explosion (that starts with a contradiction) allowed when it is common knowledge that inference stops when reaching a contradiction?

One use of explosion in a natural deduction system is to handle one or both cases of a disjunction to derive a result using disjunction elimination (vE). Here is a proof showing how that works. To eliminate the disjunction in line 1 and derive the goal P, I have to consider two cases: P and Q. The first case, P, is easy. It is already the goal I want to derive. The second case, Q, is more difficult. However, I also have an assumption on line 2, ¬Q, that I can use to derive a contradiction, symbolized by ⊥ on line 6. Now I use explosion on line 7 to derive P from that case as well. From explosion I could have derived anything, but what I need is P. So I derive that.

Having derived P in both cases I can use disjunction elimination to eliminate the disjunction on line 1, referencing both cases on lines 3-4 and lines 5-7 and derive P on line 8.

This would be one use of explosion in a natural deduction system.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

Wikipedia contributors. (2019, August 15). Reductio ad absurdum. In Wikipedia, The Free Encyclopedia. Retrieved 13:25, September 11, 2019, from https://en.wikipedia.org/w/index.php?title=Reductio_ad_absurdum&oldid=910921053

Wikipedia contributors. (2019, September 6). Principle of explosion. In Wikipedia, The Free Encyclopedia. Retrieved 13:21, September 11, 2019, from https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=914233106

• That does not really seem to answer my (now clarified) question. – polcott Sep 11 at 16:40
• @polcott In your edited question for RAA you are assuming: P → (A ∧ ¬A). That is not RAA. To use RAA, you are only allowed to assume P. From P and any other propositions, you have to actually derive A ∧ ¬A, not just assume you can. Only then can you derive ¬P. – Frank Hubeny Sep 11 at 18:22
• I could not find any concrete example of "proof by contradiction" that was simple enough, so I had to use the above propositional logic example (thus not concrete). Given (as in geometry) that P derives (A ∧ ¬A) then ¬P is proven. I really wish I could make this concrete and not merely have P derive a hypothetical contradiction. – polcott Sep 11 at 18:28
• @polcott The assumption you made that all birds are yellow and the statement that there exists a green bird would lead to a contradiction from which you can derive that all birds are not yellow. – Frank Hubeny Sep 11 at 18:43
• @polcott Having a contradiction as an intermediate formula in a derivation does not amount to accepting it as true. Nor is there any reason to halt. And if it does appear as the final output, halting won't help, what can be derived by explosion can be derived without it. The theory is inconsistent and has to be replaced. So you are arguing for what everybody does anyway. – Conifold Sep 12 at 11:33

Rather than give you the correct technical answer (edit: okay I ended up going into some technical details, oops), which has been provided, I think I'll try and diagnose where you're intuitions have led you astray.

It seems to me that you think that if a formal system can derive (P & ¬P), then we have to accept it and thus accept the resulting explosion. If I'm right, what you're doing is assuming that whenever we write a logical statement, we're endorsing it. But we're not, we're reasoning meta-logically. That is, to write "S ⊢ Q" is to say " suppose S ⊢ Q is a true statement in the logical system" not asserting it as true, and then trying to make it false later having already said it's true. If we were doing the latter, then yes, we'd have to accept the consequence of every logical statement we write.

But we don't have to, once we get the contradiction, accept the contradiction's truth. Instead, we can (actually, we have to) accept that whatever we used to prove the contradiction can't be true (nor derivable). What we've done is shown that some part of the set of statements IS NOT derivable because we assumed it was derivable and got contradiction. That is, what we've got is the following inference from our exercise:

Let S be a finite set of statements and Q be what we've derived from S. The question is, is S itself and instance of "⊢ S" or not? Suppose S ⊢ Q. But then suppose Q ⊢ (P & ¬P). You think that now we've got (P & ¬P), and given (P & ¬P) ⊢ A ( where A = any statement and its negation), we've now exploded the logic. But on the contrary, because assuming that "⊢ S" leads to S ⊢ (P & ¬P), we know that the assumption "⊢ S" must have been false. And because it's false, we know that the explosion "⊢ A" is also false. To accept (P & ¬P) as true would lead to explosion. But instead we've reasoned that, axiomatically, ⊢ ¬(P & ¬P), therefore anything deriving (P & ¬P) can't be derivable. Then we've shown that, were S derivable, (P & ¬P) would also be derivable. But this contradicts our axiom that ⊢ ¬(P & ¬P). From this it follows that S was never derivable in the first place. But if S is not derivable, then nor is anything of the form S ⊢ Q (Q standing for anything derived from S). But S ⊢ A is an instance of S ⊢ Q. So A is not derivable from S.

For the sake of completeness (in the non technical sense), lets also note that for every possible set of statements, if that set of statements derives A (still symbolising every possible statement, ie: explosion), the same proof above applies. Therefore, there is no possible set of statements that derive A. So not only do we know that a given set of statements S doesn't derive A, but that no set of statements derive A. Therefore "⊢ A" is ALWAYS false, and as such, this proves that explosion is impossible for our logical system. Isn't that a satisfying result we've now got ourselves to put our minds at rest?

When we write "⊢ S" in this (ludicrously informal) proof, we're not committed to it, nor any of its consequences. We just write it down as if it were the case, and as soon as we derive something impossible within the axiom schema and rules of inference our system is using from pretending its true, then we have a direct way of knowing it's false.

I hope I haven't left you in even more confusion.

• Why do we allow the principle of explosion to exist when we already know that contradiction ALWAYS means stop, do not proceed? – polcott Sep 11 at 20:10
• @polcott The principle explosion exists for technical reasons of its own. It provides an argument for why we're right to reject contradictions, but it's not as if, once we derive a contradiction in our proof, we then continue to do the proof until we get explosion, and THEN say "look, we've got explosion; the contradiction is wrong". Explosion just follows from the contradiction irrespective of whether we've stop doing mathematical work having found a contradiction or not. SO, you derive contradiction, you derive explosion. Explosion is just a feature of contradiction. – Daniel Prendergast Sep 11 at 20:39
• See my edits for my reply. – polcott Sep 11 at 20:41
• My comments still apply to your edit. You're right in that, once we have a contradiction, we know something is wrong with the reasoning we used to get that contradiction (which might have been our intention, or might be a mistake on our part). We don't, having found a contradiction, then prove the resultant explosion. Explosion is just a property that the logical system has if contradictions are true. In classical logic, explosion is always false because contradictions are always false. But in principle, we could define a system where contradictions are true and explosion results – Daniel Prendergast Sep 11 at 21:03
• (1) P → (A ∧ ¬A)
• (2) (A ∧ ¬A) ⊢ P
• (3) ∴ P

No. The conclusion here should be P → P, via the Hypothetical Syllogism: P → Q, Q → R ∴ P → R .

Since P → P is a tautology there is no problem.

You might be more interested that (A ∧ ¬A) ⊢ P and (A ∧ ¬A) ⊢ ¬P are both valid.

Why is the Principle of Explosion (that starts with a contradiction) allowed when it is common knowledge that inference stops when reaching a contradiction?

Because it is not common knowledge that inference stops when reaching a contradiction. The very point of PoE is that when a contradiction is derived, anything may be inferred in that context -- including contradictions.

1. A ∧ ¬A   Premise
2. P        PoE 1
3. ¬P       PoE 1

Both these inferences are valid; which means each of the derived statements are considered at least as true as the statement from which they were inferred. Since that statement is a contradiction, P and ¬P are each guaranteed to be at least false.