# Theorems (or conjectures) for the theory of proveit.logic.booleans.quantification.existence¶

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit.logic import Forall, Exists, NotExists, Boolean
from proveit.logic import Implies, Equals, TRUE, NotEquals, Not, And, in_bool, SubsetEq
from proveit.numbers import Natural, NaturalPos, one, Less, LessEq
from proveit import n, A, B, P, Q, R, alpha
from proveit.core_expr_types import (
x_1_to_n, y_1_to_n, Q__x_1_to_n, Q__y_1_to_n, P__x_1_to_n, P__y_1_to_n)
from proveit.logic.booleans.quantification import (
general_forall_Px, general_forall_Py,
general_forall_Px_if_Qx, general_forall_Py_if_Qy,
general_forall__Py_not_T, general_forall__Py_not_T__st_Qy,
general_forall_st_Qx__Px_implies_Rx,
general_exists_Px, general_exists_Px_st_Qx, general_exists_Py_st_Qy,
general_exists_Px_st_Qx, general_exists_Py_st_Qy, general_exists_Rz_st_Qz,
general_exists_in_A_Px_st_Qx, general_exists_in_B_Py_st_Qy,
general_exists_notPx_st_Qx,
general_notexists_Px, general_notexists_Px_st_Qx, general_notexists_Py_st_Qy,
general_notexists_notPy_st_Qy)
%begin theorems

Defining theorems for theory 'proveit.logic.booleans.quantification.existence'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions


By our definition for $\exists$, such an expression is always a Boolean (it acquires this property from $\forall$):

In [2]:
exists_is_bool = Forall(n, Forall(P, in_bool(general_exists_Px)),
domain=NaturalPos)

exists_is_bool (conjecture without proof):

In [3]:
exists_with_conditions_is_bool = Forall(n, Forall((P, Q), in_bool(general_exists_Py_st_Qy)),
domain=NaturalPos)

exists_with_conditions_is_bool (conjecture without proof):

In [4]:
notexists_is_bool = Forall(n, Forall(P, in_bool(general_notexists_Px)),
domain=NaturalPos)

notexists_is_bool (conjecture without proof):

In [5]:
notexists_with_conditions_is_bool = Forall(n, Forall((P, Q), in_bool(general_notexists_Py_st_Qy)),
domain=NaturalPos)

notexists_with_conditions_is_bool (conjecture without proof):

Fold and unfold the definition:

In [6]:
exists_unfolding = Forall(n, Forall((P, Q),
Implies(general_exists_Px_st_Qx,
Not(general_forall__Py_not_T__st_Qy)).with_wrap_after_operator()),
domain=NaturalPos)

exists_unfolding (established theorem):

In [7]:
exists_folding = Forall(n, Forall((P, Q), general_exists_Px_st_Qx ,
condition=Not(general_forall__Py_not_T__st_Qy)),
domain=NaturalPos)

exists_folding (conjecture without proof):

Providing a legitimate example is one way to prove that something exists:

In [8]:
existence_by_example = Forall(
n, Forall(P, Forall(y_1_to_n,
general_exists_Px,
condition=P__y_1_to_n)),
domain=NaturalPos)

existence_by_example (conjecture without proof):

In [9]:
existence_by_example_with_conditions = Forall(
n, Forall((P, Q), Forall(y_1_to_n,
general_exists_Px_st_Qx,
conditions=(P__y_1_to_n, Q__y_1_to_n))),
domain=NaturalPos)

existence_by_example_with_conditions (conjecture without proof):

If the negation of some instance exists, then it cannot always be true:

In [10]:
exists_not_implies_not_forall = Forall(
n, Forall(
(P, Q), Implies(general_exists_notPx_st_Qx,
Not(general_forall_Py_if_Qy))
.with_wrap_after_operator()),
domain=NaturalPos)

exists_not_implies_not_forall (conjecture without proof):

Negating both sides of exists_def:

In [11]:
exists_def_negation = Forall(
n, Forall(
(P, Q), Equals(general_notexists_Px_st_Qx,
general_forall__Py_not_T__st_Qy)
.with_wrap_after_operator()),
domain=NaturalPos)

