# Are proofs by contradiction really logical?

Let's say that I prove statement $A$ by showing that the negation of $A$ leads to a contradiction.

My question is this: How does one go from "so there's a contradiction if we don't have $A$" to concluding that "we have $A$"?

That, to me, seems the exact opposite of logical. It sounds like we say "so, I'll have a really big problem if this thing isn't true, so out of convenience, I am just going to act like it's true".

• You're a constructivist. Feb 22, 2016 at 23:35
• In classical logic we adopt the law of the excluded middle en.wikipedia.org/wiki/Law_of_excluded_middle
– user223391
Feb 22, 2016 at 23:37
• Either we have $A$, or we don’t. We prove that not having $A$ is impossible, since it leads to a contradiction. Therefore we must actually have $A$. (There are some people who don’t accept the truth of my first sentence: they don’t accept the law of the excluded middle. I have yet to meet anyone who does not accept it in everyday life, however, and I’ve very little sympathy with the objections raised by those who do have a problem with it in logic or mathematics.) Feb 22, 2016 at 23:38
• Even constructivists believe $q\implies (p\lor\lnot p)$ leads to $\lnot q$. They just don't believe that $\lnot\lnot q\implies q$. @GitGud Feb 22, 2016 at 23:40
• @ThomasAndrews I assume you meant $p\land \neg p$. I don't disagree and I stand by my statement. In your notation and using the OP's actual words, $q$ would be the OP's $\neg A$ and the OP is asking how to get $A$, not how to get $\neg \neg A$, hence my comment. Feb 23, 2016 at 0:07

## 14 Answers

Proof by contradiction, as you stated, is the rule$\def\imp{\Rightarrow}$ "$\neg A \imp \bot \vdash A$" for any statement $A$, which in English is "If you can derive the statement that $\neg A$ implies a contradiction, then you can derive $A$". As pointed out by others, this is not a valid rule in intuitionistic logic. But I shall now show you why you probably have no choice but to agree with the rule (under certain mild conditions).

You see, given any statement $A$, the law of excluded middle says that "$A \lor \neg A$" is true, which in English is "Either $A$ or $\neg A$". Now is there any reason for this law to hold? If you desire that everything you can derive comes with direct evidence of some sort (such as various constructive logics), then it might not hold, because sometimes we have neither evidence for nor against a statement. However, if you believe that the statements you can make have meaning in the real world, then the law obviously holds because the real world either satisfies a statement or its negation, regardless of whether you can figure out which one.

The same reasoning also shows that a contradiction can never be true, because the real world never satisfies both a statement and its negation at the same time, simply by the meaning of negation. This gives the principle of explosion, which I will come to later.

Now given the law of excluded middle consider the following reasoning. If from $\neg A$ I can derive a contradiction, then $\neg A$ must be impossible, since my other rules are truth-preserving (starting from true statements they derive only true statements). Here we have used the property that a contradiction can never be true. Since $\neg A$ is impossible, and by law of excluded middle we know that either $A$ or $\neg A$ must be true, we have no other choice but to conclude that $A$ must be true.

This explains why proof by contradiction is valid, as long as you accept that for every statement $A$, exactly one of "$A$" and "$\neg A$" is true. The fact that we use logic to reason about the world we live in is precisely why almost all logicians accept classical logic. This is why I said "mild conditions" in my first paragraph.

Back to the principle of explosion, which is the rule "$\bot \vdash A$" for any statement $A$. At first glance, this may seem even more unintuitive than the proof by contradiction rule. But on the contrary, people use it without even realizing. For example, if you do not believe that I can levitate, you might say "If you can levitate, I will eat my hat!" Why? Because you know that if the condition is false, then whether the conclusion is true or false is completely irrelevant. They are implicitly assuming the rule that "$\bot \imp A$" is always true, which is equivalent to the principle of explosion.

We can hence show by a formal deduction that the law of excluded middle and the principle of explosion together give the ability to do proofs by contradiction:

[Suppose from "$\neg A$" you can derive "Contradiction".]

$A \lor \neg A$. [law of excluded middle]

If $A$:

$A$.

If $\neg A$:

Contradiction.

Thus $A$. [principle of explosion]

