Proving $q\Rightarrow r \models (p\land q) \Rightarrow (p \land r)$ using only natural deduction.

I'm trying to prove

$$q\Rightarrow r \models (p\land q) \Rightarrow (p \land r)$$

using only the natural deduction rules in this handout.

Any hints? I am not allowed to do transformational stuff, such as converting everything to CNF or DeMorgan's, unless they are proven. (I'm sure that will make things easier!).

-
First off, you certainly can prove De Morgan's laws. You have to be careful about how you apply such transformations within the natural deduction framework. But you shouldn't really need those laws for this exercise. – dfeuer Jun 7 '13 at 1:57
I would most definitely like to see a proof of de Morgan's laws that isn't a big tree (I for some reason can't read those proofs as we don't learn to write Natural Deduction proofs that way). For me, hitting $p\lor q$ is like a brick wall in natural deduction if I don't have $\lnot p$ or $\lnot q$... – user54609 Jun 7 '13 at 1:58
Please double-check your statement of the problem: Is the expression you've written exactly what you are to prove? That would be rather elementary! Do you intend to write $(p\land q)\Rightarrow (p\land r)$? – amWhy Jun 7 '13 at 2:00
Yes, that is exactly what I want to prove. Yes, I suck at really elementary natural deduction proofs ;(( – user54609 Jun 7 '13 at 2:00
Eric, I did not mean to imply your problem is trivial! I am just quite sure that you must have miscopied/mistyped what it is you are supposed to conclude. – amWhy Jun 7 '13 at 2:06

$(1)\; q\rightarrow r \quad\text{premise}$

• $(2)\; p\land q\quad\text{Assumption}$

• $(3)\; p \quad\text{Conjunction Elimination}, (2)$

• $(4)\; q\quad \text{Conjunction Elimination}, (2)$

• $(5)\; r \quad \text{Modus Ponens}, (1), (4)$

• $(6)\; p\land r\quad \text{Conjunction Introduction}, (3),(5)$

$(7) \;(p \land q) \rightarrow (p\land r) \quad\text{Conditional Introduction}, (2 - 6)$

Remark: Note that when the proposition you are asked to prove is an implication, that's almost always a sign-post that, after listing the premise(s), you'll want to begin with a sub-proof, led off by the assumption of the antecedent, with the aim of arriving at the consequent.

-
$\large{\ddot\smile}$ – Babak S. Jun 7 '13 at 5:31
hmmm... modus ponens is the most common rule of inference around. So, does that imply that a proof which uses modus ponens earlier in the proof, ceteris paribus, is "more vulgar" than a proof which uses modus ponens later??? (I'm joking.) – Doug Spoonwood Jun 7 '13 at 6:28
Though I don't teach this stuff, and thus have little to no insight into ordinary students minds, I have to wonder if an exercise to prove what is asked here in two different sequences might help some students to better understand that proofs are by no means unique. – Doug Spoonwood Jun 7 '13 at 6:42
Ah. The only assumptions I have done before were negating the conclusion (of the whole thing) for a proof by contradiction. Thinking about it, of course I can do a subproof... – user54609 Jun 7 '13 at 11:40

The main question here has already been answered, but in the comments you asked for natural deduction proofs of DeMorgan's laws. I've used the rules cited in the question with two exceptions. I'm using Fitch-style disjunction elimination ($\lor E$) and biconditional introduction ($\leftrightarrow I$) rules.

The $\leftrightarrow I$ is a trivial difference; I cite the subproofs that start with $\phi$ and $\psi$ and end with $\psi$ and $\phi$, respectively, instead of deriving $\phi \to \psi$ and $\psi\to\phi$ individually and citing them.

The $\lor E$ is more significant. Disjunctive syllogism ($\lnot P, P \lor Q / Q$) is perfectly valid rule, but it's not typically taken as the elimination rule for disjunction in natural deduction systems. In the tradition of Gentzen, many natural deduction systems have an introduction and an elimination rule for each connective. For disjunction, the introduction rule is actually pair of rules which state that from either disjunct you may infer the disjunction:

$$\begin{array}{c} \phi \\ \hline \phi \lor \psi \end{array}\lor I_L \qquad \begin{array}{c} \psi \\ \hline \phi \lor \psi \end{array}\lor I_R \qquad$$

Disjunction elimination is a bit more complicated. It says that if $\rho$ is derivable from both $\phi$ and from $\psi$ and $\phi\lor\psi$ holds, then so does $\rho$ (and the assumptions are discharged). It captures proof by case reasoning.

$$\begin{array}{ccc} & [\phi] & [\psi] \\ & \vdots & \vdots \\ \phi\lor\psi & \rho & \rho \\ \hline & \rho \end{array}\lor E$$

Here is $(\lnot p \land \lnot q) \leftrightarrow \lnot(p \lor q)$:

• $\lnot(p \lor q)$ Assume.
• $p$ Assume.
• $p \lor q$ by $\lor I$ from 2.
• $\mathbf{false}$ by $\lnot E$ from 1 and 3.
• $\lnot p$ by $\lnot I$ from 2–4.
• $q$ Assume.
• $p \lor q$ by $\lor I$ from 6.
• $\mathbf{false}$ by $\lnot E$ from 1 and 7.
• $\lnot q$ by $\lnot I$ by 6–8.
• $\lnot p \land \lnot q$ by $\land I$ from 5 and 9.
• $\lnot p \land \lnot q$ Assume.
• $p \lor q$ Assume.
• $p$ Assume.
• $\lnot p$ by $\land E$ from 11.
• $\mathbf{false}$ by $\lnot E$ from 13 and 14.
• $q$ Assume.
• $\lnot q$ by $\land E$ from 11.
• $\mathbf{false}$ by $\lnot E$ from 16 and 17.
• $\mathbf{false}$ by $\lor E$ from 12, 13–15, and 16–18.
• $\lnot(p \lor q)$ by $\lnot I$ from 12–19.
1. $\lnot(p \lor q) \leftrightarrow (\lnot p \land \lnot q)$ by $\leftrightarrow I$ from 1–10 and 11–20.
-
You should finish that for yourself, but the full set is over at proofwiki.org/wiki/De_Morgan%27s_Laws_(Logic) Note that some forms require excluded middle for one of the implications. – dfeuer Jun 7 '13 at 2:35
@dfeuer Thanks for the comment! I've seen proofwiki.org a few times before, but I haven't looked around enough that it comes to mind automatically yet! Maybe I won't post the $\lnot(p \land q) \leftrightarrow (lnot p \lor \lnot q)$ after all, since it's here. It's often been my experience that proofs online are axiomatic, not natural deduction, so it's nice to see a bunch of natural deduction proofs up there, too. – Joshua Taylor Jun 7 '13 at 3:17
What does your disjunction elimination rule say? It's certainly not the one I know. – Doug Spoonwood Jun 7 '13 at 5:11
You've also only proved conditionals, not equivalences. – Doug Spoonwood Jun 7 '13 at 5:16
@DougSpoonwood Oy, I shouldn't write so late at night. You're right on not proving the equivalence, but that's just one more step of $\leftrightarrow I$ citing the two proofs, so that's not a big issue. The $\lor E$ that I used is disjunctive elimination citing two subproofs, not disjunctive syllogism. Unfortunately, that's not what the handout in the question called $\lor E$. I'll add line numbers and a link to the rules. – Joshua Taylor Jun 7 '13 at 12:18

Assume $p \land q$.

By simplification $\land \mathcal E_1$: $p$.

By simplification $\land \mathcal E_2$: $q$.

By the premise, $q \implies r$.

By modus ponens $\implies \mathcal E$: $r$.

By conjunction $\land \mathcal I$: $p \land r$.

By implication $\implies \mathcal I$: $p \land q \implies p \land r$.

-

If your professor doesn't insist on using fully parenthesized expressions in formal proofs, then you should complain bitterly either by insisting on fully parenthesized infix expressions, or by insisting on switching to Polish notation or Reverse Polish notation. A formal proof, after all, consists of a certain type of sequence of well-formed formulas, and if a sequence is not a sequence of well-formed formulas, it is not a formal proof.

I use Polish notation. Apq means (p$\lor$q), Cpq means (p$\implies$q), Np means $\lnot$p, Kpq means (p$\land$q), and Epq means "p" and "q" are logically equivalent. Correspondingly, the definition of a well-formed formula (wff... plural wffs) for the following proofs goes:

1) "p", "q", and "r" are wffs.

2) If w1 is a wff, then Nw1 is a wff.

3) If w1 and w2 are wffs, then Cw1w2, Aw1w2, Ew1w2, and Kw1w2 are wffs.