exists_def_negation (conjecture without proof):

In [12]:
not_exists_via_forall = Forall(
n, Forall(
(P, Q), Implies(general_forall__Py_not_T__st_Qy,
general_notexists_Px_st_Qx)
.with_wrap_after_operator()),
domain=NaturalPos)

not_exists_via_forall (conjecture without proof):

"Unfold" $\nexists$ to $\lnot \exists$:

In [13]:
not_exists_unfolding = Forall(
n, Forall(
(P, Q), Implies(general_notexists_Px_st_Qx,
Not(general_exists_Py_st_Qy))
.with_wrap_after_operator()),
domain=NaturalPos)

not_exists_unfolding (conjecture without proof):

"Fold" $\lnot \exists$ into $\nexists$:

In [14]:
not_exists_folding = Forall(
n, Forall(
(P, Q), Implies(Not(general_exists_Px_st_Qx),
general_notexists_Py_st_Qy)
.with_wrap_after_operator()),
domain=NaturalPos)

not_exists_folding (conjecture without proof):

If all instances are true, then there exists no counter-example:

In [15]:
forall_implies_not_exists_not = Forall(
n, Forall(
(P, Q), Implies(general_forall_Px_if_Qx,
general_notexists_notPy_st_Qy)
.with_wrap_after_operator()),
domain=NaturalPos)

forall_implies_not_exists_not (conjecture without proof):

If elements exists in $A$ that satisfies some criteria, they also exist in $B$ given that $A \subseteq B$ (simply because all elements in $A$ also exist in $B$):

In [16]:
exists_in_superset = Forall(
n, Forall(
(P, Q, A, B), Implies(general_exists_in_A_Px_st_Qx,
general_exists_in_B_Py_st_Qy)
.with_wrap_after_operator(),
conditions=[SubsetEq(A, B)]),
domain=NaturalPos)

exists_in_superset (conjecture without proof):

If an element exists satisfies some criteria under a certain set of conditions, it also exists under less restrictive criteria:

In [17]:
'''
exists_more_generally = Forall((i, j, k),
Forall(l, Forall((P, iter_q1k),
Implies(general_exists_Px,
exists_Px_Q1i_Qjk).with_wrap_after_operator()),
domain=NaturalPos),
domain=Natural,
conditions=[number_ordering(LessEq(one, i), Less(i, j), LessEq(j, k))])
'''


If $P(x_{1},\ldots,x_{l})$ given $R(x_1,\ldots,x_{l})$ for all appropriately conditioned instances, then existence of a satisfying instance of the former implies existence of a satisfying instance of the latter (e.g., the same instance).

In [18]:
existential_implication = Forall(n, Forall((P, Q, R),
Implies(general_forall_st_Qx__Px_implies_Rx,
Implies(general_exists_Py_st_Qy,
general_exists_Rz_st_Qz).with_wrap_after_operator()) \
.with_wrap_after_operator()),
domain=NaturalPos)

existential_implication (conjecture without proof):

In [19]:
skolem_elim_lemma = Forall(
(n, alpha),
Forall((P, Q),
Implies(And(Exists(y_1_to_n, P__y_1_to_n, conditions=[Q__y_1_to_n]),
Forall(x_1_to_n,
Implies(P__x_1_to_n, alpha),
conditions=[Q__x_1_to_n])), alpha)),
domains=[NaturalPos, Boolean])

skolem_elim_lemma (established theorem):

In [20]:
skolem_elim = Forall(
n,
Forall((P, Q, alpha),
Implies(And(Exists(y_1_to_n, P__y_1_to_n, conditions=[Q__y_1_to_n]),
Forall(x_1_to_n,
Implies(P__x_1_to_n, alpha),
conditions=[Q__x_1_to_n])), alpha)),
domain=NaturalPos)

skolem_elim (established theorem):

In [21]:
%end theorems

These theorems may now be imported from the theory package: proveit.logic.booleans.quantification.existence