# Prove $\vdash (A_1 ↔ A_2) \vee (A_2 ↔ A_3) \vee (A_3 ↔ A_1)$ using natural deduction.

I think this is true. Because by the pigeon hole principle, Two of $$A_1, A_2, A_3$$ must have the same true value. But I have no idea how to prove it.. Can somebody help me?

Of course, we can use well-known logical laws. For example De Morgan, law of the excluded middle..

• You can not use DeMorgan to prove $\vdash$ (unless there is a rule in your natural deduction system that has the form of the DeMorgan law, which is usually not the case). $\vdash \phi$ means "$\phi$ is derivable in some formal system", e.g. natural deduction. The DeMorgan laws, on the other hand, are logical equivalences (statements of the form $\phi \equiv \psi$), which talk about truth under an assignment function. $\vdash$ is not the same as $\vDash$. If you are supposed to show $\vdash$, you have to use the rules of natural deduction. – lemontree Apr 15 at 10:47
• @lemontree Since we have already proved De Morgan laws $\vdash \neg (\alpha_1\vee \alpha_2) ↔ \neg \alpha_1\wedge \neg \alpha_2$ for all wff $\alpha_1, \alpha_2$, I think we can use it without repeating the proof. So, I think If we got the proof of $\vdash \neg (\alpha_1\vee \alpha_2)$, we can get $\vdash \neg \alpha_1\wedge \neg \alpha_2$ by modus ponens. Of course, if we follow the definition of natural deduction rigorously, this is wrong, but if we do so, I think this proof seems very long... If I misunderstand something, please let me know. – amoogae Apr 15 at 11:37
• If you have the DeMorgan laws as derivable biimplications, sure, that works. I just thought you might be confusing syntax with semantics. – lemontree Apr 15 at 13:30

Here is a proof in a Fitch-style natural deduction proof:

Long comment

I think that the proof is quite long: we can try with a simpler (but similar) example :

$$\vdash (A_1 \to A_2) \lor (A_2 \to A_3) \lor (A_3 \to A_1)$$.

In this case, the proof is straightforward, using EM :

1) $$\vdash A_1 \lor \lnot A_1$$

2) $$A_1$$ --- assumed [a] for $$\lor$$-elim

3) $$A_3 \to A_1$$ --- from 2) by $$\to$$-intro

4) $$(A_2 \to A_3) \lor (A_3 \to A_1)$$ --- from 3) by $$\lor$$-intro

5) $$(A_1 \to A_2) \lor (A_2 \to A_3) \lor (A_3 \to A_1)$$ --- from 4) by $$\lor$$-intro

6) $$\lnot A_1$$ --- assumed [b] for $$\lor$$-elim

7) $$A_1$$ --- assumed [c]

8) $$A_2$$ --- from 6) and 7)

9) $$A_1 \to A_2$$ --- from 7) and 8) by $$\to$$-intro, discharging [c]

10) $$(A_1 \to A_2) \lor (A_2 \to A_3)$$ --- from 9) by $$\lor$$-intro

11) $$(A_1 \to A_2) \lor (A_2 \to A_3) \lor (A_3 \to A_1)$$ --- from 10) by $$\lor$$-intro

Now we can conclude by $$\lor$$-elim from 1), discharging [a] and [b].

I think one can take advantage of the fact that the operators <-> (biconditionnal) and " w " ( X-OR, exclusive or ) are, so to say, the "negation" of each other , in the same manner as & and NAND ( Which can be checked using truth tables).

I'll use the following facts ( which can be proved with natural deduction, except maybe the first part of fact 1 , that is linked to the associativity of disjunction; this extremely basic fact might require a semantic method, I do not know).

(1) (AvBvC) is equivalent to (AvB)v C , which in turn is equivalent to
(~ (AvB) --> C )

(2) [ replacement rule ] from ~(A <--> B) infer ( AwB) , and reciprocally ( with " w" meaning " exclusive or" )

(3) [ w elim 1 ]from (AwB) and A, infer ~B / from (AwB) and B, infer ~A

(4) [ w elim 2 ] from (AwB) and ~A infer B / from (AwB) and ~B infer A

(5) [<-> Intro ] From (A --> B) and (B -->A) infer( A <--> B) [ <-> Intro ]

Strategy :

Fact (1) means that, in order to prove (A1<->A2) v (A2<->A3) v (A3<->A1)

we only have to prove that : ~ ( (A1<->A2) v (A2<->A3) ) --> (A3<->A1) , which makes of conditional proof a possible strategy.

Proof :

Now, suppose ( for conditional proof) that you have :

~ ( (A1<->A2) v (A2<->A3) ).

By DeMorgan's law, infer from that :

~ (A1<->A2) & ~ (A2<->A3).

Eliminate & to get

~ (A1<->A2)

~ (A2<->A3).

Use fact (2) - that is : ~ (A <->B) iff (AwB) - to get :

(A1 w A2)

(A2 w A3)

Now, suppose ( for conditional proof inside our main conditional proof) you have A1.

Using fact (3) infer from A1 that : ~ A2. And, using fact (4), infer from ~ A2 that A3 is true. You have shown that :

                               IF A1 THEN A3


In the same way, suppose ( for conditional proof, still inside the main conditional proof) that you have A3.

Using fact (3), infer that A2 is false. And using fact (4), infer from ~A2 that A1 is true. You have shown that :

                                  IF A3 THEN A1


Now , using the fact (5) ( that is <--> Intro) infer from (A1 --> A3) and (A3 --> A1) that

                                     **A1 <--> A3**


Under our main assumption : ~ ( (A1<->A2) v (A2<->A3) ), we have shown : A1 <--> A3.

The conditional proof rule allows us to derive from this that :

         ~  ( (A1<->A2) v (A2<->A3) ) --> A1 <--> A3


But , by fact (1) we know that this is equivalent to :

            ( (A1<->A2) v (A2<->A3) ) v  (A1 <--> A3)  ,


and finally to our goal :

               (A1<->A2) v (A2<->A3)  v  (A3 <--> A1)


( knowing that the <-> operator is commutative)