Арифметизация булевых формул с кванторами

Введём понятие арифметизации булевых формул. Пусть нам дана формула [math]\phi(x_1 \ldots x_m)[/math]. Сделаем следующие преобразования и получим формулу [math]A_\phi(x_1, x_2, \ldots, x_m)[/math]:

1. [math] x_i \to x_i[/math];
2. [math] \lnot x \to 1 - x[/math];
3. [math]\Phi \land \Psi \to A_\Phi \cdot A_\Psi[/math];
4. [math]\Phi \lor \Psi \to 1 - (1 - A_\Phi) \cdot (1 - A_\Psi)[/math].

Заметим, что длина формулы при этом возрастёт не более, чем в константу раз.

Лемма (1):

[math]\phi(x_1 \ldots x_m) = A_\phi(x_1, \ldots, x_m)[/math].