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

Введём понятие арифметизации булевых формул. Пусть нам дана формула [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]Q_i = \sum\limits_{x_i = 0}^{1}[/math] или [math]Q_i = \prod\limits_{x_i = 0}^{1}[/math]
• [math]s = Q_1 \ldots Q_m A(x_1, \ldots, x_m)[/math]
• [math]A_i(x_{i+1}) = Q_{i + 2} \ldots Q_m A(c_1,\ldots, c_i, x_{i+1}, ..., x_m)[/math], где [math]c_1, \ldots, c_i[/math] — двоичные константы.

Лемма (2):

При введенных выше обозначениях выполняются: Если [math]Q_1 = \sum\limits_{x_1 = 0}^{1}[/math], то [math]A_0(0) + A_0(1) = s[/math], если [math]Q_1 = \prod\limits_{x_1 = 0}^{1}[/math], то [math]A_0(0) \cdot A_0(1) = s[/math] Если [math]Q_i = \sum\limits_{x_i = 0}^{1}[/math], то [math] A_i(0) + A_i(1) = A_{i-1}(c_i)[/math] Если [math]Q_i = \prod\limits_{x_i = 0}^{1}[/math], то [math] A_i(0) \cdot A_i(1) = A_{i-1}(c_i)[/math]

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

[math]\triangleright[/math]

proof

[math]\triangleleft[/math]