# Rule of inference for proof by contradiction.

In the book "Discrete Mathematical Structures" - Kolman, author has stated that proof by contradiction is based on the tautology ((p⇒q)∧(~q))⇒(~p).And that this argument form is often applied to the case where q is an absurdity. But this tautology is modus tollens.

In another text-book rule of inference for proof by contradiction is :

          ~p⇒c, where c is contradiction.
∴p


Please help me understand how rule of inference for proof by contradiction is modus tollens or based on above tautology. And what is the relation between two rules of inference?

-
I believe the intended meaning of "contradiction" in the block quote is actually "absurdity" (false). You simply replace $q$ in your first formula with $\neg c$. – Tunococ Jan 18 '13 at 12:57
You might also want to read the post proof by contradiction, vs. proof by contrapositive. – amWhy Jan 18 '13 at 14:34

The thing you're missing is the law of non-contradiction:

$$\neg (P \wedge \neg P)$$

i.e. $\neg c$ when $c$ is a contradiction.

To perform a proof by contradiction -- proving $\neg p$ via a proof of $p \implies c$ -- via proof by contrapositive, let $q$ be $c$.

The form of proof by contradiction you quote follows from the form I mention above by the equivalence $\neg \neg p \equiv p$. (so substitute $\neg p$ into your proof by contrapositive)

-

"Proof by contradiction" is, I take it, another label for the Reductio rule which can helpfully be displayed as

$$\quad\quad | \quad A$$ $$\quad\quad | \quad \vdots$$ $$\quad\quad | \quad C$$ $$\quad\quad | \quad \vdots$$ $$\quad\quad | \quad \neg C$$ $$\neg A$$

or (in another formulation)

$$\quad\quad | \quad A$$ $$\quad\quad | \quad \vdots$$ $$\quad\quad | \quad \bot$$ $$\neg A$$

When $A$ is a temporary assumption, which (via some subproof) leads to an explicit contradition or an absurdity $\bot$, we are allowed to discharge that temporary assumption and conclude (from whatever other premisses are in play) that it must be false, $\neg A$.

This is a valid rule of inference in systems of logic which lack a conditional (and even where a conditional can't be defined). So it is unhelpful -- to say the least -- to say that is "based on" a tautology involving a conditional (or on modus tolens).

If you do have reductio and modus ponens that modus tollens will be a derived rule:

$$A \to C$$ $$\neg C$$ $$\quad\quad | \quad A$$ $$\quad\quad | \quad C$$ $$\quad\quad | \quad \bot$$ $$\neg A$$

And conversely, if you have a conditional proof rule for introducing conditionals, modus tollens, and the assumption $\neg\bot$ then you could get reductio as a derived rule.

But, to repeat, it would be wrong to say that the result that (with a bit of help) you can get reductio from modus tollens is what "really" underlies reductio. Reductio is a warranted inferential rule because of the meaning of negation, not (even in part) because of the meaning of the conditional.

That, as they say, is the take-home message!

-
Do any of the standard packages for proof-layout Fitch-style (fitch.sty) or Gentzen-style (bussproofs.sty) work here? I'm assuming not ... but I'm unclear what the best cheat for such things is! – Peter Smith Jan 18 '13 at 15:14
PeterSmith: good question. It would be nice if someone can answer your question. I'd like to know, too! – amWhy Jan 18 '13 at 15:40