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

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.

• It's unlikely that de Morgan's law is a rule in your proof system (though it is certainly derivable). NJ is this system which you can make classical by adding one of the rules listed here. Allegedly, what Wikipedia calls $\mathrm{XM}_2$ is the one Gentzen used for NK. Alternatively, present the rules of inference that are in the system you are actually using. – Derek Elkins Jul 13 at 2:21
• @Derek Elkins Yes, the rules that is used here is NJ + XM_{2} which is what I was using as the system of NK. As you said, the de Morgan’s law here can be derived in the system of NK and I just skipped it as prior knowledge. I’ll update the post about that. The reason why I posted this is because the theorem looks fairly simple but it requires quite a lot of derivations (more than what I have expected) so I thought there might be some other solutions... – Lagomnist Jul 13 at 3:01
• I would recommend trying to find the normal form proof. It's not too difficult, though that doesn't mean it's the shortest or most intuitive proof. – Derek Elkins Jul 13 at 3:06
• @DerekElkins Could I ask what you mean by normal form proof? I think one easy way of proving this is to draw a truth table but I feel like the way I showed in the picture is nicer because it scales to larger theorems and better for my understandings (You don’t have to draw giant tables of ps and qs) – Lagomnist Jul 13 at 3:16
• Truth tables won't help you when you get to first-order logic. Also, you technically need a completeness proof, because showing that a formula is a tautology with truth tables is not the same thing as showing that it is provable. A normal form proof for NJ, is one where you never have an introduction rule for a connective immediately followed by its elimination rule, and that the only uses of the hyp rule are for atomic propositions. $\mathrm{XM}_2$ spoils things a bit, but you can still make a proof that is normal form as far as the constructive reasoning is concerned. – Derek Elkins Jul 13 at 3:41

$$\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$$.
$$\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}$$