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
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)
In [3]:
exists_with_conditions_is_bool = Forall(n, Forall((P, Q), in_bool(general_exists_Py_st_Qy)),
domain=NaturalPos)
In [4]:
notexists_is_bool = Forall(n, Forall(P, in_bool(general_notexists_Px)),
domain=NaturalPos)
In [5]:
notexists_with_conditions_is_bool = Forall(n, Forall((P, Q), in_bool(general_notexists_Py_st_Qy)),
domain=NaturalPos)
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)
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)
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)
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)
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)
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)
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)
"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)
"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)
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)
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)
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)
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])
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)
In [21]:
%end theorems