Полнота системы тождеств
Система \(\tau\) является полной для эквивалентных преобразований формул над фиксированным базисом, если для любых эквивалентных F′ и F″ существует цепочка преобразований по подстановкам тождеств \(\tau\), переводящая F′ в F″. Требование существенно сильнее, чем просто истинность каждого тождества: система должна быть достаточной для всех эквивалентных формул класса.1
Стандартный базис \(\text{Б}_{0}\)
Для \(\text{Б}_{0}=\{\wedge,\vee,\neg \}\) курс выделяет систему основных тождеств \(\tau_{\text{осн}}\) и расширенную систему \(\tau\)eосн. Сначала показывается, что расширенные тождества выводимы из основных. Затем теорема 2.1 доказывает полноту \(\tau_{\text{осн}}\).1
В самой \(\tau_{\text{осн}}\) выбраны восемь базовых тождеств: правило де Моргана для конъюнкции, двойное отрицание, ассоциативность, коммутативность и отождествление для конъюнкции, дистрибутивность \(\wedge\) относительно \(\vee\), а также два тождества подстановки констант для \(\wedge\). Симметричные тождества для \(\vee\), остальные варианты дистрибутивности и подстановки констант, а также поглощение образуют расширенную систему и выводятся из \(\tau_{\text{осн}}\).1
Схема доказательства каноническая. Отрицания поднимают к переменным, раскрывают скобки, приводят подобные члены, устраняют противоречивые и поглощаемые конъюнкции и при необходимости дополняют их до совершенной формы. В результате эквивалентные формулы приводятся к одному каноническому представлению реализуемой функции. Поэтому одну формулу можно преобразовать в канонический вид, а затем обратными шагами — во вторую.
Различные базисы и теорема перехода
Пусть Б и Б′ — конечные полные базисы. Для каждой операции одного базиса выбирают формулу, реализующую её в другом, и получают системы тождеств перехода. Если \(\tau\) — конечная полная система для формул над Б, то после структурного моделирования тождеств \(\tau\) в Б′ и добавления моделированных тождеств обратного перехода получается конечная полная система для Б′. В обозначениях курса теорема 5.2 имеет вид: из \(\tau\) и систем перехода \(\Pi '\): \(\text{Б}\to\text{Б}'\) и \(\Pi\): \(\text{Б}'\to\text{Б}\) строится КПСТ \(\{\Pi'(\tau), \Pi'(\Pi)\}\) для формул над Б′.1
Смысл результата в том, что полнота эквивалентных преобразований не привязана только к стандартной записи \(\wedge,\vee,\neg\). При наличии взаимного функционального моделирования её можно конструктивно перенести в другой полный конечный базис.