Proving non-contradiction in a natural deduction system

Question

I am stuck on a problem from Goldrei's Propositional and Predicate Calculus (p. 131):

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

(0) If $\phi\in\Gamma$ then $\Gamma\vdash_N\phi$.

(1) If $\Gamma\vdash_N\phi$ then $\Gamma_N\vdash_N(\phi\lor\psi)$

(2) If $\Gamma\vdash_N\psi$ then $\Gamma_N\vdash_N(\phi\lor\psi)$

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

(4) If $\Gamma,\phi\vdash_N\psi$ and $\Gamma,\phi\vdash_N\neg\psi$ then $\Gamma\vdash_N\neg\phi$

(5) If $\Gamma\vdash_N\neg\neg\phi$ then $\Gamma\vdash_N\phi$

Goldrei then asks several questions about this system. I'm interested in only the following:

Show that $\vdash_N(\phi\lor\neg\phi)$

I am really stuck here. My attempts so far have been to work backwards. Since I want to arrive at an empty set of assumptions ($\Gamma=\emptyset$), and since only (5) can remove negations, I figure I need to end my proof by using (4) followed by (5). In other words, if I can show that $\neg(\phi\lor\neg\phi)\vdash_N \xi$ and $\neg(\phi\lor\neg\phi)\vdash_N \neg\xi$ for some $\xi$, then an application of (4) followed by (5) gives the solution. But how to get there, I'm not at all sure.

Answer 1

Assume $\lnot (\phi \lor \lnot \phi)$.

Then assume $\phi$ and derive $(\phi \lor \lnot \phi)$ by (1).

Thus, $\lnot (\phi \lor \lnot \phi), \phi \vdash (\phi \lor \lnot \phi)$.

But also $\lnot (\phi \lor \lnot \phi), \phi \vdash \lnot (\phi \lor \lnot \phi)$.

So, applying (4): $\lnot (\phi \lor \lnot \phi) \vdash \lnot \phi$.

But $\lnot \phi \vdash \phi \lor \lnot \phi$.

Thus, $\lnot (\phi \lor \lnot \phi) \vdash \phi \lor \lnot \phi$.

From it and: $\lnot (\phi \lor \lnot \phi) \vdash \lnot (\phi \lor \lnot \phi)$, using again (4) we conclude with:

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

and the result follow by (5).