How to prove $\neg(p\to q) \vdash p \land \neg q$ in NK/NJ?

Question

I know how to prove $\neg(p \implies q) \vdash p \land \neg q$ (look at the following picture) but I feel like there should be some simpler way to prove this (eg. without using de Morgan’s law) Any better proofs?Proof assuming NK (double negation elimination is possible)

Postscript

Here I use de Morgan’s law ( $\neg(p \land q) \vdash \neg p \lor \neg q$ ) and Disjunctive syllogism as prior knowledge (because they can be derived in the system of NK)

Looking for proofs especially in NJ, if any.

Answer 1

$$\dfrac{\dfrac{\mathcal D}{\neg(p\to q)\vdash p}\mathrm{XM}_2\qquad\dfrac{\dfrac{\dfrac{}{\neg(p\to q)\vdash\neg (p\to q)}\rlap{\mathrm{hyp}}\qquad\dfrac{\dfrac{}{p,q\vdash q}\rlap{\mathrm{hyp}}}{q\vdash p\to q}\rlap{\to I}}{\neg(p\to q),q\vdash\bot}\rlap{\neg E}}{\neg(p\to q)\vdash \neg q}\rlap{\neg I}}{\neg(p\to q)\vdash p\land\neg q}\land I$$ where $\mathcal D$ is $$\dfrac{\dfrac{\dfrac{}{\neg(p\to q)\vdash\neg(p\to q)}\mathrm{hyp}\qquad\dfrac{\dfrac{\dfrac{\dfrac{}{\neg p\vdash\neg p}\qquad\dfrac{}{p\vdash p}\rlap{\mathrm{hyp}}}{\neg p,p\vdash\bot}\rlap{\neg E}}{\neg p,p\vdash q}\rlap{\bot E}}{\neg p\vdash p\to q}\rlap{\to I}}{\neg(p\to q),\neg p\vdash \bot}\rlap{\neg E}}{\neg(p\to q)\vdash\neg\neg p}\neg I$$

Here $\neg I$ and $\neg E$ are $\to I$ and $\to E$ if $\neg P$ is defined as $P\to\bot$.

Answer 2

Your plan: Proof by RAA: assume the contrary of the conclusion to derive the contrary of the premise.

$$\dfrac{\dfrac{\dfrac{\lower{1ex}{\lnot(p\to q)}\quad\dfrac{\dfrac{\dfrac{\dfrac{\lower{1ex}{[\lnot(p\land\lnot q)]^1}\quad\dfrac{[p]^2\quad[\lnot q]^3}{p\land\lnot q}{\small\land\mathsf i}}{\bot}{\small\lnot\mathsf e}}{\lnot\lnot q}{\small\lnot\mathsf i^3}}{q}{\small\lnot\lnot\mathsf e}}{p\to q}{\small\to\mathsf i^2}}{\bot}{\small\lnot\mathsf e}}{\lnot\lnot(p\land\lnot q)}{\small\lnot\mathsf i^1}}{p\land\lnot q}{\small\lnot\lnot\mathsf e}$$

---

Alternatively: conjoin two subproofs of $p$ and $\lnot q$.

$$\dfrac{\dfrac{\dfrac{\dfrac{\lower{1.5ex}{\lnot(p\to q)}~~\dfrac{\dfrac{\dfrac{[\lnot p]^1\quad[p]^2}{\bot}{\small\lnot\mathsf e}}{q}{\small\mathsf{efq}}}{p\to q}{\small\to\!\mathsf i^2}}{\bot}{\small\lnot\mathsf e}}{\lnot\lnot p}{\small\lnot\mathsf i^1}}{p}{\small\lnot\lnot\mathsf e}\quad\dfrac{\dfrac{\lower{1.5ex}{\lnot(p\to q)}~~{\dfrac{[q]^3\quad[p]^4}{p\to q}{\small\to\!\mathsf i^4}}}{\bot}{\small\lnot\mathsf e}}{\lnot q}{\small\lnot\mathsf i^3}}{p\land\lnot q}{\small\small\land\mathsf i}$$