Алгоритм нормальных форм и его применения

Урок о нормальных формах дал два доказательства их существования. Первое проходит через таблицу истинности, в которой $2^n$ строк для $n$ переменных; второе обходит формулу от переменных, следуя единственному правилу её образования. Ни одно из них не говорит, как действовать перед формулой, записанной с импликациями, эквиваленциями и вложенными отрицаниями, а именно так обычно и предъявляются формулы. Если это так, недостаёт процедуры, которая работала бы с самой записью, могла бы выполняться не думая, о которой было бы известно, что она завершается и даёт эквивалентную формулу. Это и есть алгоритм, и его изучение составляет первый предмет этого урока; второй предмет составляет то, что с его помощью делается: описание формулами поведения устройства и построение схемы, которая его воспроизводит.

Записи и замена

Напомним, что формулы курса являются цепочками кружков и дисков и что $\neg$, $\vee$, $\wedge$, $\rightarrow$, $\leftrightarrow$ и $\veebar$ являются сокращениями, определёнными через стрелку Пирса (урок о языке логики высказываний). Когда мы пишем $((p \vee q) \rightarrow (\neg q \wedge p))$, мы пишем не цепочку, а запись этой цепочки: дерево, листья которого являются переменными, а узлы являются связками $\neg$, $\wedge$, $\vee$, $\rightarrow$, $\leftrightarrow$, $\veebar$ и $\downarrow$, каждая со своими компонентами. Всякая запись обозначает одну-единственную формулу, ту, что получается развёртыванием её сокращений; и одна и та же формула может иметь несколько записей: урок о нормальных формах заметил, что $\neg\neg\varphi$ и $(\varphi \vee \varphi)$ представляют собой одну и ту же цепочку. Алгоритм читает запись, а не цепочку; поэтому их полезно различать. Так как различие важно лишь для того, чтобы знать, где действует каждый шаг, мы будем употреблять буквы $\varphi$, $\psi$, $\chi$ для записей и для обозначаемых ими формул и будем писать $\varphi \eqsem \psi$, когда обозначаемые формулы семантически эквивалентны. Подзапись записи есть поддерево, растущее из одного из её узлов.

Шаг алгоритма заменяет одну подзапись другой. Инструментом, гарантирующим, что такая замена не меняет смысла, служит теорема о семантической замене из урока о семантическом следовании и эквивалентности; но та теорема заменяет одно вхождение в цепочке, а подзаписи может соответствовать несколько вхождений в цепочке, поскольку каждое сокращение копирует свои компоненты: в $(\varphi \vee \psi) = ((\varphi \downarrow \psi) \downarrow (\varphi \downarrow \psi))$ компонента $\varphi$ встречается дважды. Следующая лемма приспосабливает замену к записям.

Здесь $F_c$ есть функция истинности связки: $F_\neg(a) = 1 - a$, $F_\wedge(a, b) = ab$, и так для остальных. Тот же результат получается из теоремы о семантической замене, если применить её по одному разу к каждой копии $\theta$ в цепочке и связать эквивалентности транзитивностью; доказательство через запись короче, потому что считает написанные связки, а не копии.