# How to prove $C$ from $A \leftrightarrow (B \leftrightarrow C)$ and $A \leftrightarrow B$?

How does one prove $C$ from the premises: $A \leftrightarrow (B \leftrightarrow C)$ and $A \leftrightarrow B$ ?

I've tried to prove $C$ by contradiction, using a sub-proof which presumes $\neg C$, but although I can conclude all of the following in the subproof: $\neg A$, $\neg B$, $\neg (B \leftrightarrow C)$, I'm unable to find a contradiction this way.

I've been stuck on this for the whole day, and I think I might be over-thinking the problem.

Note: I want to prove this using the basic first-order logic rules (I'm using the First-Order Logic from the Language, Proof and Logic book).

• There are several 'basic FOL rules'. I take it you're using the ones from the LPL book because you mentioned it in this question. If this is the case, then I suggest you instead say it's the rules from this book. – Git Gud Sep 20 '14 at 18:34
• You are indeed correct. I did not know that there were so many different kinds of FOL basics. I have appended it in the question. – Qqwy Sep 20 '14 at 18:49
• I would try proving that ((A↔(B↔C))$\rightarrow$((A↔B)↔C)) first. I could put up an answer a proof in a different natural deduction system than yours if you'd like. The system I refer to has no negation introduction rule. – Doug Spoonwood Sep 20 '14 at 21:43

Due to the transitivity of $\leftrightarrow$ and due to the fact that $A$ comes up on both premises 'at the same level', I find it natural to focus on $A$ and let it act as a pivot of sorts.

Start by proving $A\lor \neg A$ and perform $\lor$-$\text{Elim}$ on this disjunction.

In the first case just use $\leftrightarrow$-$\text{Elim}$ successively on the premises to get $C$.

In the second case (where one starts a subproof with the premise $\neg A$), use the premise $A\leftrightarrow B$ to get $\neg B$ and the premise $A\leftrightarrow (B \leftrightarrow C)$ to get $\neg(B\leftrightarrow C)$ (in both cases by negation introduction).
Now assume $\neg C$, prove $\neg B\leftrightarrow \neg C$ and from this last statement get $B\leftrightarrow C$.
At this point you can find a contradiction allowing you to conclude $C$ in the subproof whose premise is $\neg A$.

I leave the proof below.

• The software that comes with the book doesn't seem to deal well with big proofs.This was the best possible presentation I could get. One can note that in justification of the steps there are some missing steps, the software itself did that. – Git Gud Sep 20 '14 at 22:18

This basically follows from the associativity of $\leftrightarrow$. But let's pretend that we didn't know that.

We consider two exhaustive, mutually exclusive cases.

Case 1: Suppose that $B$ is true. Then since $A \leftrightarrow B$ is true, we know that $A$ is true. Thus, since $A \leftrightarrow (B \leftrightarrow C)$ is true, we know that $B \leftrightarrow C$ is true. But then since $B$ is true, we know that $C$ is true, as desired.

Case 2: Suppose that $B$ is false. Then since $A \leftrightarrow B$ is true, we know that $A$ is false. Thus, since $A \leftrightarrow (B \leftrightarrow C)$ is true, we know that $B \leftrightarrow C$ is false. But then since $B$ is false, we know that $C$ is true (otherwise, if $C$ was actually false, then $B \leftrightarrow C$ would be true, a contradiction). So we're done!

• Thanks a lot! The only thing I still am having trouble with is how conclude $C$ from $\neg (B \leftrightarrow C)$ and $\neg B$ – Qqwy Sep 20 '14 at 20:33
• Use a proof by contradiction. Suppose instead that $C$ is actually false. Now since $\neg B$ is true, we know that $B$ is false. But then since $B$ and $C$ are both false, we know that $B \leftrightarrow C$ is true. But this contradicts the fact that $\neg(B \leftrightarrow C)$ is true. – Adriano Sep 20 '14 at 20:41
• It is unfortunate that I cannot mark two answers as accepted. This answer was enough for me to arrive at a conclusion. However, I did mark Git Gud's answer because other people who stumble across the same problem might have more use for the complete proof themselves. – Qqwy Sep 21 '14 at 0:31

\newcommand{\calc}{\begin{align} \quad &} \newcommand{\calcop}[2]{\\ #1 \quad & \quad \text{"#2"} \\ \quad & } \newcommand{\endcalc}{\end{align}}Your proof by contradiction approach is fine, here is how you can complete your proof.

Assume $\;C\;$ is false, then $$\calc A \leftrightarrow (B \leftrightarrow C) \calcop{\leftrightarrow}{using what we know about \;C\;} A \leftrightarrow (B \leftrightarrow \text{false}) \calcop{\leftrightarrow}{left hand side: use \;A \leftrightarrow B\;; right hand side: simplify} B \leftrightarrow \lnot B \calcop{\leftrightarrow}{logic} \text{false} \endcalc$$

which is a contradiction. Therefore $\;C\;$ is true.

I would use the algebraic machinery:

$A\leftrightarrow B\quad$ iff $\quad 1\oplus A\oplus B$

and get $(A\leftrightarrow (B\leftrightarrow C))\wedge (A\leftrightarrow B)\quad$ iff $\quad (1\oplus A\oplus 1\oplus B\oplus C)(1\oplus A\oplus B)=$ $=(A\oplus B\oplus C)(1\oplus A\oplus B)$ $=A\oplus B\oplus C\oplus A\oplus AB\oplus AC\oplus AB\oplus B\oplus BC=$ $=C\oplus AC\oplus BC=C(1\oplus A\oplus B)\quad$ iff $\quad C\wedge(A\leftrightarrow B)$, which imply C.

Which considering the note may not be as relevant, but...