Note that $\forall$ is a core concept of **Prove-It** pertaining to the *instantiation* and *generalization* derivation steps. As such, axioms are not needed to define the fundamentals of $\forall$. These axioms just add some extra properties that are not intrinsic to those core fundamentals.

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 Forall, in_bool
from proveit.numbers import NaturalPos
from proveit import n, P
from proveit.logic.booleans.quantification import general_forall_Px
%begin axioms
```

**If a $\forall$ statement is not true (the instance expression is not true for all valid instances) then it is defined to be false:**

In [2]:

```
forall_in_bool = Forall(n, Forall(P, in_bool(general_forall_Px)),
domain=NaturalPos)
```

This is applicable to any universal quantification. Note that there is no guarantee that it can be proven to be true or false, but it must be one of these according to this axiom.

In [3]:

```
%end axioms
```