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

Question

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..

Answer 1

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

Answer 2

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].

Answer 3

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)