De Morgan's laws in natural deduction? 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?

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 $\
eg(\varphi \land \psi)$ you can derive $\
eg\varphi \lor \
eg\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?