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..
 A: 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].
A: Here is a proof in a Fitch-style natural deduction proof:



A: 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) 
