Proof of proveit.logic.booleans.quantification.existence.skolem_elim_lemma theorem¶
In [1]:
import proveit
from proveit import 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 import defaults
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving skolem_elim_lemma
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
skolem_elim_lemma:
(see dependencies)
skolem_elim_lemma:
(see dependencies)
In [3]:
antecedent = skolem_elim_lemma.instance_expr.instance_expr.antecedent
antecedent: 
In [4]:
main_assumptions = (*skolem_elim_lemma.conditions.entries, antecedent)
main_assumptions: 
This is be a proof by contradiction¶
In [5]:
defaults.assumptions = (*main_assumptions, Not(alpha))
defaults.assumptions: 
In [6]:
existential, universal = antecedent.derive_left(), antecedent.derive_right()
In [7]:
unfolded_existential = existential.unfold()
unfolded_existential: 
, ⊢ 
, ⊢ 
In [8]:
universal
In [9]:
alpha_under_assumptions = universal.instantiate(assumptions=[Q__x_1_to_n]).derive_consequent(
assumptions=[Equals(P__x_1_to_n, TRUE)])
alpha_under_assumptions: 
, , 
⊢ 
, , 
⊢ 
In [10]:
contradiction = Not(alpha).derive_contradiction(
assumptions=[*defaults.assumptions, Q__x_1_to_n, Equals(P__x_1_to_n, TRUE)])
contradiction: , , , 
⊢ 
, , , 
⊢ 
In [11]:
contradiction.deny_assumption(Equals(P__x_1_to_n, TRUE))
, , ⊢ 
In [12]:
P_neq_T = NotEquals(P__x_1_to_n, TRUE).prove(assumptions=[*defaults.assumptions, Q__x_1_to_n])
P_neq_T: , , ⊢ 
, , ⊢ 
In [13]:
P_neq_T.generalize(x_1_to_n, conditions=[Q__x_1_to_n])
, ⊢ 
In [14]:
unfolded_existential.affirm_via_contradiction(alpha, assumptions=main_assumptions)
, , ⊢
In [15]:
%qed
Out[15]:
