Теорема об алгоритме распознавания полноты

Вопрос о существовании алгоритма, позволяющего для каждой конечной системы $F~=~{f_1,\dots ,f_s}$ функций из $\mathbb {P_k}$ выяснять, будет она полной или нет, является ключевым вопросом $k$-значных логик.

Теорема. Существует алгоритм распознавания полноты конечной системы $F~=~{f_1,\dots ,f_s}$ функций из $\mathbb {P_k}$.

Определение. Обозначим через $[F]_{x1,x2}$ множество всех функций из $[F]$, зависящих от переменных $x1,x2$

Ключевым моментом доказательства теоремы служит следующая .

Доказательство теоремы. На первом шаге при помощи мы строим классы $\Re_0, \Re_1,\dots , \Re_t$, до момента стабилизации, т.е. строим множество $[F]_{x1,x2} = \Re_t$.

На втором шаге по тому, содержится или нет функция Вебба в $[F]_{x1,x2}$, определяем, имеет ли место полнота для системы $F$.

{1} Если $V_k(x_1,x_2)\in [F]_{x1,x2}$ то $V_k(x_1,x_2)\in [F]$ и, в силу , система $F$ является полной.

{2} Если же $V_k(x_1,x_2)\notin [F]_{x1,x2}$, то $V_k(x_1,x_2)\notin [F]$. Следовательно, $F$ не полна.$~~~\square$