# Propositional Logic Proof of $\vdash \lnot (p \supset q) \supset (p \land \lnot q)$

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

-
Your guess that it is not intuitionistically valid is right -- proving $\vdash \neg\neg p \supset p$ from it is an easy exercise. What exactly do you mean by "natural logic" -- the same as natural deduction? If so, an answer will depend on your precise axioms: there are various equivalent ways to introduce classical reasoning in ND, and without knowing which one you're using it is hard to give a relevant hint. – Henning Makholm Nov 15 '11 at 0:44
There don't seem to be any predicates here. – Chris Eagle Feb 16 '13 at 10:21

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.

-
Drat, after all the $\LaTeX$ing, just noticed the original question was a very old one ... sigh. Ah well, I suppose someone sometime might find it useful. – Peter Smith Feb 16 '13 at 16:27

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

-