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

In [1]:
import proveit
from proveit import defaults
from proveit import A, B, C, D
from proveit.logic import Or
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving constructive_dilemma

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

Prove by applying the singular_constructive_dilemma on $(C \lor D)$ as a unit, using or_if_left to prove $A \Rightarrow (C \lor D)$ and or_if_right to prove $B \Rightarrow (C \lor D)$ under the constructive_dilemma conditions.

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

defaults.assumptions:
In [4]:
Or(C, D).conclude_via_example(C, assumptions = defaults.assumptions + (A,))

, , ,  ⊢
In [5]:
Or(C, D).conclude_via_example(D, assumptions = defaults.assumptions + (B,))

, , ,  ⊢
In [6]:
Or(A, B).derive_via_singular_dilemma(Or(C, D))

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

In [7]:
%qed

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

Out[7]:
step typerequirementsstatement
0generalization1
1instantiation2, 3, 4, 5, 6, 7, , , , , ,  ⊢
: , : , :
2theorem
proveit.logic.booleans.disjunction.singular_constructive_dilemma
3assumption
4assumption
5assumption
6deduction8, ,  ⊢
7deduction9, ,  ⊢
8instantiation10, 13, 14, 11, , ,  ⊢
: , :
9instantiation12, 13, 14, 15, , ,  ⊢
: , :
10conjecture
proveit.logic.booleans.disjunction.or_if_left
11modus ponens16, 17,  ⊢
12conjecture
proveit.logic.booleans.disjunction.or_if_right
13assumption
14assumption
15modus ponens18, 19,  ⊢
16assumption
17assumption
18assumption
19assumption