70
правок
Изменения
Нет описания правки
Введём понятие арифметизации булевых формул. Пусть нам дана формула <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>\Phi varphi \land \Psi psi \to A_\Phi varphi \cdot A_\Psipsi</tex>;# <tex>\Phi varphi \lor \Psi psi \to 1 - (1 - A_\Phivarphi) \cdot (1 - A_\Psipsi)</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> {{---}} некоторая константа.
{{Лемма
|statement=<tex>\phi(x_1 \ldots x_m) = A_\phi(x_1, \ldots, x_m)</tex>.
|proof=
proof
}}
Введем обозначение: <tex>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)</tex>, где <tex>c_1, \ldots, c_i</tex> {{---}} некоторые константы.
{{Лемма
|about=2
|statement=
При введенных выше обозначениях выполняются:
# <tex>A_0(0) + A_0(1) = k</tex>
# <tex>\forall 1 \le i \le m: A_i(0) + A_i(1) = A_{i-1}(c_i)</tex>
|proof=
proof
}}