Therefore $A$. [disjunction elimination]

Another possible way to obtain the proof by contradiction rule is if you accept double negation elimination, that is "$\neg \neg A \vdash A$" for any statement $A$. This can be justified by exactly the same reasoning as before, because if "$A$" is true then "$\neg A$" is false and hence "$\neg \neg A$" is true, and similarly if "$A$" is false so is "$\neg \neg A$". Below is a formal deduction showing that contradiction elimination and double negation elimination together give the ability to do proofs by contradiction:

[Suppose from "$\neg A$" you can derive "Contradiction".]

If $\neg A$:

Contradiction.

Therefore $\neg \neg A$. [contradiction elimination / negation introduction]

Thus $A$. [double negation elimination]

• @Nemo: The underlying assumption is that there is one single real world. You may ask, why is this reasonable? Perhaps there are many worlds? I simply say, those many worlds that you might talk about and their properties and interactions are all still governed by some single underlying mechanism in some overarching framework, which is just a part of the true real world, which is the entirety of everything. There is just one entirety. Feb 24, 2016 at 8:23
• Everything for which we know one of A and not A to be true, only one of them is true. I am unaware of an observation of the "real world" that actually shows that always A or not A is true: that presumes there is nothing inherently unknowable about the real world, and/or that the real world exists in ways we cannot know about. Are there sub-plank gremlins who move particles following our physical laws and use QM as a joke on us? That is unknowable: stating it is either true or false is ridiculous. It has no impact on any possible observations we can make.
– Yakk
Feb 24, 2016 at 15:14
• Let's try a specific statement; say, the Continuum Hypothesis (CH). Are you asserting that CH is definitely either true or false in the "real world"? I am not sure I even know what that means, much less that it is "intuitively clear". And isn't calling something "intuitively clear" basically the same as making it an axiom? In which case, your argument reduces to "if you believe the law of the excluded middle then you should believe the law of the excluded middle"...
– Nemo
Feb 24, 2016 at 19:09
• @Nemo: But defining truth of statements over PA is circular since it's only meaningful in some meta-system that already has the standard model of PA as an object! The question of why we should accept any particular meta-system then arises... I mentioned the approximate real world interpretation of PA to avoid that; at least we can say that all evidence points to PA being meaningful for numbers below $2^{2^{30}}$. Back to CH, it is a meaningful statement about the real world if you can give a real-world interpretation of ZFC. If not, then it's not a "statement" for the purposes of my post. Feb 25, 2016 at 7:38
• @Nemo: In short, the justification for classical logic is that it is the most reasonable when we want a logic system that can handle the real world as a model. It does not mean that non-classical logics like intuitionistic logic are not applicable in specific situations. We also have to study non-classical logics within a classical framework, because to state any meta-property of a non-classical logic, we already assume that either the logic satisfies the property or it does not! If law of non-contradiction does not hold in the meta-system, then what's the point of proving any meta-property? Feb 25, 2016 at 7:48

A contradiction isn't a “problem”. A contradiction is an impossibility. This isn't a matter of saying “Gee, if I have fewer than 20 dollars in the back I won't be able to go out to dinner and I want to so badly, I'll just assume I have more than 20 dollars.” This is a matter of walking into the bank and saying "I'd like to withdraw 20 dollars" and having a trapdoor under you collapse and a 300 lb security guard jumping on your spleen shouting in you ear “You don't have it!!! You don't have it!!”

You can't just say “Oh, I got a contradiction when I assumed I had 20 dollars... But that doesn't mean I don't have 20 dollars.”

It means precisely that. It is impossible for you to have 20. So you must conclude you don't have 20 dollars.

If you get a contradiction, it just isn't possible for A to be false.

A contradiction, by its definition is an impossibility. So if you assume A isn't true and you get a contradiction. You have proven that it is impossible for A not to be true. If it is impossible for something not to be true what other options are there?

