Unlike `Forall`

, `Exists`

is not fundamentally defined in the core of **Prove-It**. It must be defined via its relationship with `Forall`

.

In [1]:

```
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
```

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

In [2]:

```
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)
```

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**:

In [3]:

```
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)
```

In [4]:

```
%end axioms
```