# Proving non-contradiction in a natural deduction system

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$$

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.

• Yes, very good thinking so far! Now, what do you think might work for this $\xi$? May 24, 2021 at 15:12
• @Bram28 Okay good to hear! Then the $\xi$ part is exactly where I'm stuck. May 24, 2021 at 18:05
• Well ... this $\xi$ needs to follow from $\neg (\phi \lor \neg \phi)$ .... so what follows from $\neg (\phi \lor \neg \phi)$? (HINT: DeMorgan ...) May 24, 2021 at 18:14
• @Doubt Right! DeMorgan is not a rule ... but it was my hint to get you thinking on what this $\xi$ would be. That is, since $\neg(\phi \lor \neg \phi)$ is equivalent to $\neg \phi \land \neg \neg \phi$, I was hoping you would have realized that $\neg \phi$ would have been a perfect pick for this $\xi$. And I didn;t want to give the proof itself .. I wanted you to think about this ... that's the only way to get better at this! May 25, 2021 at 15:46
• @Bram28 Awesome. Appreciate your pedagogic tack May 25, 2021 at 17:14

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).