• "If it is impossible for something not to be true what other options are there?" Hm, well, what is the sound of one hand clapping? Feb 23, 2016 at 5:14
• @Mehrdad Obligatory Simpsons link Feb 23, 2016 at 6:17
• I think your example may be precisely the kind of counter-example the OP was thinking of. If you go to the bank and ask to withdraw \$20, and the bank says it's not there, it's actually still possible that you have \$20 and they simply made a mistake. It can and does happen. So the contradiction is solved by learning there was a mistake, but it wasn't a mistake in your assumption of having \$20. Rather, it was a mistake in the bank's ability to count. If assuming A leads to contradiction, ¬A may not be the answer if the mistake was assuming B instead of ¬B. Which may mean A and ¬A contradict Feb 23, 2016 at 9:00 • Nice illustration, but perhaps you should stress one aspect: this is a contradiction with already proven facts. You can well have propositions contradicting one another, but you can only reject one of them after you have proven the other. – MvG Feb 23, 2016 at 19:41 • I was being general (actually I was being snarky and impatient; I have no idea why people like my answer as it's just emotional). The idea is that a "contradiction" isn't simply "something troubling". It is, in context, a proof that the possibility of the proposition is false is out right impossible. Of course you have to acccept the law of excluded middle but I don't think that was the OPs concern. Feb 23, 2016 at 22:17 NOTE FOR INTUITIONISTS: Read the OP's question: if you think the OP or any other reader at that level will benefit from what to them will be incomprehensible distinctions, by all means add to the comments on this answer. I assume you're familiar and comfortable with proofs that don't use proof-by-contradiction. The recipe for these proofs is: • Start with some statements (assumptions)$X,Y,Z$that we take to be true. • (Also start with a bunch of typically unstated statements we take to be true, like laws of arithmetic, or previously proved theorems.) • Use rules of logic that we deem to be sound: these rules take true statements and let us deduce new true statements. • Combine these to get a new statement,$A$. Since we started from true statements, and used rules that make new true statements out of old true statements, we conclude$A$is true. The recipe for a classical logic proof-by-contradiction is: • Start with some statements (assumptions)$X,Y,Z$that we take to be true. • (Also start with a bunch of typically unstated statements we take to be true, like laws of arithmetic, or previously proved theorems.) • Use rules of logic that we deem to be sound: these rules take true statements and let us deduce new true statements. • Assume statement$P$is true. • Combine these to get a new statement that we know to be false. If we hadn't included$P$, any deductions from our true statements$X,Y,Z$would be true. We did include$P$and deduced a false statement, so we conclude$P$is false. Edit: More precisely, we conclude$P$is false in the context of$X,Y,Z$all being true, or$X \wedge Y \wedge Z$imply$P$is false. The above probably won't make you comfortable with proof-by-contradiction (that takes time and thought; see note below) but it should at least show you the process isn't just assuming something we want to assume. Note: I spent many nights going to sleep worrying about the irrationality of$\sqrt2$because the only proof I knew - using contradiction - seemed so weird! • Note that$P$is a hypothesis like any other. You might as well have concluded from the same arguments that$X$,$Z$, and$P$imply that$Y$is false. Feb 23, 2016 at 5:55 • And you shouldn't have lost sleep over the irrationality of$\sqrt2$. That statement just says that$\sqrt2$cannot possibly be a rational number, and proving that is obtaining a contradiction (from the rationality hypothesis). Feb 23, 2016 at 5:58 • @MarcvanLeeuwen: I hadn't notice my imprecision :-). I hope my rewording is clearer :-). Feb 23, 2016 at 6:23 • Frentos, @MarcvanLeeuwen is trying to say that the irrationality of$\sqrt{2}$does not actually involve a true proof by contradiction. In intuitionistic logic contradiction elimination (or negation introduction) is still a valid rule, so if you define "irrational" as "not rational" you can still prove irrationality of$\sqrt{2}$in intuitionistic logic. Some people even define "$\neg A$" as "$A \rightarrow \bot$" when they rewrite everything is in terms of implication and use only modus ponens. Feb 23, 2016 at 6:43 • @user21820: As per my comment and clarified answer (did you read it?), my past loss of sleep was not over the fact of irrationality of$\sqrt2$per se, but over the subjective weirdness of the particular proof by contradiction of that fact to which I had then been exposed. I've known of constructive proofs of the same fact for years, and in any case no longer have qualms about the nonconstructive proofs. But thanks for your final sentence - that was news to me :-). Feb 23, 2016 at 7:43 The solution comes from the definition of statement: you may have not hought about it, but it is, by definition, something that must be true or false. Since you get a contradiction assuming$A$is false, it must necessarily be true. There may be some things that are not statements in real life, but in mathematics we usually deal only with them. • Your first statement is true for classical logic but not intuitionistic logic. I accept classical logic, but it's better to be clear about that. My answer explains this in detail. Feb 23, 2016 at 4:23 • Thanks, I'll keep it in mind! Feb 23, 2016 at 12:32 I found Bourbaki's "Theory Of Sets" helpful in deepening my understanding of the concept of proof when I was an undergraduate. In it "he" introduces a particular formal language, and proceeds to rigorously define the concept of proof. In particular he introduces the logical symbols$\vee$and$\lnot$. He defines$A \implies B$to be$\lnot A \vee B$, and introduces a few axioms such as$A \vee B \implies B \vee A, A \implies A \vee B, A \vee A \implies A$, and most importantly, $$\lnot\lnot A \Longleftrightarrow A$$ That is the key axiom for proof by contradiction. (This is not contradicting user21820's statements about the law of the excluded middle - just coming at it from a different direction.) A proof, according to Bourbaki, is a list of statements such that every statement in the list is • A direct application of an axiom (i.e., the axiom with variables replaced by specific expressions), or • A statement$B$, which has been preceded in the proof by two other statements$A$and$A \implies B$. A theorem is any statement that appears in a proof. After introducing this concept, he then develops several common proof techniques, which in his parlance are not actual proofs, but meta-mathematical arguments that actual proofs exist. These include • Allowing "proofs" that contain applications of previously proven theorems, instead of starting with axioms only. This indicates an actual proof exists, since you can simply precede the abreviated proof with the proofs of each theorem used in it to create a full proof. • proof by added hypothesis: You create a new mathematical theory by appending an additional axiom$A$to the normal axioms. Any proof in the augmented theory can be converted to a proof in the original theory by prepending any statements dependent on$A$with "$A \implies$". • proof by contradiction: To prove$A$, as in proof by added hypothesis, you form a new theory by appending a new axiom. In this case,$\lnot A$. In this augmented theory you then produce a contradiction. Bourbaki had already demonstrated at this point that you can prove all statements from a contradiction. In particular, you can prove$A$in the augmented theory. As with proof by added hypothesis, this means you can prove$\lnot A \implies A$in the original theory. But$\lnot A \implies A$is by definition$(\lnot \lnot A) \vee A$, which is equivalent to$A \vee A$which in turn implies$A$. So in a theory where basis laws of logic hold, if$\lnot\lnot A \Longleftrightarrow A$also holds, any proof by contradiction can be translated into a normal proof. Of course, this is only one example of how to develop a theory of proof, and others may prefer different approaches. But it remains to me the clearest demonstration I've encountered. • Indeed. Double negation elimination is another way to get to the proof by contradiction, because we simply get$\neg A \imp \bot \vdash \neg \neg A \vdash A$. I forgot to mention it. In fact, the same reasoning I gave to justify the law of excluded middle and the principle of explosion also justifies the equivalence of$\neg \neg A$and$A$, and that is how I normally explain the meaning of "$\neg$". Feb 23, 2016 at 6:02 It's just case analysis with the assumption that one of the cases must be valid. Proof that all cases but one are invalid. The one left over therefore has to be valid. The only thing you can challenge is the assumption doesn't hold. • When you assume ¬A and derive a contradiction (False) it proves A because ¬A ⟹ False == A ∨ False == A, Feb 23, 2016 at 22:41 Another way to see it is that a proof by contradiction is a simplification where you "forget", for a while, that$A$can be true. An usual scheme of proof by contradiction is the following: • Assume$\neg A$• Prove$B$• Prove$\neg B$• This is a contradiction, then$A$is true. If you want to follow the same pattern but without assuming anything false, you can do: • Start with$A\vee \neg A$(always true) • With the same arguments as before, prove$A\vee (\neg A \wedge B)$• With the same arguments as before, prove$A\vee (\neg A \wedge B \wedge \neg B)$• Since$B \wedge \neg B$is false, then you have just proven the following statements:$A\vee (\neg A \wedge$false$)$, then$A\vee ($false$)$and finally$A$. This approach manipulates only true statements, which is arguably comfortable in a proof, but the cost is that we always take into account that "$A$can also be true". Then, the bottom line is basically "Either$A$is true, or nothing". I agree with @user21820 but there is a deeper point. You say: You see, given any statement A, the law of excluded middle says that "A ∨¬A" is true, which in English is "Either A or ¬A". Now is there any reason for this law to hold? The deeper point is that if the law was not true, then nothing could be proven, nothing would be true or false. The concept of "proof" starts with the axiom that A is not non-A, to keep it in English, with a hat-tip to Aristotle for this discovery. If it were possible for A to be, at the same time and in the same respect, non-A, then you could make no statements whatsoever. You could not say "this is a cat" or "this conclusion is correct" or even "I am hungry." Why not? Because a cat could be a non-cat (a dog, a bus or a musical symphony); a feeling of hunger could be a sound, a sunrise or a moment in history; and a conclusion would continuously vary in content and in outcome: nothing would be set, nothing would certain, everything would be an ever changing, primordial mixture of colors, sounds and sensations. Because we start with the axiom A is not non-A, we can start with simple observations and form an unbroken chain to the abstract heights where proof, certainty and reason are possible. Without this simple starting point, we would never get there. Anyone who tries to deny the axiom A is not non-A has to use it in order to attempt to prove it is not true, which is another well-known fallacy. • Well a possible objection from intuitionists is that you're making the fallacy of false dichotomy. You claim that every meaningful statement is either true or false but not both. Intuitionists claim is that some meaningful statements are neither true nor false. If you prove "this is a cat" by intuitionistically acceptable means, whatever that means, then intuitionists would accept that statement as true and not false. So that statement would have a fixed truth value, and is is not justifiable for you to claim that without classical truth values every statement would be indeterminate. Feb 25, 2016 at 8:01 • However, your last sentence is still valid in a certain sense, namely that an intuitionist cannot prove intuitionistically that classical logic is false. Feb 25, 2016 at 8:02 It's a heck of a lot more logical than trying to go through infinitely many possibilities. For example, let's say statement $$A$$ is that $$\sqrt{2}$$ is irrational. This means that there is no combination of integers $$p$$ and $$q$$ such that $$\frac{p}{q} = \sqrt{2}.$$ Obviously $$q \neq 0$$. We can assume for convenience that $$p$$ and $$q$$ are both positive. We can actually iterate $$q$$ through several positive integers, choosing a $$p$$ that will get the division arbitrarily close to $$\sqrt{2}$$, but we can't possibly iterate $$q$$ through enough possibilities to be absolutely certain. The negation of $$A$$ is therefore much easier: we assume that the $$p$$ and $$q$$ we're looking for do exist. If the pair does exist, we will be able to deduce a lot of facts about these numbers. But if the pair does not exist, we should arrive at a contradiction. • I don't think your post addresses the question at all. There are existence theorems that cannot be proven without showing that its negation leads to contradiction. Feb 1, 2021 at 16:01 easy to follow but not exacting or rigorous answer... Yes as long as the contrapositive is constructed in such a way that the answer space is complete and you disprove the contrapositive in the general case. so picture a venn diagram that where there is clear lint between true and false and all the space is filled with one or the other with no overlaps. Then find a way to contradict false in such generality that you can cross out all of false. Well all you have left is true so accept it. It sounds like we say "so, I'll have a really big problem if this thing isn't true, so out of convenience, I am just going to act like it's true". I think it's worth considering several cases. 1. If there is a contradiction between two unproven statements, that just means that they can't be true at the same time. You can't use the contradiction to directly prove or disprove either one. 2. If one of them appears particularly plausible, then that would be a good fit for your “big problem” description. But then what you have to do is conjecture that the plausible thing holds true, and prefix every statement you derive from this with “if the … conjecture holds, then …” or “assuming the … conjecture, …”. Essentially you have proven an implication: the truth of the conjecture implies everything you derive from that. 3. If your new statement contradicts something already proven, then you can indeed follow that the statement must be false. That's because assuming it to be true would not merely be a “big problem”, but by definition simply impossible, at least in terms of classical logic. Other answers expand on this point. 4. Of course, theoretically we may one day find that classical logic isn't good at describing reality, and therefore choose to discard such conclusions and start from scratch. On the other hand, logic usually doesn't claim to describe reality, but instead describe formal axiomatic systems which we believe to resemble those in reality. 5. Another thing worth considering is that someone made a mistake. But it would be wrong to say “I derived something from this proven fact, and now it's wrong.” Instead you'd have to concede that you believed some statement to be proven, when in fact it was not proven. That's because by definition, a proof can only derive true statements. Anything else may look like a proof, but isn't. Actually the reductio ad absurdum (RAA) is a little bit controversial. There exists a branch of mathematics that rejects that way of proving things it's called constructive or intutionistic math. The thing is how you go about contradictions, how you interpret that. That is how you interpret the fact that you have proven both$\phi$and$\neg\phi$or perhaps that you've proven$\phi\land\neg\phi$. The standard interpretation is that implication means that the right hand statement is true whenever the left hand statement is, which means that an implication is true if either the right statement is true or the left statement is false (or both). This means that if the left statement is false then the implication holds. One also consider any statement on the form$\phi\land\neg\phi$to be false. So with that interpretation we always would have$(\phi\land\neg\phi)\rightarrow\psi$, so if we can from$\neg\psi$prove both$\phi$and$\neg\phi$and thereby$\phi\land\neg\phi$we would have$\neg\phi\rightarrow(\psi\land\neg\psi)\rightarrow\psi$. And of course you have$\psi\rightarrow\psi$. From this follows that$(\psi\lor\neg\psi)\rightarrow\psi$, and we consider$\psi\lor\neg\psi\$ to be true.

