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

Вопрос о существовании алгоритма, позволяющего для каждой конечной системы $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$

Ключевым моментом доказательства теоремы служит следующая [[math:discrete:lemma_f_x1_x2|лемма]].

Доказательство теоремы. На первом шаге при помощи [[math:discrete:lemma_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]$ и, в силу [[math:discrete:theorem_of_full_systems|теоремы о заведомо полныx системаx]], система $F$ является полной.

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