4) Anything not falling under conditions 1)-3) is not a wff for the following proofs.

To indicate a connection with more conventional terminology, X-in refers to an introduction rule for connective X, and X-out refers to an elimination rule for connective X. For any well-formed formulas "w1" and "w2" and "w3", the rules for this natural deduction system go as follows:

K-in: From w1 and w2, infer Kw1w2.

K-out: From Kw1w2, infer w1. From Kw1w2, infer w2.

A-in: From w1, infer Aw1w2. From w2, infer Aw1w2.

A-out: From Aw1w2, Cw1w3, and Cw2w3, infer w3.

C-in: From a derivation that starts with w1 and ends with w2 (where w1 and w2 have the same scope), infer Cw1w2.

C-out: From w1 and Cw1w2, infer w2.

N-in: From a derivation which starts with w1 and ends with Kw2Nw2 (where w1 and Kw2Nw2 have the same scope), infer Nw1.

N-out: From a derivation which starts with Nw1 and ends with Kw2Nw2 (where Nw1 and Kw2Nw2 have the same scope), infer w1.

E-in: From Cw1w2 and Cw2w1, infer Ew1w2.

E-out: (not used here): From Ew1w2, infer Cw1w2. From Ew1w2, infer Cw2w1.

Rule of assumption: Any assumption may get introduced so long as it the scope of assumption remains clear. If multiple assumptions get introduced, then the scope of the (n+1)th assumption falls within the scope of the nth assumption, until assumption (n+1) gets discharged by the conditional introduction rule, the negation elimination rule, or the negation introduction rule.