Basically RAA is based on the fact that a statement is considered either true or false (even if we are not able to prove it), and how that makes compound statements true or false (by using negation, implication, conjunction, disjunction etc).

The best way to get a perspective on the issue - as already seen by many of the replies here - is to pull back from classical logic to something more general and to address the matter in the more general setting. The reason is that classical logic flattens out important distinctions that lend the needed perspective on the matter and clarify what is going on. So, we need to consider a more general setting where those distinctions are not conflated.

In reality, what you're actually asking - in reverse - is what kind of logic permits the rule you cited. When you ask "why", you also need to have something on the playing field where the "why not" is also the case: and that's what makes it necessary to step back. Otherwise, the answer would simply be "the rule is a rule in classical logic, because that's just what classical logic is" and that would be that.

But actually, even a foray into intuitionistic logic isn't enough. To get a better view, still, of the matter, you should also broaden the scope to bi-intuitionist logic. I will show you, first, a comparison of the three and where they fit in terms of the question and see where everything fits together.

There are actually two senses of the word "not" that are in common use; and people do actually make a distinction between the two. The weaker version of "not A" is "A is not true", while the strong one of "not A" is "A is false". The most familiar example is seen in political discourse, where respected adversaries disagree not by saying the other person's point "is false", but only that it is "not true".

