Arithmetization can be viewed in many contexts. This topic is referring to the arithmetization of mathematical theorems into integer optimization problems and therefore open the possibility to computer-based mathematical proving.

Any boolean formula can be transformed into a 3 way conjunctive normal form. Any 3 way conjunctive normal form boolean formula itself can be transformed into an integer nonlinear equation. With the transformations

\begin{align} \left( A \vee B \right) & \mapsto & 1 - \left( 1-A \right) \cdot \left( 1-B \right) \\ \left( A \wedge B \right) & \mapsto & A \cdot B \\ \neg A & \mapsto & 1-A \end{align}

Notice that De Morgan's rules apply since \begin{equation} \neg \left( A \wedge B \right) \Leftrightarrow \left( \neg A \vee \neg B \right) \mapsto 1 - A \cdot B \end{equation}