# Structure of an if and only if proof

I am trying to get this proof to work out and so far I feel like I have the first part right but I'm stuck on how to get the A→B part. Here is a very similar question with three answers: Prove (¬P ∨ Q) ↔ (P → Q) Your question seems to be focused on the Fitch system and your approach to the problem seems to be different. I will only address how you might proceed without considering how you might do this in the Fitch system.

You are attempting to use disjunction elimination with the first line having ¬A v A. However, what you need to show is given A→B that you can derive ¬A ∨ B and then show given ¬A ∨ B that you can derive A→B.

Here is how it would be done with another proof checker. I include it to show what might work. You will have to adjust it to the rules and syntax of the proof checker you are using. Note that one direction of the biconditional (if and only if) proof occurs on lines 1 to 9. The other direction occurs on line 10 to 17. On line 18, the biconditional (↔) is introduced.

The descriptions of the rules are given in 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, Winter 2018. http://forallx.openlogicproject.org/

I am trying to get this proof to work out and so far I feel like I have the first part right but I'm stuck on how to get the A→B part.

Begin by assuming A → B, then state LEM as a Tautological Consequence to use disjunction elimination to derive ¬A ˅ B. Also, your attempt needs to be tidied up, you have a few unecsessary steps and you seem to forget that the goal is ¬A ˅ B (rather than A ˅ ¬B as you have towards the end).

``````| |_ A → B            Assumption
| | ¬A ˅ A            Taut Con (LEM)
| | |_ ¬A             Assumption
| | |  ¬A ˅ B         ˅ Intro
| | ¬A → (¬A ˅ B)     → Intro
| | |_ A              Assumption
| | |  B              → Elim
| | |  ¬A ˅ B         ˅ Intro
| | A → (¬A ˅ B)      → Intro
| | (¬A ˅ B)          ˅ Elim
| (A → B) → (¬A ˅ B)  → Intro
``````

Now, for the converse, you should assume ¬A ˅ B and derive A → B through ˅ elimination. Assuming ¬A and A will derive B from explosion, while assuming B and A will derive B from reiteration.

Hence (¬A ˅ B) → (A → B).

Then use biconditional introduction to complete the proof.