# Prove: $(p \lor q) \land (\lnot p \lor \lnot q) \Rightarrow (p \land \lnot q) \lor (\lnot p \land q)$ using natural deduction.

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.

• 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. en.wikipedia.org/wiki/Principle_of_explosion – Jack Rousseau Feb 2 '13 at 10:19
• @JackRousseau So this is what I have written: i.imgur.com/c4fcgu8.png – user1791452 Feb 2 '13 at 14:01

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.

• 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: i.imgur.com/c4fcgu8.png – 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(i.imgur.com/c4fcgu8.png) 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

$$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}$$To prove $$( (p \lor q) \land (\lnot p \lor \lnot q) )\to( (p \land \lnot q) \lor (\lnot p \land q) )$$ using natural deduction, you must complete it by introducing that conditional.   Naturally this requires a conditional (sub)proof.   Thus you need to assume the antecedent aiming to derive the consequent.

$$\fitch{}{\fitch{\textsf{Assumption}}{\vdots\\\textsf{Consequent Derived}}\\\textsf{Conditional Introduction}}$$

The antecedent is a conjunction of disjunctions.   You shall need to eliminate these.   Eliminating each disjunction takes the form of a proof by cases.   You are going to be nesting these.

$$\fitch{}{\fitch{\textsf{Assumption}}{\textsf{Conjunction Elimination}\\\textsf{Conjunction Elimination}\\\fitch{\textsf{Assumption}}{\textsf{Reiteration}\\\fitch{\textsf{Assumption}}{\vdots\\\textsf{Consequent Derived}}\\\fitch{\textsf{Assumption}}{\vdots\\\textsf{Consequent Derived}}\\\textsf{Disjunction Elimination}}\\\fitch{\textsf{Assumption}}{\textsf{Reiteration}\\\fitch{\textsf{Assumption}}{\vdots\\\textsf{Consequent Derived}}\\\fitch{\textsf{Assumption}}{\vdots\\\textsf{Consequent Derived}}\\\textsf{Disjunction Elimination}}\\\textsf{Disjunction Elimination}}\\\textsf{Conditional Introduction}}$$

The consequent is a disjunction of two conjunctions.   You are going to need to introduce these in each branch of the nested proof by cases.   However, it looks clear that along the way you will encounter contradictions, but these may be exploded to derive the consequent.

$$\fitch{}{\fitch{\textsf{Assumption}}{\textsf{Conjunction Elimination}\\\textsf{Conjunction Elimination}\\\fitch{\textsf{Assumption}}{\textsf{Reiteration}\\\fitch{\textsf{Assumption}}{\textsf{Negation Elimination}\\\textsf{Explosion}}\\\fitch{\textsf{Assumption}}{\textsf{Conjunction Introduction}\\\textsf{Disjunction Introduction}}\\\textsf{Disjunction Elimination}}\\\fitch{\textsf{Assumption}}{\textsf{Reiteration}\\\fitch{\textsf{Assumption}}{\textsf{Conjunction Introduction}\\\textsf{Disjunction Introduction}}\\\fitch{\textsf{Assumption}}{\textsf{Negation Elimination}\\\textsf{Explosion}}\\\textsf{Disjunction Elimination}}\\\textsf{Disjunction Elimination}}\\\textsf{Conditional Introduction}}$$