Derivation using inference rules

Question

Suppose I have the premise:

~(AvB).(Negation A or B)

How can I get to the conclusion:

A<=>B (A if and only if B)

using inference rules like introduction or elimination and also assumptions?

I need to set up a derivation with a scope line.

Answer 1

Here's about half the proof you need:

1. ~(A v B)   Premise
2. | A        Assumption
3. | A v B    vI 2
4. | (A v B) & ~ (A v B) &I 3,1
5. ~A         Contradiction Elimination
6. ~A v B     vI 5
7. A -> B     Material Implication 6
...
~14. A <-> B   Biconditional Introduction 7, 13

---

Proof with DeMorgan:

1. ~(A v B)   Premise
2. ~A & ~B    DeM 1
3. ~A         &E 2
4. ~A v B     vI 3
5. A -> B     Material Implication 4
...
10. A <-> B Biconditional Introduction 5,9

Answer 2

Here is an alternate proof using contradiction elimination (explosion):

The proof uses disjunction introduction (∨I), contradiction introduction (⊥I), contradiction elimination (⊥E) and biconditional introduction (↔I).

To help make this result intuitive, ¬(A ∨ B) is true only when both A and B are false. But that is also a valuation that makes A↔B true. When ¬(A ∨ B) is false it does not matter what value A↔B has. The conditional representing the premise as antecedent and the conclusion as consequent will be true.

Links to the proof checker and descriptions of these inference rules can be found 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