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

  • 1
    $\begingroup$ 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. $\endgroup$ – Git Gud Sep 20 '14 at 18:34
  • $\begingroup$ 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. $\endgroup$ – Qqwy Sep 20 '14 at 18:49
  • $\begingroup$ 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. $\endgroup$ – 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.

Formal proof

  • 1
    $\begingroup$ 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. $\endgroup$ – 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!

  • $\begingroup$ Thanks a lot! The only thing I still am having trouble with is how conclude $C$ from $\neg (B \leftrightarrow C)$ and $\neg B$ $\endgroup$ – Qqwy Sep 20 '14 at 20:33
  • 1
    $\begingroup$ 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. $\endgroup$ – Adriano Sep 20 '14 at 20:41
  • $\begingroup$ 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. $\endgroup$ – 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...


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.