In classical logic, no such distinction exists: they're the same.

In intuitionistic logic, only "is false" sense can be formulated: formalizing the "is false" sense of "not A" as ¬A = A⊃⊥. This is expressed in terms of the "only if" connective ⊃ (i.e. A⊃B means "A only if B", or equivalently "if A then B") and the "false" statement ⊥. So, let's call the stronger version of not "refute".

A key property - the defining property in fact - of the conditional is that there is a one-to-one correspondence between inferences C∧A ⊢ B (that is: inferences of B from the conjunction "C and A") and inferences C ⊢ A⊃B (i.e. inferences of the conditional A⊃B from C alone). The two are equivalent.

Applied to the "refute" operator, this expresses a one-to-one correspondence between C∧A ⊢ ⊥ and C ⊢ ¬A ... voilá! There's part of what you're looking for: the positive version of proof by contradiction. If C and A together yield a contradiction then from C alone we may infer the strong "A is false" version of "not A" - that we: we may refute A, from C.

If you use this version of "not", then the best you can achieve from this is to start with the inference C∧¬A ⊢ ⊥ and conclude that C ⊢ ¬¬A. In classical logic, this is good enough, because you have the double-negative rule. But this doesn't really answer your question: it only shifts the question over to the double-negative rule and puts the spotlight on that, instead. And, so you don't get any real insight on the matter other than "it holds in classical logic, but not in intuitionistic logic ... because they're different."

