1

So I'm stuck on a fitch style proof to get $(A \wedge B) \vee (\neg A \wedge \neg B)$ from $A\leftrightarrow B$. I'm not allowed to use De Morgan's or Modus Tollens for this proof.

I know I have to isolate each letter but I'm not sure how to do so because each attempt I end up isolating one of the letters but in the scope of a subproof, not the main scope line.

Right now I assumed the negation of the conclusion and eliminated the biconditional and that's what I've been working around now.

Thanks for helping.

Rodrigo de Azevedo
  • 1
user494506
  • 13
  • 2
  • How did you define $A\leftrightarrow B$? Because $(A\wedge B)\vee(\neg A\wedge \neg B)$ might very well be one way to do it. –  Oct 22 '17 at 22:30
  • A $\leftrightarrow$ B is defined as (A $\implies$ B) /\ (B $\implies$ A) – user494506 Oct 22 '17 at 22:40

3 Answers3

0
  1. $A \implies B$ (base assumption)
  2. $B \implies A$ (base assumption)
    • $A$ (assumption)
    • $A \implies B$ (restating 1)
    • $B$ (by 3 and 4, $\implies$ elim)
  3. $A \vee \neg A $ (taut)
  4. $(A \wedge B) \vee (\neg A)$ ($\wedge$ intro from 2-3)
    • $\neg A$ (assumption)
      • $B$ (assumption)
      • $A$ (by 2)
    • contradiction so $\neg B$ by above
  5. $\neg A \implies (\neg A \wedge \neg B)$
  6. ($A \wedge B) \vee (\neg A \wedge \neg B)$

As you can probably tell, I'm new to this area. But i do believe this is a complete proof. Please point out any issues in the comments. (Also if anyone knows how to write out the proofs better, please do point me in the right direction or feel free to edit).

mdave16
  • 951
0

Here's a possible proof not assuming you already know excluded middle follows in the Fitch system as mdave16's answer did:

  1. $(A \rightarrow B) \wedge (B \rightarrow A)$ (assumption)
  2. $\quad A \rightarrow B, B \rightarrow A$ ($\wedge$-elim) on 1
  3. $\quad \lnot ((A \wedge B) \vee (\lnot A \wedge \lnot B))$ (assumption)
  4. $\quad\quad A \wedge B$ (assumption)
  5. $\quad\quad\quad (A \wedge B) \vee (\lnot A \wedge \lnot B)$ ($\vee$-intro from 4)
  6. $\quad\quad\quad \lnot ((A \wedge B) \vee (\lnot A \wedge \lnot B))$ (from 3)
  7. $\quad\quad A\wedge B \rightarrow (A \wedge B) \vee (\lnot A \wedge \lnot B)$ ($\rightarrow$-intro from 4 through 5)
  8. $\quad\quad A\wedge B \rightarrow \lnot ((A \wedge B) \vee (\lnot A \wedge \lnot B))$ ($\rightarrow$-intro from 4 through 6)
  9. $\quad\quad \lnot(A\wedge B)$ ($\lnot$-intro from 7 and 8)
  10. $\quad\quad A$ (assumption)
  11. $\quad\quad\quad A \rightarrow B$ (from 2)
  12. $\quad\quad\quad B$ (modus ponens from 11 and 10)
  13. $\quad\quad\quad A \wedge B$ ($\wedge$-intro from 10 and 12)
  14. $\quad\quad\quad \lnot (A \wedge B)$ (from 9)
  15. $\quad\quad A \rightarrow A \wedge B$ ($\rightarrow$-intro from 10 through 13)
  16. $\quad\quad A \rightarrow \lnot (A \wedge B)$ ($\rightarrow$-intro from 10 through 14)
  17. $\quad\quad \lnot A$ ($\lnot$-intro from 15 and 16)
  18. $\quad\quad B$ (assumption)
  19. $\quad\quad\quad \lnot A$ (from 17)
  20. $\quad\quad B \rightarrow \lnot A$ ($\rightarrow$-intro from 18 through 19)
  21. $\quad\quad B \rightarrow A$ (from 2)
  22. $\quad\quad \lnot B$ ($\lnot$-intro from 21 and 20)
  23. $\quad\quad \lnot A \wedge \lnot B$ ($\wedge$-intro from 17 and 22)
  24. $\quad\quad (A \wedge B) \vee (\lnot A \wedge \lnot B)$ ($\vee$-intro from 23)
  25. $\quad\quad \lnot ((A \wedge B) \vee (\lnot A \wedge \lnot B))$ (from 3)
  26. $\quad \lnot ((A \wedge B) \vee (\lnot A \wedge \lnot B)) \rightarrow (A \wedge B) \vee (\lnot A \wedge \lnot B)$ ($\rightarrow$-intro from 3 through 24)
  27. $\quad \lnot ((A \wedge B) \vee (\lnot A \wedge \lnot B)) \rightarrow \lnot ((A \wedge B) \vee (\lnot A \wedge \lnot B))$ ($\rightarrow$-intro from 3 through 25)
  28. $\quad (A \wedge B) \vee (\lnot A \wedge \lnot B)$ ($\lnot$-elim from 26 and 27)
  29. (optional) $(A \leftrightarrow B) \rightarrow ((A \wedge B) \vee (\lnot A \wedge \lnot B))$ ($\rightarrow$-intro from 1 through 28)

