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.
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.
Sign up to join this communitySuppose 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.
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
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