# 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?

• How do you define $P \to Q$? – Adriano Sep 17 '14 at 22:12
• Which kind of formal proof system for propositional logic do you want to prove the equivalence in? There are several quite different ones. – Henning Makholm Sep 17 '14 at 22:35
• This is often given as the definition, although I prefer $P\implies Q\equiv \neg[P \land \neg Q]$. – Dan Christensen Sep 18 '14 at 17:27
• Possible duplicate of Equivalence of $a \rightarrow b$ and $\lnot a \vee b$ – Greek - Area 51 Proposal Nov 13 '16 at 12:22

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.
1. $P → Q$ (given)
2. $Q \lor \neg Q$ (tautology)
3. $\neg Q → \neg P$ (modus tollens)
4. from (2) and (3): $Q \lor \neg P$