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.
1
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
-
-
Because we need to arrive at a contradiction to get out of the conditional proof? – virmaior Mar 15 '16 at 7:47
-
Thank you. By the way in case you haven't noticed I am very new to this, that is why I am asking such basic questions. We all have to start somewhere right? – Ant Mar 15 '16 at 8:06
-
Can we use de-morgan to simplify ~A and ~B derivation? Can we then conclude that A=B? I mean can we switch to the semantic level saying that if premise requires both A = false and B =false, which means that their logic value is the same and thus propositions are equal? – Valentin Tihomirov Mar 15 '16 at 9:55
-
@ValentinTihomirov either of those approaches could work depending on the conditions under which one is asked to prove this. DeMorgan would eliminate the need for a conditional proof. – virmaior Mar 15 '16 at 13:04
1
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
answered Jun 11 at 19:04
