Prove that $\lnot (p \implies q)$ is equivalent to $p \land \lnot q$? By equivalent I mean the biconditional, as in
$$\lnot (p \implies  q) \iff p \land \lnot q$$

Given the definition of implication, I understand why this is true, but I need a bit of help showing this with a formal proof using rules like $\lor-\text{Elim}$  and $\bot-\text{Intro}$.
Here is the pure natural deduction proof (Fitch-Style).



If $p \land \neg q$:

&emsp; $p$;

&emsp; $\neg q$.

&emsp; If $p \to q$:

&emsp; &emsp; ...

&emsp; &emsp; $\bot$.

&emsp; $\neg( p \to q )$.

If $\neg( p \to q )$:

&emsp; If $\neg p$:

&emsp; &emsp; If $p$:

&emsp; &emsp; &emsp; $\bot$.

&emsp; &emsp; &emsp; $q$.

&emsp; &emsp; $p \to q$.

&emsp; &emsp; $\bot$.

&emsp; $\neg \neg p$.

&emsp; $p$.

&emsp; If $q$:

&emsp; &emsp; ...

&emsp; &emsp; $p \to q$.

&emsp; &emsp; $\bot$.

&emsp; $\neg q$.

&emsp; $p \land \neg q$.

$p \land \neg q \leftrightarrow \neg( p \to q )$.



I'll leave you to fill in the blanks, which should be easy. See this post for a brief description of the general method to discovering such a proof. Sometimes it can be convenient to use LEM (law of excluded middle) to split cases in a clever manner to shorten the proof, but that way requires some experience.

As for the interesting side question of whether or not one can prove the equivalence in intuitionistic logic, which has the same inference rules except without DNE (double negation elimination), and hence LEM does not hold, the answer is that indeed it cannot be done. Note that the above proof only uses DNE once. Feel free to ignore the rest of this post if you are not interested in intuitionistic logic.

In intuitionistic logic, "$\neg p$" is simply a short-form for "$p \to \bot$". To prove that some sentence is not provable in intuitionistic logic, it suffices to construct a Kripke frame that does not satisfy it (see this post). Consider the Kripke frame $0 \to 1$ where $p$ is known only at $1$ and $q$ is not known at both $0,1$. Then $\neg( p \to q )$, which denotes $( p \to q ) \to \bot$, is known everywhere, but $p \land \neg q$ is not known at $0$.

Alternatively, note that if it were provable in intuitionistic logic, it would hold when $q = \bot$, but that gives $\neg( p \to \bot ) \to p \land ( \neg \bot )$, which is equivalent (by definition) to $\neg \neg p \to p$, which is not valid in intuitionistic logic.
The OP is looking for the following:


  Given the definition of implication, I understand why this is true, but I need a bit of help showing this with a formal proof using rules like ∨−Elim and ⊥−Intro.


The following proof uses disjunction elimination ("∨−Elim" or "vE") on line 20 and negation introduction ("⊥−Intro" or "⊥I") on lines 6 and 21.

 

For a description of the justification used see the text forallx and the associated proof checker referenced below.



Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/