You actually want the negative version of proof by contradiction, that whenever the inference (the context of Other Stuff) and (not A) ⊢ ⊥ holds, then we also have the inference (the context of Other Stuff) ⊢ A. That's what your question is alluding to.

Collecting all the "Other Stuff" into C, this reads as the rule that given the inference C∧(not A) ⊢ ⊥ we should also have the inference C ⊢ A.

Do we? Well, that's where we get into bi-intuitionistic logic; because that's actually a characterization of the other, weaker version of "not"!

Bi-intuitionistic logic is a form of logic that lies between intuitionistic and classical logic. It includes the dual versions of the "not" and "only if" operators; which we will denote here respectively: A⊂B for "A unless B", ⨽B = ⊤⊂B, for the "B is not true" version of "not B". We'll call this the "denial" operator.

Here, the property that characterizes the "unless" connective ⊂ is that there is a one-to-one correspondence between inferences A ⊢ B∨D and A⊂B ⊢ D. That is: if we can infer the disjunction B∨D (i.e. B or D) from A, then by excluding B, we may infer D, alone, i.e. from "A unless B".

When applied to the denial operator, this leads to the rule that if we can infer ⊤ ⊢ B∨D (that is: if we can actually assert that B or D is true), the we can equivalently infer ⨽B ⊢ D: i.e. we can infer D alone from the denial of B. Now you're almost where you need to be.