Proof that "Cqr |- CKpqKpr" (you wrote "|=" instead of "|-", but if you have a formal proof you've demonstrated syntactic validity which means you have "|-", where "|=" indicates semantic entailment... syntactic validity and semantic entailment in some sense can get thought to imply each other in classical propositional logic, because of soundness and completeness, but I digress.)

 1 |  Cqr  axiom (it has a permanent status, so I call the assumption an axiom)
2 || Kpq assumption
3 || q  2 K-out
4 || r 3, 1 C-out
5 || p 2 K-out
6 || Kpr 5, 4 K-in
7 |  CKpqKpr 2-6 C-in


Proof of "De Morgan's" Law ENApqKNpNq (De Morgan didn't discover these laws... they go back at least to William of Ockham, if not the Stoics).

1  |    NApq assumption
2  ||   p assumption
3  ||   Apq 2 A-in
4  ||   KApqNApq 1, 3 K-in
5  |    Np 2-4 N-in
6  ||   q assumption
7  ||   Apq 6 A-in
8  ||   KApqNApq 7, 1 K-in
9  |    Nq 6-8 N-in
10 |    KNpNq 5, 9 K-in
11      CNApqKNpNq 1-10 C-in
12 |    KNpNq assumption
13 ||   Apq assumption
14 |||  p assumption
15 ||   Cpp 14-14 C-in
16 |||  q assumption
17 |||| Np assumption
18 |||| Nq 12 K-out
19 |||| KqNq 16, 18 K-in
20 |||  p 17-19 N-out
21 ||   Cqp 16-20 C-in
22 ||   p 13, 15, 21 A-out
23 ||   Np 12 K-out
24 ||   KpNp 22, 23 K-in
25 |    NApq 13-24 N-in
26      CKNpNqNApq 12-25 C-in
27      ENApqKNpNq 11, 26 E-in


Proof of "De Morgan's" Law ENKpqANpNq

1  |    NKpq assumption
2  ||   p assumption
3  |||  q assumption
4  |||  Kpq 2, 3 K-in
5  |||  KKpqNKpq 1, 4 K-in
6  ||   Nq 3-5 N-in
7  ||   ANpNq 6 A-in
8  |    CpANpNq 2-7 C-in
9  ||   Np assumption
10 ||   ANpNq 9 A-in
11 |    CNpANpNq 9-10 C-in
12 ||   NApNp assumption
13 |||  p assumption
14 |||  ApNp 13 A-in
15 |||  KApNpNApNp 12, 14 K-in
16 ||   Np 13-15 N-in
17 ||   ApNp 16 A-in
18 ||   KApNpNApNp 17, 12 K-in
19 |    ApNp 12-18 N-out
20 |    ANpNq 8, 11, 19 A-out
21      CNKpqANpNq 1-20 C-in


And the second half:

22 |    ANpNq assumption
23 ||   Kpq assumption
24 |||  Np assumption
25 |||| q assumption
26 |||| p 23 K-out
27 |||| KpNp 26, 24 K-in
28 |||  Nq 25-27 N-in
29 ||   CNpNq 24-28 C-in
30 |||  Nq assumption
31 ||   CNqNq 30-30 C-in
32 ||   Nq 22, 29, 31 A-out
33 ||   q 23 K-out
34 ||   KqNq 32, 33 K-in
35 |    NKpq 23-34 N-in
36      CANpNqNKpq 22-35 C-in
37      ENKpqANpNq 21, 36 E-in


Proof of EKpqNANpNq:

1  |    Kpq assumption
2  ||   ANpNq assumption
3  |||  Np assumption
4  |||| q  assumption
5  |||| p 1 K-out
6  |||| KpNp 5, 3 K-in
7  |||  Nq 4-6 N-in
8  ||   CNpNq 3-7 C-in
9  |||  Nq assumption
10 ||   CNqNq 9-9 C-in
11 ||   Nq 2, 8, 10, A-out
12 ||   q 1 K-out
13 ||   KqNq 12, 11 K-in
14 |    NANpNq 2-13 N-in
15      CKpqNANpNq 1-14 C-in
16 |    NANpNq assumption
17 ||   Np assumption
18 ||   ANpNq 17 A-in
19 ||   KANpNqNANpNq 18, 16 K-in
20 |    p 17-19 N-out
21 ||   Nq assumption
22 ||   ANpNq 21 A-in
23 ||   KANpNqNANpNq 22, 16 K-in
24 |    q 21-23 N-out
25 |    Kpq 20, 24 K-in
26      CNANpNqKpq 16-25 C-in
27      EKpqNANpNq 15, 26 E-in


Proof of EApqNKNpNq:

1  |    Apq assumption
2  ||   KNpNq assumption
3  |||  p assumption
4  ||   Cpp 3-3 C-in
5  |||  q assumption
6  |||| Np assumption
7  |||| Nq 2 K-out
8  |||| KqNq 5, 7 K-in
9  |||  p 6-8 N-out
10 ||   Cqp 5-9 C-in
11 ||   p 1, 4, 10 A-out
12 ||   Np 2 K-out
13 ||   KpNp 11, 12 K-in
14 |    NKNpNq 2-13 N-in
15      CApqNKNpNq 1-14 C-in


And the second half, so to speak:

16 |    NKNpNq assumption
17 ||   NApNp assumption
18 |||  p assumption
19 |||  ApNp 18 A-in
20 |||  KApNpNApNp 19, 17 K-in
21 ||   Np 18-20 N-in
22 ||   ApNp 21 A-in
23 ||   KApNpNApNp 17, 22 K-in
24 |    ApNp 17-23 N-out
25 ||   p assumption
26 ||   Apq 25 A-in
27 |    CpApq 25-26 C-in
28 ||   Np assumption
29 |||  Nq assumption
30 |||  KNpNq 28, 29 K-in
31 |||  KKNpNqNKNpNq 30, 16 K-in
32 ||   q 29-31 N-out
33 ||   Apq 32 A-in
34 |    CNpApq 28-33 C-in
35 |    Apq 24, 27, 34 A-out
36      CNKNpNqApq 16-35 C-in
37      EApqNKNpNq 15, 36 E-in


What proofs look like for the natural deductive system you've learned, even if written in Polish notation, may well differ from the proofs above, in part because the rules of inference can differ in natural deductive systems (though I don't know of any instance of the K-out rule differing between natural deductive system, some of the rules do vary).

I'll add here that anytime you have a wff which has no scope or equivalently the wff is a theorem, if you absolutely must stick only the basic (as opposed to derived rules of inference) rules of inference of a natural deduction system, then you can put the formal proof of that wff within the scope of any other assumption. Above, some of the formal proofs have ApNp and Cpp appearing within the formal proof. If one does several proofs where one might want them or any other theorems, then one might want to prove them as theorems, and then just introduce them as theorems with the following rule of inference:

Th-in: If w1 is a theorem, then introduce w1 at any point in any proof.

So, one might write something like the following first:

 1 |  NApNp assumption
2 || p assumption
3 || ApNp 2 A-in
4 || KApNpNApNp 3, 1 K-in
5 |  Np 2-4 N-in
6 |  ApNp 1-5 A-in
7 |  KApNp 1, 6 K-in
8    ApNp 1-7 N-in


and then prove CNKNpNqApq as follows:

 1  |   NKNpNq assumption
2  |   ApNp Th-in
3  ||  p assumption
4  ||  Apq 3 A-in
5  |   CpApq 3-4 C-in
6  ||  Np assumption
7  ||| Nq assumption
8  ||| KNpNq 6, 7 K-in
9  ||| KKNpNqNKNpNq 1, 8 K-in
10 ||  q 7-9 N-out
11 ||  Apq 10 A-in
12 |   CNpApq 6-11 C-in
13 |   Apq 2, 5, 12 A-out
14     CNKNpNqApq 1-13 C-in


Now, consider the De Morgan laws. Since they're equivalences, you can use theorem-introduction to shorten proofs, because of the E-out and the C-out rules. Say you want to prove CNNNKpqANpNq.

 1  |   NNNKpq assumption
2  ||  NNKpq assumption
3  ||  KNNKpqNNNKpq 2, 1 K-in
4  |   NKpq 2-3 N-out
5  |   ENKpqANpNq Th-in
6  |   CNKpqANpNq 5 E-out
7  |   ANpNq 4, 6 C-out
8      CNNNKpqANpNq 1-7 C-in


Which gives us an 8-line proof instead of a 30 some line proof if we had to reprove ENKpqANpNq at line 5.

-