How to prove that $P \rightarrow Q$ is equivalent with $\neg P \lor Q $? In my book about Logic, which is called 'Language, Proof and Logic', by the way, there is explained that the conditional $ P \rightarrow Q $ is equivalent with $\neg P \lor Q$.
There is another answer on math.stackexchange that gives as answer: 'just compare the truth tables and you can see that they are equivalent'. However, I would like to know how to prove this using formal propositional logic. This should be possible, right?
 A: Layout:
To prove that $\neg P\lor Q$ is a formal consequence of $P\to Q$, start by assuming $P\to Q$ and further suppose that $\neg (\neg P\lor Q)$ holds. At this point you should prove $P\lor \neg P$ and perform $\lor$-$\text{Elim}$ on this disjunction. It's easy to find contradictions on both cases yielding $\neg \neg (\neg P\lor Q)$.
For the other direction, naturally start by assuming that $\neg P\lor Q$ holds and then assume $P$. Now start yet another subproof (within the assumption that $P$ holds) assuming that $\neg Q$ holds. At this point perform $\lor$-$\text{Elim}$ on the assumption $\neg P\lor Q$. It's easy to find a contradiction in this last subproof.
A: *

*$P → Q$ (given)

*$Q \lor \neg Q$ (tautology)

*$\neg Q → \neg P$ (contrapositive of (1) )

*from (2) and (3): $Q \lor \neg P$ (modus ponens)
A: You may translate the two expressions using sheffer's stroke, symbol : | 


*

*X | Y means , by definition ~ ( X & Y) 

*X --> Y means ~ ( X & ~ Y) and, hence : X | ~Y 

*X v Y means ~ ( ~X & ~Y) , hence : ~X | ~Y 
Now, let ~P play the role of X and Q play the role of Y. 


*

*~P v Q means (~ ~ P | ~Q), that is : ( P | ~Q) , using double negation. 


Let P play the role of X and Q play the role of Y. 


*

*( P --> Q) means ( P | ~Q).
The sheffer's stroke translation shows that the two formulas mean exactly the same thing; hence they are equivalent. 