In bi-intuitionistic logic, a denial may be inferred from a refutation. That is: ¬A ⊢ ⨽A is a valid inference: "is not true" follows from "is false".

The instant you assert the converse as a rule, you have classical logic. Classical logic is equivalent to bi-intuitionistic logic plus the rule ⨽B ⊢ ¬B that equates denial with refutation. And that's where important distinctions start to collapse.

The threshold from intuitionistic or bi-intuitionistic logic to classical logic is actually a watershed. If any of a large number of rules is added to either form of logic, the result is equivalent to classical logic. And every single rule in that watershed is a rule that has had a long controversial history attached to it.

My favorite one is the "continuation rule", which generalizes the equivalence rule for conditionals by attaching a "continuation" (∨D) to the right. It says that the inference C∧A ⊢ B∨D is equivalent to the inference C ⊢ (A⊃B)∨D. If you add that rule to intuitionistic logic, you get classical logic.

In many cases, the watershed rules have reflections expressed in terms of the dual operators that are valid in bi-intuitionistic logic, but don't cross the watershed. So, we can begin to see the distinctions that classical logic flattens out.

First, from the trivial valid inference ¬A ⊢ ¬A, we have ¬A∧A ⊢ ⊥. The "rule of contradiction" applies to the "refute" operator. In contrast, if the same rule is expressed in terms of the denial operator B∧⨽B ⊢ ⊥, then it's actually one of the above-mentioned watershed rules that pushes you into classical logic.

Second, from the trivial valid inference ⨽B ⊢ ⨽B, we have ⊤ ⊢ B∨⨽B. The "excluded third" rule holds for the "denial" operator. But if we try to impose the same rule on the "refute" operator ⊤ ⊢ ¬A∨A, then the result (once again) is another watershed rule and we've landed in classical logic.

Bi-intuitionism plus the rule B∧⨽B ⊢ ⊥ equals classical logic.

Intuitionism plus the rule ⊤ ⊢ ¬A∨A also equals classical logic.

Your version of proof by contradiction rule (where expressed in terms of the "refute" operator) ... as we saw above ... is tantamount to the double-negative rule; and that's one of the watershed rules that pushes you into classical logic.

In contrast, when your version of the proof by contradiction rule is expressed in terms of the "denial" operator, the result is a weaker rule that actually does hold in bi-intuitionistic logic, but can't be expressed in intuitionistic logic, because it is using the extra "denial" and "unless" connectives.

