Prove $(P\to Q) \lor (Q\to P)$

Question

Prove that $(P\to Q) \lor (Q\to P)$

In natural language, it reads as: if $P$ then $Q$, or if $Q$ then $P$

Answer 1

I think the basic idea is this: \begin{align} (P \to Q) \lor (Q \to P) &\equiv (\neg P \lor Q) \lor (\neg Q \lor P) \\ &\equiv (\neg P \lor P) \lor (\neg Q \lor Q) \\ &\equiv \sf{T} \lor \sf{T} \\ &\equiv \sf{T}. \end{align} (Sorry about the notation; I hope that it can be understood).

In the first part use the logic indentity (or rule) \begin{align} (P \to Q) &\equiv (\neg P \lor Q) \end{align} to obtain the right side of the equivalence,
Then is just reordening the terms (beacuse they are all $\lor$) and finally use : \begin{align} (P \lor -P) &\equiv \sf{T} \end{align}

Answer 2

The comments indicate that a proof using natural deduction is desired, so I'll give some hints about how to do it that way (I won't give a complete formal proof because to be honest I am not very familiar with natural deduction.)

There are only two ways to derive a disjunction that I am aware of: by deriving one of the disjuncts, or by using the law of excluded middle. Neither of the disjuncts is true in general, so we have to use the law of excluded middle. This gives us $(P \to Q) \vee \neg(P \to Q)$. Then we can reduce the problem to deriving $Q \to P$ from $\neg(P \to Q)$.

Assume $\neg(P \to Q)$. To derive the implication $Q \to P$, we assume the antecedent $Q$ and derive the consequent $P$. So assume $Q$. Then we can derive the implication $P \to Q$. But this contradicts our assumption. From the contradiction we can derive $P$.

Answer 3

$P \to Q$ is false only when P is true and Q is false. But, in that case $Q \to P$ is true. So $(P\to Q) \lor (Q\to P)$ is always true.

Answer 4

Disclaimer: this answer is for fun and to demonstrate yet another method of proving your formula. It assumes basic familiarity with typed $\lambda$-calculus, so if you don't know what it is, just ignore this post.

---

To prove in classical logic

$$(P \to Q) \lor (Q \to P)$$

we could use double-negation elimination/introduction

$$ \neg \neg P \equiv P$$

and somehow prove $$ \neg \neg ((P \to \neg \neg Q) \lor (Q \to \neg \neg P)). \tag{1} $$

Let's assume that

$$A \lor B \equiv \mathtt{Left} A \mid \mathtt{Right} B$$

and

$$\neg A \equiv A \to \bot,$$

then the inhabitant of

$$ \Big(\Big((P \to (Q \to \bot) \to \bot) \lor (Q \to (P \to \bot) \to \bot)\Big) \to \bot \Big) \to \bot $$

is

$$\lambda k_0.\ k_0\big( \mathtt{Left}\ \lambda p.\ \lambda k_L.\ k_0 (\mathtt{Right}\ \lambda q.\ \lambda k_R.\ k_R\ p) \big)$$

and this proves $(1)$ by Curry-Howard isomorphism.

Have fun!

Answer 5

In Polish notation ((P -> Q) $\lor$ (Q -> P)) corresponds to ACpqCqp. The system I'll use has the following rules of inference. The rules are not independent. I will also use a rule of inference outside the scope of a hypothesis to get discharged or an assumption still in effect, and thus it may get questioned if the following works in the spirit of natural deductive proofs on two counts, though I believe that St. Jaskowski at least would not object to the last two steps:

C-in: From $\alpha$ $\vdash$$\beta$ we may infer C$\alpha$$\beta$ provided that $\alpha$ and $\beta$ have the same scope, and $\alpha$ is a hypothesis. The right column of the proof analysis will help keep track of which hypotheses are still in effect.

For all the other rules I'll write Q $\vdash$ P where Q is a set of wffs such that each member of Q is under the scope of hypotheses still in effect.

A-in-left: {$\alpha$} $\vdash$ A$\alpha$$\beta$

K-in: {$\alpha$, $\beta$} $\vdash$ K$\alpha$$\beta$

N-in: {C$\alpha$K$\beta$N$\beta$} $\vdash$ N$\alpha$

N-out: {CN$\alpha$K$\beta$N$\beta$} $\vdash$ $\alpha$

K-out left: {K$\alpha$$\beta$} $\vdash$ $\alpha$

A-in-right: {$\alpha$} $\vdash$ A$\beta$$\alpha$

                                     Hypotheses still in effect
hypothesis     1 | NACpqCqp                       1
hypothesis     2 || Cpq                           1, 2
A-in left 2    3 || ACpqCqp                       1, 2
K-in 3, 1      4 || KACpqCqpNACpqCqp              1, 2
Ci 2-4         5 | CCpqKACpqCqpNACpqCqp           1, 2
N-in, 5        6 | NCpq                           1
hypothesis     7 || Np                            1, 7
hypothesis     8 ||| p                            1, 7, 8
hypothesis     9 |||| Nq                          1, 7, 8, 9
K-in 8, 7     10 |||| KpNp                        1, 7, 8, 9
C-in 9-10     11 ||| CNqKpNp                      1, 7, 8
N-out 11      12 ||| q                            1, 7, 8
8-12 Ci       13 || Cpq                           1, 7
K-in 13, 6    14 || KCpqNCpq                      1, 7
7-14 Ci       15 | CNpKCpqNCpq                    1
N-out 15      16 | p                              1
hypothesis    17 || q                             1, 17
K-in 16, 17   18 || Kpq                           1, 17
K-out-left 18 19 || p                             1, 17
Ci 17-19      20 | Cqp                            1
hypothesis    21 || Cqp                           1, 21
A-in right    22 || ACpqCqp                       1, 21
K-in 22, 1    23 || KACpqCqpNACpqCqp              1, 21
Ci 21-23      24 | CCqpKACpqCqpNACpqCqp           1
N-in          25 | NCqp                           1
K-in 20, 25   26 | KCqpNCqp                       1
Ci 1-26       27 CNACpqCqpKCqpNCqp                None   
27 N-out      28 ACpqCqp                          None

Answer 6

One way to approach a proof like this is with Boolean Identities. You can find a list of them at What are a list of helpful boolean identities for solving boolean functions?. I strongly suggest that you familiarize yourself with these as they prove indispensable for manipulating Boolean expressions.