3

I am working on a proof where I was able to derive this general form:

~(a ↔ b)

From this I would like to obtain:

a ↔ ~b

I have made sure that the two statements are equivalent by drawing out truth-tables. The problem is that I am not really sure how to go from the first statement to the second statement in Fitch.

If it helps in answering the question, the specific proof I am working on is LPL's Exercise 8.50. It is the following: 

1.| Cube(b) ↔ (Cube(a) ↔ Cube(c))
2.| | Dodec(b)                            (assumption)
3.| | | Cube(a)↔Cube(c)                   (assumption)
4.| | | Cube(b)                           ↔Elim 1, 3
5.| | | ⊥                                 AnaCon 2, 4
6.| | ~(Cube(a)↔Cube(c))                  ~Intro 3-5
∴ Dodec(b) → (Cube(a) ↔ ¬Cube(c))

Lines 2-6 are my work. I know that this argument is valid because if b was anything besides a cube (a dodec or a tet), then if Cube(a), it would necessarily follow that ~Cube(c) and vice versa, because if Cube(a) implied Cube(c) or vice versa, it would necessitate that b would have to be a cube.

Matt
  • 67

2 Answers2

1

0) $\lnot (a \leftrightarrow b)$ --- premise

1) $a$ --- assumed [a]

2) $b \to a$ --- from 1) by $\to$-intro

3) $b$ --- assumed [b]

4) $a \to b$ --- from 3) by $\to$-intro

5) $a \leftrightarrow b$ --- from 2) and 4)

6) $\bot$ --- from 0) and 5)

7) $\lnot b$ --- from 1) and 6) by $\lnot$-intro, discharging [b]

8) $a \to \lnot b$ --- from 1) and 7) by $\to$-intro, discharging [a].

9) $\lnot b$ --- assumed [c]

10) $b$ --- assumed [d]

11) $\bot$ --- from 9) and 10)

12) $a$ --- from 11)

13) $b \to a$ --- from 10) and 12) by $\to$-intro, discharging [d]

14) $\lnot a$ --- assumed [e]

15) $a$ --- assumed [f]

16) $\bot$ --- from 14) and 15)

17) $b$ --- from 16)

18) $a \to b$ --- from 15) and 17) by $\to$-intro, discharging [f]

19) $a \leftrightarrow b$ --- from 13) and 18)

20) $\bot$ --- from 0) and 19)

21) $a$ --- from 14) and 20) by Double Negation, discharging [e]

22) $\lnot b \to a$ --- from 9) and 21) by $\to$-intro, discharging [c]

23) $a \leftrightarrow \lnot b$ --- from 8) and 22).

Mauro ALLEGRANZA
  • 94,169
  • In step 2, how did you obtain b → a from step 1? Step 1 was just a. From my understanding, →Intro requires us to make a subproof beginning with the antecedent and ending with the consequent. – Matt May 29 '17 at 22:56
  • @Matt - by $\to$-intro; intuitively (by truth table for conditionals) if $a$ is true also $b \to a$ is true, for $b$ whatever. More "formally": assume $b$, assume $a$, by $\to$-intro derive $b \to a$ discharging $b$. – Mauro ALLEGRANZA May 30 '17 at 05:54
  • 1
    I think in the Fitch program, I would have to assume a, obtain ~b v a (intro disjunction), then obtain b->a from ~b v a. Thanks for the help, I think I got it. – Matt May 31 '17 at 07:03
  • No, @Matt , your system might just require you to assume $a$ and $b$ a few more times. $\small\def\fitch#1#2{\quad\begin{array}{|l}#1\\hline #2\end{array}}\def\getsto{\leftrightarrow} \fitch{\lnot (a\getsto b)}{\fitch{a}{\fitch{b}{\fitch ab\a\to b\\quad\vdots\b\to a\a\getsto b\\bot}\\lnot b}\a\to\lnot b\\quad\vdots\\lnot b\to a\a\getsto\lnot b}$ – Graham Kemp Jul 22 '19 at 23:35
-1

One direction of the equivalence is relatively easy to show: $A ↔ ¬B ∴ ¬(A ↔ B)$. The basic plan is to negate the goal, derive a contradiction which will then allow one to derive the goal.

Here is a proof using a Fitch-style natural deduction proof checker:

enter image description here

To show the other direction is more involved. Again, one can negate the goal, $A ↔ ¬B$, but one should rewrite the goal as a conjunction of disjunctions, $(¬A ∨ ¬B) ∧ (A ∨ B)$, so one can use other inference rules. Once one reaches a contradiction this will give one the rewritten goal from which one can derive the desired biconditional.

Here is a proof of the other direction, $¬(A ↔ B) ∴ A ↔ ¬B$:

enter image description here

For the proof checker and the associated textbook see the links below.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf

Frank Hubeny
  • 1,527