Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

share|improve this question
6  
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
    
please add homework tag if this is homework/assignment. –  Kaveh Nov 19 '11 at 18:04
1  
There don't seem to be any predicates here. –  Chris Eagle Feb 16 '13 at 10:21

2 Answers 2

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.

share|improve this answer
    
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
share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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