Proof of proveit.logic.booleans.quantification.existence.skolem_elim theorem

import proveit
from proveit import P, Q, alpha
from proveit.core_expr_types import x_1_to_n, Q__x_1_to_n, P__x_1_to_n
from proveit.logic import Not, Equals, TRUE, NotEquals
from proveit.logic.booleans.quantification.existence import skolem_elim_lemma
from proveit import defaults
theory = proveit.Theory() # the theorem's theory

%proving skolem_elim

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

skolem_elim_lemma

 ⊢  

skolem_elim_lemma_inst = skolem_elim_lemma.instantiate({alpha:Equals(alpha, TRUE), P:P, Q:Q}, 
                                                   assumptions=[skolem_elim.condition])

skolem_elim_lemma_inst:  ⊢  

antecedent = skolem_elim.instance_expr.instance_expr.antecedent

antecedent:

defaults.assumptions = (skolem_elim_lemma.condition, antecedent)

defaults.assumptions:

P_impl_alpha = antecedent.derive_right().instantiate(assumptions=[Q__x_1_to_n])

P_impl_alpha: ,  ⊢  

P_impl_alpha.derive_consequent(assumptions=[P__x_1_to_n])

, ,  ⊢  

alpha_eq_true__under__assumptions = Equals(alpha, TRUE).prove(
    assumptions=[*defaults.assumptions, Q__x_1_to_n, P__x_1_to_n])

alpha_eq_true__under__assumptions: , ,  ⊢  

P__impl__alpha_eq_T = alpha_eq_true__under__assumptions.as_implication(P__x_1_to_n)

P__impl__alpha_eq_T: ,  ⊢  

P__impl__alpha_eq_T.generalize(x_1_to_n, conditions=[Q__x_1_to_n])

 ⊢  

skolem_elim_lemma_inst.derive_consequent()

,  ⊢  

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

%qed

proveit.logic.booleans.quantification.existence.skolem_elim has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	deduction	2	⊢
2	instantiation	3, 4	,  ⊢
	:
3	axiom		⊢
	proveit.logic.booleans.eq_true_elim
4	modus ponens	5, 6	,  ⊢
5	instantiation	7, 8, 9	⊢
	: , : , : , :
6	instantiation	10, 11, 12	⊢
	: , :
7	conjecture		⊢
	proveit.logic.booleans.quantification.existence.skolem_elim_lemma
8	assumption		⊢
9	instantiation	13	⊢
	: , :
10	conjecture		⊢
	proveit.logic.booleans.conjunction.and_if_both
11	instantiation	14, 24	⊢
	: , :
12	generalization	15	⊢
13	axiom		⊢
	proveit.logic.equality.equality_in_bool
14	theorem		⊢
	proveit.logic.booleans.conjunction.left_from_and
15	deduction	16	,  ⊢
16	instantiation	17, 18	, ,  ⊢
	:
17	axiom		⊢
	proveit.logic.booleans.eq_true_intro
18	modus ponens	19, 20	, ,  ⊢
19	instantiation	21, 22	,  ⊢
	:
20	assumption		⊢
21	instantiation	23, 24	⊢
	: , :
22	assumption		⊢
23	theorem		⊢
	proveit.logic.booleans.conjunction.right_from_and
24	assumption		⊢