logo

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