# Proof of proveit.logic.booleans.disjunction.destructive_dilemma theorem¶

In [1]:
import proveit
from proveit import defaults
from proveit import A, B, C, D
from proveit.logic import Implies, Not, Or
from proveit.logic.booleans.disjunction  import left_in_bool, right_in_bool
left_in_bool.proof().disable(); right_in_bool.proof().disable() # disable these to avoid a longer proof
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving destructive_dilemma

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
destructive_dilemma:
(see dependencies)

Prove by applying the constructive_dilemma after taking contraposing $A \Rightarrow C$ to $\lnot C \Rightarrow \lnot A$ and $B \Rightarrow D$ to $\lnot D \Rightarrow \lnot B$.

In [3]:
defaults.assumptions = destructive_dilemma.all_conditions()

defaults.assumptions:
In [4]:
Implies(A, C).contrapose()

In [5]:
Implies(B, D).contrapose()

In [6]:
Or(Not(C), Not(D)).derive_via_multi_dilemma(Or(Not(A), Not(B)))

, , , , , ,  ⊢
destructive_dilemma may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

In [7]:
%qed

proveit.logic.booleans.disjunction.destructive_dilemma has been proven.

Out[7]:
step typerequirementsstatement
0generalization1
1instantiation2, 3, 4, 5, 6, 7, 8, 9, , , , , ,  ⊢
: , : , : , :
2conjecture
proveit.logic.booleans.disjunction.constructive_dilemma
3instantiation12, 10
:
4instantiation12, 11
:
5instantiation12, 14
:
6instantiation12, 17
:
7assumption
8instantiation15, 13, 14,  ⊢
: , :
9instantiation15, 16, 17,  ⊢
: , :
10assumption
11assumption
12conjecture
proveit.logic.booleans.negation.closure
13assumption
14assumption
15theorem
proveit.logic.booleans.implication.to_contraposition
16assumption
17assumption