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

  • $\begingroup$ 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. $\endgroup$ – lemontree Apr 15 at 10:47
  • $\begingroup$ @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. $\endgroup$ – amoogae Apr 15 at 11:37
  • $\begingroup$ If you have the DeMorgan laws as derivable biimplications, sure, that works. I just thought you might be confusing syntax with semantics. $\endgroup$ – lemontree Apr 15 at 13:30

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

enter image description here

enter image description here

enter image description here


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)


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.