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.

$\endgroup$
2
  • 6
    $\begingroup$ 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. $\endgroup$ Nov 15 '11 at 0:44
  • 1
    $\begingroup$ There don't seem to be any predicates here. $\endgroup$ Feb 16 '13 at 10:21
1
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$ Feb 16 '13 at 16:27
0
$\begingroup$

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.