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

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.

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

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)),
                      domain=NaturalPos)

forall_in_bool:

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.

%end axioms

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