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.
# 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
Defining axioms for theory 'proveit.logic.booleans.quantification.universality' Subsequent end-of-cell assignments will define axioms %end_axioms will finalize the definitions
If a $\forall$ statement is not true (the instance expression is not true for all valid instances) then it is defined to be false:
forall_in_bool = Forall(n, Forall(P, in_bool(general_forall_Px)),
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.
These axioms may now be imported from the theory package: proveit.logic.booleans.quantification.universality