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.

  • $\begingroup$ Yes, very good thinking so far! Now, what do you think might work for this $\xi$? $\endgroup$
    – Bram28
    May 24, 2021 at 15:12
  • $\begingroup$ @Bram28 Okay good to hear! Then the $\xi$ part is exactly where I'm stuck. $\endgroup$
    – Doubt
    May 24, 2021 at 18:05
  • $\begingroup$ Well ... this $\xi$ needs to follow from $\neg (\phi \lor \neg \phi)$ .... so what follows from $\neg (\phi \lor \neg \phi)$? (HINT: DeMorgan ...) $\endgroup$
    – Bram28
    May 24, 2021 at 18:14
  • 1
    $\begingroup$ @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! $\endgroup$
    – Bram28
    May 25, 2021 at 15:46
  • 1
    $\begingroup$ @Bram28 Awesome. Appreciate your pedagogic tack $\endgroup$
    – Doubt
    May 25, 2021 at 17:14

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


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .