3
$\begingroup$

We are asked to use natural deduction to prove some stuff. Problem is, without De Morgan's law, which I think belongs in transformational proof, lots of things seem difficult to prove. Would using de Morgan's laws be a violation of "In your natural deduction proofs, use only natural deduction inference rules; i.e., do not use any transformational laws."? If so, how can I work around de Morgan?

$\endgroup$
  • 7
    $\begingroup$ Can you further specify this 'natural deduction'? $\endgroup$ – Berci Jun 1 '13 at 23:32
7
$\begingroup$

The usual natural deduction introduction and elimination rules for $\land$ and $\lor$, together with the classical rules for negation allow you to derive De Morgan's laws, I.e. to show that from $\neg(\varphi \land \psi)$ you can derive $\neg\varphi \lor \neg\psi$, and vice versa, and the duals. Each of the four proofs is easy and no more than about a dozen lines [Fitch style] or the equivalent [Gentzen style]. They are routine examples, or exercises for beginners.

So it is never really harder to prove something from natural deduction first principles alone rather than from the natural deduction rules augmented with De Morgan's laws as derived rules, it is just a bit longer. Whenever you want to invoke one of De Morgan's laws, just slot in the standard proof routine using the basic natural deduction rules to derive the required instance. What's the problem?

$\endgroup$
  • $\begingroup$ don't be so patronising, this is a Q&A site, the user was clearly looking for the natural deduction proofs! $\endgroup$ – Alexandre Holden Daly May 2 '14 at 21:22
3
$\begingroup$

Eric, my advice would be to learn the transformational laws expressed natural deduction. Then, whenever you feel a transformational law is needed you can apply the natural deduction proof of said rule. For instance, here is an example of $(\lnot\phi\lor\lnot\psi) \to \lnot(\phi\land\psi)$:

$$ \frac{\displaystyle \frac{\displaystyle \lnot\phi \lor \lnot\psi \quad \frac{\displaystyle \frac{\displaystyle \frac{}{\phi\land\psi}\scriptstyle (2)} {\phi} \quad \frac{}{\lnot\phi}\scriptstyle (1)} {\bot} \quad \frac{\displaystyle \frac{\displaystyle \frac{}{\phi\land\psi}\scriptstyle(2)} {\psi} \quad \frac{}{\lnot\psi}\scriptstyle(1)} {\bot} } {\bot}\scriptstyle (1) } {\lnot(\phi\land\psi)}\scriptstyle (2) $$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.