Proof of proveit.logic.booleans.negation.double_negation_elim_lemma theorem

import proveit
from proveit import A
from proveit.logic import TRUE, FALSE, Implies, Not, Equals
from proveit.logic.booleans  import true_axiom
from proveit.logic.booleans.implication import false_antecedent_implication
from proveit.logic.booleans.negation  import not_t
theory = proveit.Theory() # the theorem's theory

%proving double_negation_elim_lemma

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

Use the above theorem to perform proof-by-cases. Start with the $A=\top$ case.

true_axiom

 ⊢  

true_axiom.as_implication(Not(Not(TRUE)))

 ⊢  

Now for the $A=\bot$ case.

Not(Not(FALSE)).disprove()

 ⊢  

Implies(Not(Not(FALSE)), FALSE).prove()

 ⊢  

We will now be able to prove our theorem by cases.

%qed

proveit.logic.booleans.negation.double_negation_elim_lemma has been proven.

	step type	requirements	statement
0	instantiation	1, 2, 3	⊢
	: , : , :
1	conjecture		⊢
	proveit.logic.booleans.conditioned_forall_over_bool_by_cases
2	deduction	4	⊢
3	instantiation	5, 6	⊢
	: , :
4	axiom		⊢
	proveit.logic.booleans.true_axiom
5	theorem		⊢
	proveit.logic.booleans.implication.falsified_antecedent_implication
6	instantiation	7, 8	⊢
	:
7	theorem		⊢
	proveit.logic.booleans.negation.double_negation_intro
8	theorem		⊢
	proveit.logic.booleans.negation.not_false