To see this, suppose that taking C and the denial of B together yields a contradiction. That is: suppose we have the inference C∧⨽B ⊢ ⊥. Then, we may switch the order of the conjunction to rewrite this as ⨽B∧C ⊢ ⊥ and then apply the conversion for the "refute" operator to rewrite this equivalently as ⨽B ⊢ ¬C and apply the conversion for the "denial" operator to write this, in turn, equivalently as ⊤ ⊢ B∨¬C.

So, now let's add the supposition of C, itself, and attach it as a conjunction. Then we have C ⊢ C∧⊤ ⊢ C∧(B∨¬C) ⊢ (C∧B)∨(C∧¬C), where we apply distributivity in the last step.

Since we already have the rule of contradiction ¬C∧C ⊢ ⊥, then switching the order of the conjunction, we have the inference C∧¬C ⊢ ⊥. Applying this to the above result, we get C ⊢ (C∧B)∨(C∧¬C) ⊢ (C∧B)∨⊥ ⊢ C∧B ⊢ B.

So, the answer to your question is: Yes. Your rule is logical - but only with the weaker "denial" operator in bi-intuitionistic logic. And the answer to the implied, underlying, question (what logic is the rule valid in) is: bi-intuitionistic logic.

Many of the "watershed" rules that push you from either intuitionism or bi-intuitionism over into classical logic have weaker versions that are written by replacing one version of the "not" operator with the other. So, we can actually segregate the rules by which "not" they work with and draw a very finely-graded distinction between each of the watershed rules.

One further example I will give here is that the double-negative rule holds in one direction A ⊢ ¬¬A for the "refute" operator and in the other direction ⨽⨽B ⊢ B for the "deny" operator. The converse direction only holds for negatives; i.e. ¬¬¬A ⊢ ¬A and ⨽B ⊢ ⨽⨽⨽B are both valid.

(Correspondingly, we may then say that in intuitionistic logic, the "regular" statement - i.e. the statements equivalent to their double-negatives - are one and the same as the "negative" statements; and that classical logic is what results from intuitionistic logic by allowing only negative statements; or more briefly: classical logic is pessimistic).

There is actually an entire hierarchy of statements that may be generated from a single statement C, by repeatedly applying different combinations of ⨽ and ¬ to C; so the word "not" acquires a very nuanced meaning in bi-intuitionistic logic. So, there is plenty of room to draw many distinctions between different nuances of each of the watershed rules, as we just did above.

There are 13 answers already, with some getting Dozens of upvotes. I wanted to Pitch in with Some Points, which may or may not help in getting a little more clarity.

(1) Consistency : Implicitly, there are assumptions in logic and mathematics, that the Postulates & Axioms are consistent. When statements break the assumptions, we get inconsistent statements and the whole thing breaks down, meaninglessly. Eg, We can show that 0+0=0, but not show that 0+0=1. If we can show that 0+0=0 AND 0+0=1, then we can extend that to show that 0=1, then 0=(0)+(0)=(0+0)+(0+0)=(1)+(1)=2, eventually all numbers become equal. Totally meaningless. Thus, consistency is a core corner stone of logic and mathematics.

(2) Contradiction : When we show that "Statement A is true" and "Statement A is false", we are claiming that "true is false". Then there is nothing more left in logic. Totally meaningless. Everything becomes true and false. Thus we must avoid contradiction.

(3) Exactly One Possibility out of many : Comparing Integers and rational numbers, we know that either (1) A<B or (2) A=B or (3) A>B. If we can Prove that two of these Possibilities are not correct or are false, then we know that the third and last remaining Possibility must be correct or must be true. Likewise, Statement A can be either (1) true or (2) false ; If we can Prove that One Possibility is not correct, then the other Possibility must be correct.

(4) Zero Possibilities out of many : We must be careful to avoid cases where all Possibilities can be wrong. Due to various reasons, Sentences like "There is exactly one line Parallel to the given line L and Passing through Point P" & "This Statement is false" & "I always tell lies" & "Try that" & "Wow" can neither be true nor false.

(5) Proof By Contradiction : If we take "the negation of A is true" and show that there is some contradiction, then we are showing that things become inconsistent. We thus conclude "Statement A is true". Implicitly, we are assuming "Consistency" & "Either A is true or A is false". When these assumptions are wrong, this Proof is not correct.