Axioms for the theory of proveit.logic.booleans.quantification.existence

Unlike Forall, Exists is not fundamentally defined in the core of Prove-It. It must be defined via its relationship with Forall.

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit.logic import TRUE, in_bool, Forall, Exists, NotExists, Not, Equals, NotEquals
from proveit.numbers import Natural, NaturalPos
from proveit import n, P, Q
from proveit.logic.booleans.quantification import (
    general_exists_Px_st_Qx, general_exists_Py_st_Qy, general_forall__Py_not_T__st_Qy, general_notexists_Px_st_Qx)
%begin axioms

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

Defines the $\exists$ operation generically for any number of instance variables or conditions by equating it to an equivalent expression in terms of $\forall$:

exists_def = Forall(n, Forall((P, Q), 
                             Equals(general_exists_Px_st_Qx, 
                                    Not(general_forall__Py_not_T__st_Qy)).with_wrap_after_operator()),
                  domain=NaturalPos)

exists_def:

The equivalent expression to saying "there exists an instance of $x_1, \ldots, x_l$ variables for which the set of $Q_{1}, \ldots, Q_{k}$ conditions are satisfied such that $P(x_1, \ldots, x_l)$ is true" is to say that the following is not true: "for all occurrences of $x_1, \ldots, x_l$ for which the set of $Q_{1}, \ldots, Q_{k}$ conditions are satisfied,$P(x_1, \ldots, x_l)$ is not equal to TRUE". That is, "there exists appropriately constrained operands of $P$ for which the $P$ operation is true" means that "it is not the case that all appropriately constrained operands of $P$ cause the $P$ operation to not evaluate to true". This is expressed in a way that does not assume that the $P$ operation returns a Boolean, exploiting the fact that Equals ($=$) is defined to always evaluate to a Boolean and therefore NotEquals ($\neq$) as well. Existence in this theory means that the $P$ operation evaluates to true for some instance of appropriately constrained operands but it does not mean that the $P$ operation always evaluates to a Boolean under this constraint.

Defines the $\nexists$ operation generically for any number of instance variables or conditions by equating it to the negation of the corresponding $\exists$ operation:

not_exists_def = Forall(n, Forall((P, Q), 
                                Equals(general_notexists_Px_st_Qx, 
                                       Not(general_exists_Py_st_Qy)).with_wrap_after_operator()),
                      domain=NaturalPos)

not_exists_def:

%end axioms

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