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

Введём понятие арифметизации булевых формул. Пусть нам дана формула [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]\varphi \land \psi \to A_\varphi \cdot A_\psi[/math];
4. [math]\varphi \lor \psi \to 1 - (1 - A_\varphi) \cdot (1 - A_\psi)[/math];
5. [math]\exists x \varphi(x) \to \sum\limits_{x=0}^{1} A_\varphi(x)[/math];
6. [math]\forall x \varphi(x) \to \prod\limits_{x=0}^{1} A_\varphi(x)[/math].

Заметим, что если [math]\phi[/math] не содержит кванторов, то [math]|A_\phi| \le C |\phi|[/math] , где [math]C[/math] — некоторая константа.

Лемма (1):

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

Доказательство:

[math]\triangleright[/math]

proof

[math]\triangleleft[/math]

Введем обозначение: [math]A_i(x_{i+1}) = \sum\limits_{x_{i+2} = 0}^{1}\ldots\sum\limits_{x_m = 0}^{1} A(c_1,\ldots, c_i, x_{i+1}, ..., x_m)[/math], где [math]c_1, \ldots, c_i[/math] — некоторые константы.

Лемма (2):

При введенных выше обозначениях выполняются: [math]A_0(0) + A_0(1) = k[/math] [math]\forall 1 \le i \le m: A_i(0) + A_i(1) = A_{i-1}(c_i)[/math]

Доказательство:

[math]\triangleright[/math]

proof

[math]\triangleleft[/math]