So, to summarize the logical flow of the proof:

Suppose $A \leftrightarrow B$; we will prove $(A \wedge B) \vee (\lnot A \vee \lnot B)$ by contradiction. So, suppose also that $\lnot ((A \wedge B) \vee (\lnot A \vee \lnot B))$. Then this implies $\lnot (A \wedge B)$ (up through line 9). This in turn implies $A$ cannot be true; otherwise $B$ would also be true, and we would get a contradiction $A \wedge B$ (up through line 17). However, since $B \rightarrow A$, if we know $\lnot A$ holds, then $\lnot B$ also holds (up through line 22). But now we have $\lnot A \wedge \lnot B$, so $(A \wedge B) \vee (\lnot A \wedge \lnot B)$ in fact holds, contradicting the assumption (up through line 25). Therefore, by contradiction, we have proven that $(A \wedge B) \vee (\lnot A \vee \lnot B)$ (up through line 28).

Daniel Schepler
  • 20,364
  • Off topic -- If I put this proof into Coq (with Peirce's law) and reduce to normal form, the corresponding program seems to be this: First, the program guesses $\lnot A \wedge \lnot B$ is the case with synthetic functions for $\lnot A$ and $\lnot B$. The synthetic function for $\lnot A$, if ever called with a proof of $A$, rewinds to the original function call and then uses that proof along with $A \rightarrow B$ to return a proof of $A \wedge B$. And similarly for the synthetic function for $\lnot B$. – Daniel Schepler Oct 23 '17 at 00:23
0

Here is another Fitch style proof:

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$

$\fitch{ 1. A \leftrightarrow B \quad Premise}{ \fitch{ 2. \neg ((A \land B) \lor (\neg A \land \neg B)) \quad \ Assume} { \fitch{ 3. A \quad \ Assume}{ 4. B \quad \leftrightarrow \ Elim \ 1,3\\ 5. A \land B \quad \land \ Intro \ 3,4\\ 6. (A \land B) \lor (\neg A \land \neg B) \quad \lor \ Intro \ 5\\ 7. \bot \quad \bot \ Intro \ 2,6\\ }\\ 8. \neg A \quad \neg \ Intro \ 3-7\\ \fitch{ 9. B \quad Assume}{ 10. A \quad \leftrightarrow \ Elim \ 1,9\\ 11. \bot \quad \bot \ Intro \ 8,10\\ }\\ 12. \neg B \quad \neg \ Intro \ 9-11\\ 13. \neg A \land \neg B \quad \land \ Intro \ 8,12\\ 14. (A \land B) \lor (\neg A \land \neg B) \quad \lor \ Intro \ 13\\ 15. \bot \quad \bot \ Intro \ 2,14\\ }\\ 16. \neg \neg ((A \land B) \lor (\neg A \land \neg B)) \quad \neg \ Intro \ 2-15\\ 17. (A \land B) \lor (\neg A \land \neg B) \quad \neg \ Elim \ 16\\ }$

Bram28
  • 100,612
  • 6
  • 70
  • 118