$\vdash \lnot (p \supset q) \supset (p \land \lnot q)$
I need to prove the above proposition via intuitionistic logic rules and/or natural logic rules. I guess it is not possible to prove with intuitionistic logic becuase we cannot use PBC rule.
$\vdash \lnot (p \supset q) \supset (p \land \lnot q)$
I need to prove the above proposition via intuitionistic logic rules and/or natural logic rules. I guess it is not possible to prove with intuitionistic logic becuase we cannot use PBC rule.
It is evidently enough to prove (i) $\neg(p \supset q) \vdash p$ and (ii) $\neg(p \supset q) \vdash \neg q$. And plainly we can't get the target result if we can't prove those (assuming $\land$-elimination and modus ponens are available).
But note (i) is inuitionistically invalid, so we indeed do need to be working in a classical framework. (Given (i), we'd have in particular $\neg(p \supset \bot) \vdash p$, i.e. $\neg\neg p \vdash p$, as Henning Makholm remarked.)
For (i) a proof with a standard set of ND rules for the conditional and classical negation would go
$\begin{array}{cccccccl} 1 & \neg(p \supset q) & & & & & & premiss\\ 2 & & | & \neg p & & & & assumption\\ 3 & & | & & | & p & & assumption\\ 4 & & | & & | & \bot & & from\ 2, 3\\ 5 & & | & & | & q & & from\ 4\\ 6 & & | & (p \supset q) & & & & from\ 3-5\\ 7 & & | & \bot & & & & from\ 1, 6\\ 8 & \neg\neg p & & & & & & from\ 2-7\\ 9 & p & & & & & & from\ 8, DN\\ \end{array} $ Note the use of the intuitionistically unwarranted step at the last line.
For (ii) we can argue
$\begin{array}{cccccccl} 1 & \neg(p \supset q) & & & & & & premiss\\ 2 & & | & q & & & & assumption\\ 3 & & | & & | & p & & assumption\\ 4 & & | & & | & q & & from\ 2, reit\\ 5 & & | & (p \supset q) & & & & from\ 3-4\\ 6 & & | & \bot & & & & from\ 1, 5\\ 7 & \neg q & & & & & & from\ 2-6 \end{array} $
Obviously, with a different set of classical ND rules, the proofs will have to go differently but similarly, mutatis mutandis.
My proof strategy basically assumes the negation of each part of the conjunction in turn, shows that each part leads to a contradiction, then conjuncts the results.
With the rules of conditional introduction (Ci), conditional elimination (Co), conjunction introduction (Ki), negation introduction (Ni) as "if we have a derivation starting with p, and we derive a contradiction, we may infer Np, the negation of p.", and negation elimination (No) "if we have a derivation starting with Np, and we derive a contradiction, we may infer p." a possible proof (in Polish notation which helps identify the type of wff you have, which can help when thinking of proof techniques) goes as follows:
1 | NCpq hypothesis 2 || Np hypothesis 3 ||| p hypothesis 4 |||| Nq hypothesis 5 |||| KpNp 2, 3 Ki 6 ||| q 4-5 No 7 || Cpq 2-6 Ci 8 || KCpqNCpq 1, 7 Ki 9 | p 2-8 No 10 || q hypothesis 11 ||| p hypothesis 12 |||| q hypothesis 13 ||| Cqq 12-12 Ci 14 ||| q 10, 13 Co 15 || Cpq 11-14 Ci 16 || KCpqNCpq 15, 1 Ki 17 | Nq 10-16 Ni 18 | KpNq 9, 17 Ki 19 CNCpqKpNq 1-18 Ci