2
$\begingroup$

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

  • 1
    There don't seem to be any predicates here.2013-02-16

2 Answers 2

1

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.

  • 0
    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.2013-02-16
0

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