Введём понятие арифметизации булевых формул. Пусть нам дана формула <tex>\phi(x_1 \ldots x_m)</tex>. Сделаем следующие преобразования и получим формулу <tex>A_\phi(x_1, x_2, \ldots, x_m)</tex>:
# * <tex>x_i \to x_i</tex>;# * <tex>\lnot x \to 1 - x</tex>;# * <tex>\varphi \land \psi \to A_\varphi \cdot A_\psi</tex>;# * <tex>\varphi \lor \psi \to 1 - (1 - A_\varphi) \cdot (1 - A_\psi)</tex>;# <tex>\exists x \varphi(x) \to \sum\limits_{x=0}^{1} A_\varphi(x)</tex>;# <tex>\forall x \varphi(x) \to \prod\limits_{x=0}^{1} A_\varphi(x)</tex>.Заметим, что если <tex>\phi</tex> не содержит кванторов, то <tex>|A_\phi| \le C |\phi|</tex> , где <tex>C</tex> {{---}} некоторая константа.
{{Лемма
}}
Введем обозначенияДля арифметизации булевых формул с кванторами добавим еще два правила преобразования:* <tex>Q_i = \exists x \varphi(x) \to \sum\limits_{x_i x= 0}^{1}A_\varphi(x)</tex> или ;* <tex>Q_i = \forall x \varphi(x) \to \prod\limits_{x_i x= 0}^{1}A_\varphi(x)</tex>. Будем обозначать через <tex>Q_i</tex> квантор, связывающий переменную <tex>x_i</tex>. Через <tex>R_i</tex> будем обозначать операцию, в которую преобразуется квантор <tex>Q_i</tex>в процессе арифметизации. * Заметим, что любую булеву формулу можно привести к виду <tex>s = Q_1 \ldots Q_m A\phi(x_1, \ldots, x_m)</tex>* , где <tex>\phi</tex>A_i(x_{i+1{---}) = Q_{i + 2} формула, не содержащая кванторов. Кроме того, в процессе арифметизации <tex>Q_1 \ldots Q_m A\phi(c_1x_1,\ldots, c_i, x_{i+1}, ..., x_m)</tex>, где переходит в <tex>c_1R_1 \ldots R_m A_\phi(x_1, \ldots, c_ix_m)</tex> {{---}} двоичные константы. Поэтому далее будем рассматривать только формулы, которые имеют вид, указанный выше.
{{Лемма
|about=2
|statement=
При введенных выше обозначениях выполняются:# Если Пусть <tex>Q_1 \ldots Q_m \phi(x_1, \ldots, x_m)</tex> {{---}} булева формула с кванторами, переходящая в процессе арифметизации в <tex>s = R_1 \sumldots R_m A_\phi(x_1, \ldots, x_m)</tex>. <tex>c_1, \limits_ldots, c_m</tex> {x_1 {---}} двоичные константы. Обозначим через <tex>A_i(x_{i+1}) = 0R_{i+2}^\ldots R_m A_\phi(c_1, \ldots, c_i, x_{i+1}, \ldots, x_m)</tex>, где <tex>0 \le i \le m - 1</tex>. Тогда:# Если <tex>R_1 = \sum</tex>, то <tex>A_0(0) + A_0(1) = s</tex>, если <tex>Q_1 R_1 = \prod\limits_{x_1 = 0}^{1}</tex>, то <tex>A_0(0) \cdot A_0(1) = s</tex>.# Если <tex>Q_i = \sumforall i : 1 \le i \limits_{x_i = 0}^le m - 1</tex> если <tex>R_{i+1}= \sum</tex>, то <tex> A_i(0) + A_i(1) = A_{i-1}(c_i)</tex># Если , если <tex>Q_i R_{i+1} = \prod\limits_{x_i = 0}^{1}</tex>, то <tex> A_i(0) \cdot A_i(1) = A_{i-1}(c_i)</tex>.
|proof=
proof
}}
