Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I am trying to prove

$$ (p \lor q) \land (\lnot p \lor \lnot q) \Rightarrow (p \land \lnot q) \lor (\lnot p \land q) $$ using Natural deduction.

But I am unable to get beyond the implication reduction and the conjuction elimination on the left.

Can someone please suggest something to finish the proof.

share|cite|improve this question
Well, $p$ and $\lnot p$ cannot both be true. Likewise for $q$ and $\lnot q$. – Jack Rousseau Feb 2 '13 at 5:57
In words: both sides of this implication are saying the same thing. In particular, they are both saying that $p$ and $q$ have different truth values. This means you could actually have an iff rather than a $\rightarrow$. – Benjamin Dickman Feb 2 '13 at 6:08
@JackRousseau So can I say that in the case p & ~p, I can assume anything to be true. Becauase that solves the proof. And, if so, what is the name of the rule? – user1791452 Feb 2 '13 at 10:01
No. It is not as simple as that. What conditions must hold for $(p \lor q) \land (\lnot p \lor \lnot q)$ to be true? The name of the rule you are referring to is ex falso quodlibet. – Jack Rousseau Feb 2 '13 at 10:19
@JackRousseau So this is what I have written: – user1791452 Feb 2 '13 at 14:01
up vote 1 down vote accepted

You'd need a rule for a proof step based on an or, something like "if we can get from $x$ to $z$, and we can get from $y$ to $z$, then we can conclude $z$ is a consequence of $x \lor y$. Also needed are rules such as: from $u$ we can derive $u \lor v$ for whatever $v$ we want.

case 1) assume $p$. Bring down next $ \lnot p \lor \lnot q$, and use some rule to arrive at $\lnot q$. Now combine the case assumption $p$ with this and get to $p \land \lnot q$, and finally use the rule about placing any other statement with this in an or to arrive at the conclusion for case 1 of $(p \land \lnot q) \lor (\lnot p \land q)$

case 2) assume $q$. This time bring down $\lnot p \lor \lnot q$ and after a few steps get again the same conclusion $(p \land \lnot q) \lor (\lnot p \land q)$ as case 1 produced.

Now looking at the two deductions of the same final $(p \land \lnot q) \lor (\lnot p \land q)$, one ("case 1") from $p$ and the other ("case 2") from $q$, you can put these two together and say you have shown that $(p \lor q) \land (\lnot p \land \lnot q)$ implies $(p \land \lnot q) \lor (\lnot p \land q).$

There are some details left out, which need to be filled in by using whatever deduction rules your version of "natural deduction" might be. But I believe the above is a general framework for the proof. Some versions use numbered lines in the proof, and refer to previous line numbers and rules used to fully justify the overall proof.

share|cite|improve this answer
I have done the proof in Coq, but I have trouble visualizing it. Here is how it looks : Require Import Classical. Variables p q : Prop. Theorem l: (p \/q) /\(~p\/~q) ->(p/\~q)\/(~p/\q). Proof. intros. destruct H. destruct H. left. split. trivial. destruct H0. contradiction. trivial. right. destruct H0. split. exact H0. exact H. contradiction. Qed. – user1791452 Feb 2 '13 at 8:37
I don't follow the steps in Coq, since I've never seen it. But it looks like at the word "split" is where the proof branches on one of the two assumed "ors" which are the two premisses of the argument. – coffeemath Feb 2 '13 at 13:46
I don't understand the part where you say "....and use some rule to arrive at ~q.". The rest is pretty trivial, I guess. This is what I have tried to do: – user1791452 Feb 2 '13 at 14:05
If you have two lines, one saying $p$ and the other saying $\lnot p \lor \lnot q$, there should be some rule which allows one to deduce $\lnot q$ from these two lines. I don't remember what this rule was called when I was doing logic, and even if I did it's likely the name given to such a step is different in whatever list of rules for natural deduction you're using. – coffeemath Feb 3 '13 at 5:18
So I have figured it out, finally. It's called bot elimination. So basically, my proof( is okay. Lines 8 and 23 is exactly where it is being implemented, just that the rule name is bot elimination (ex falso quodlibet), instead of RAA. – user1791452 Feb 3 '13 at 14:55

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.