Proving conjunction introduction in a natural deduction system with negation and disjunction

Question

I'm stuck solving the following problem from Goldrei's Propositional and Predicate Calculus (p. 131):

$L$ is a propositional language based on the connectives $\lnot$, $\lor$. A system $S$ for $L$ has the following (natural deduction) rules of inference:

(0) If $\phi$ $\in$ $\Gamma$ then $\Gamma \vdash \phi$

(1) If $\Gamma \vdash \phi$ then $\Gamma \vdash (\phi \lor \psi)$

(2) If $\Gamma \vdash \psi$ then $\Gamma \vdash (\phi \lor \psi)$

(3) If $\Gamma, \phi \vdash \theta$ and $\Gamma, \psi \vdash \theta$ then $\Gamma, (\phi \lor \psi) \vdash \theta$

(4) If $\Gamma, \phi \vdash \psi$ and $\Gamma, \phi \vdash \lnot \psi$ then $\Gamma \vdash \lnot \phi$

(5) If $\Gamma \vdash \lnot \lnot \phi$ then $\Gamma \vdash \phi$

Show that

$\phi, \psi \vdash \lnot (\lnot \phi \lor \lnot \psi)$

I think I need to somehow derive a contradiction and use inference rule number 4. One idea I have is to derive the disjunctive syllogism first and then assume $(\lnot \phi \lor \lnot \psi)$. But I can't seem to make any progress here either.

Answer 1

You are right. One way to approach this is by deriving a contradiction and use inference rule $(4)$. First of all, note that the inference rule $(0)$ implies that $\phi \vdash \phi$ as $\phi$ is part of the class of formulas composed solely by $\phi$. From this you can get other $\vdash$ relations. For example, $$\phi, \psi, \neg \phi \vee \neg \psi \vdash \phi.$$ So we are getting somewhere near to use inference rule $(4)$. “All” we have to do is to show that $\phi, \psi, \neg \phi \vee \neg \psi \vdash \neg \phi$ holds as well. To do this, we argue the following. Inference rule $(0)$ also allows you to conclude that $$\phi, \psi, \neg \phi \vdash \neg \phi.$$ But it also allows you to infere that $$\phi, \psi, \neg \psi, \phi \vdash \psi \quad\text{and} \quad \phi, \psi, \neg \psi, \phi \vdash \neg \psi.$$ Now, if we use inference rule $(4)$, we get $\phi, \psi, \neg \psi \vdash \neg \phi$. Hence, by inference rule $(3)$, applied to $\phi, \psi, \neg \phi \vdash \neg \phi$ and $\phi, \psi, \neg \psi \vdash \neg \phi$, we obtain $$\phi, \psi, \neg \phi \vee \neg \psi \vdash \neg \phi.$$ Therefore, since $\phi, \psi, \neg \phi \vee \neg \psi \vdash \phi$ and $\phi, \psi, \neg \phi \vee \neg \psi \vdash \neg \phi$, we conclude by inference rule $(4)$ that $$\phi, \psi \vdash \neg(\neg \phi \vee \neg \psi).$$ In this kind of proofs it may be fruitful to do what you have done: to look at where you want to get, and try to select the rules that will allow you to get there.

Answer 2

I recommend that you write it bottom-up. Then the form of the formula will guide you on what rule to apply: you just want to simplify your formula the most possible, get rid of the connectives.

---

The "then" part of your definitions of rules is usually written with a bar.

For instance

• If $\Gamma ⊢ \neg\neg\phi$ then $\Gamma ⊢ \phi$

is usually written as

$\qquad\dfrac{\Gamma\vdash\neg\neg\phi}{\Gamma\vdash\phi\phantom{\neg\neg}}$

With this in mind let's construct a tree but from bottom-up.

---

We have $\phi,\psi ⊢ \neg(\neg\phi ∨ \neg\psi)$. The only rule that makes sense to apply here is rule $(4)$. We'll use $\psi\equiv\bot$ since we know how to prove $\neg\bot$ trivially.

$\qquad\dfrac{\phi,\psi,\neg\phi\lor\neg\psi\vdash\bot\quad\phi,\psi,\neg\phi\lor\neg\psi\vdash\neg\bot}{\phi,\psi\vdash\neg(\neg\phi\lor\neg\phi)}$

If we forget the right path you may notice that what this rules tells you is that you can "move" a formula from the left of the $\vdash$ to the right of it by adding a $\neg$.

$\qquad\dfrac{\phi,\psi,\neg\phi\lor\neg\psi\vdash\bot}{\phi,\psi\vdash\neg(\neg\phi\lor\neg\phi)}$

---

Next step is clearly rule $(3)$, since it's the only one which has that "form".

$\qquad\dfrac{\dfrac{\phi,\psi,\neg\phi\vdash\bot\quad\phi,\psi,\neg\phi\vdash\bot}{\phi,\psi,\neg\phi\lor\neg\psi\vdash\bot}}{\phi,\psi\vdash\neg(\neg\phi\lor\neg\phi)}$

---

Here's a tangent. Your system is classical, meaning it has rule $(5)$, but you can deduce from it and from rule $(4)$ a rule that lets you "move" from the right of $\vdash$ to the left of it with a $\neg$, just as we did before to go from the left to the right.

$\qquad\dfrac{\Gamma\vdash\phi}{\Gamma,\neg\phi\vdash\bot}$

If you only consider this new rule instead of rule $(5)$, you get constructive logic.

---

Now applying this rule to each of the branches we get

$\qquad\dfrac{\dfrac{\phi,\psi\vdash\phi}{\phi,\psi,\neg\phi\vdash\bot}\quad\dfrac{\phi,\psi\vdash\psi}{\phi,\psi,\neg\psi\vdash\bot}}{\dfrac{\phi,\psi,\neg\phi\lor\neg\psi\vdash\bot}{\phi,\psi\vdash\neg(\neg\phi\lor\neg\psi)}}$

where now all is left to apply is rule $(1)$ to each branch.