0

I'm working on this: $$\dashv \lnot P \to \ (( P \to\ \lnot Q)\to\lnot P) $$

So I did this :

$1\ assume \ \lnot p.\\ 2 \ assume \ p \to \lnot q.\\ 3 \ therefore \ (p \to \lnot q)\to \lnot p. \ (\to)I 2,1\\ 4 \ therefore \ \lnot p \to \ (p \to \lnot q)\to \lnot p. (\to)I 1,3$

And now tree proof,is it good?

\begin{align} \cfrac{\cfrac {\cfrac{[\lnot p]^1}{[p\to \lnot q]^1} }{(p\to\lnot q )\to \lnot p } (\to)\text {I}} {\lnot p \to((p\to\lnot q )\to \lnot p)} (\to) \text {I} \end{align}

user61589
  • 139
  • 5
  • Start with $\neg p$ on top – Bram28 Feb 07 '17 at 21:03
  • @Bram28 ok it was my error, but it is right? – user61589 Feb 07 '17 at 21:32
  • OK, I still don;t know the exact rules, but looking at it intuitively, I would think that since $p \to \neg q$ is an assumption, that that should not go under the $\neg p$, but rather to the side of it. Then when you do the first $\to I$, you 'use' the $p \to \neg q$ (so that gets index 1), and when you do the second $\to I$, you use the $\neg p$ (so that should get a 2. And maybe use these indices also with the rules so you know what goes with what. – Bram28 Feb 07 '17 at 21:42
  • I put how I think it is in my Answer. – Bram28 Feb 07 '17 at 21:46

1 Answers1

1

So more like this ...

\begin{align} \cfrac{\cfrac {[\lnot p]^2 \: [p\to \lnot q]^1 }{(p\to\lnot q )\to \lnot p } (\to)\text {I}^1} {\lnot p \to((p\to\lnot q )\to \lnot p)} (\to) \text {I}^2 \end{align}

Bram28
  • 100,612
  • 6
  • 70
  • 118