Propositional logic - Natural deduction I'm stuck with a big proof in my homework. I have to use natural deduction to prove something, and I think if I can prove this somehow then I can finish the full proof. Can anyone help?
P v Q, ¬P : Q
I have to do it from first principles though, I can't use DM's laws.
I can use the following rules:
implication intro, implication elim, conjunction intro, conjunction elim, disjunction intro, disjunction elim, (double) negation elimination, negation introduction (using Reductio Ad Absurdum)
 A: The proof goes as follow:


*

*$p\lor q$ [premise]

*$p$
2.1. $\neg p$ [premise]
2.2  $\bot$ [$\rightarrow_e$ 2 and 2.1]
2.3. $q$ [absurdity rule 2.2]

*$q$
3.1. $q$ [copy 3]

*$q$ [$\lor_e$ 2 - 3.1]


I hope it is clear what I meant. Any further questions/comments?
A: You can show that $P\Rightarrow Q$ with those assumptions. You just assume $P$ and note that $\neg Q\Rightarrow P$ and $\neg Q\Rightarrow\neg P$ (via implication introduction via the assuming $\neg Q$) and conclude that $Q$.
Then you have by the implication introduction that the asssuming $P$ and that $Q$ is amoung your assumption that $P\implies Q$. But as $Q\Rightarrow Q$ also holds $Q$ follows from disjunction elimination.


*

*$P\lor Q, \neg P, P, \neg Q \vdash \neg P$

*$P\lor Q, \neg P, P \vdash \neg Q \Rightarrow \neg P$ (1+II)

*$P\lor Q, \neg P, P, \neg Q \vdash P$ 

*$P\lor Q, \neg P, P \vdash \neg Q \Rightarrow P$ (3+II)

*$P\lor Q, \neg P, P \vdash \neg\neg Q$ (2+4+NI)

*$P\lor Q, \neg P, P \vdash Q$ (5+DNE)

*$P\lor Q, \neg P \vdash P\Rightarrow Q$ (6+II)

*$P\lor Q, \neg P, Q \vdash Q$

*$P\lor Q, \neg P \vdash Q\Rightarrow Q$ (8+II)

*$P\lor Q, \neg P \vdash P\lor Q$

*$P\lor Q, \neg P \vdash Q$ (7+9+10+DE)

A: Natural deduction? If you have the choice between p and q, probably both but p is not allowed then q remain to be chosen. That is the natural argument which can be formalized: $[p\vee q]\wedge \neg p\equiv [p\wedge\neg p]\vee [\neg p\wedge q]$. There it is.
A: I use Polish notation.  The formation rules go:


*

*All lower case letters of the Latin alphabet stand as well-formed formulas.

*If $\alpha$ and $\beta$ qualify as formulas, so do A$\alpha$$\beta$, C$\alpha$$\beta$, and N$\alpha$.



assumption                        1 Apq
assumption                        2 Np
hypothesis                        3 | p
hypothesis                        4 || Nq
4, 3, 2, negation introduction    5 | NNq
5 negation elimination            6 | q
3-6 conditional introduction      7 Cpq
hypothesis                        8 | q
8-8 conditional introduction      9 Cqq
1, 7, 9 disjunction introduction 10 q


A: P ∨ Q, ~P : Q

{1}       1.   P ∨ Q                       Prem.
{2}       2.   ~P                          Prem.
{3}       3.   P                           Assum. (1. 1st Disj.)
{4}       4.   ~Q                          Assum.
{3,4}     5.   P & ~Q                      3,4 &I
{3,4}     6.   P                           5 &E
{3}       7.   ~Q → P                      3,4 CP
{2,3}     8.   ~~Q                         2,7 MT
{2,3}     9.   Q                           9 DNE (1. 1st Concl.)
{10}      10.  Q                           Assum. (1. 1st Disj.; 1st Concl.)
{1,2}     11.  Q                           1,3,9,10,10 ∨E

