Перейти к содержимому
Topos Uranos
Русский

Семантика: итоги и задачи повышенной трудности

Краткое содержание

Этот урок завершает раздел, посвящённый семантике. Он восстанавливает дедуктивную цепь, которая ведёт от продолжения оценки на все формулы и от леммы о совпадении к следованию, к эквивалентности и к двум её рабочим теоремам, о замене и о равномерной подстановке; оттуда к законам для любого числа членов, к функциональной полноте и к системам связок, а оттуда к нормальным формам, к их алгоритму и к схемам, и указывает в каждом звене, какие результаты в нём используются и в каком уроке оно доказывается. Он отделяет то, что раздел доказал, от того, что раздел взял из предыдущих, тремя способами решает вопрос о рассуждении, которое курс проносит с первого раздела, и объясняет, почему вопрос, который раздел оставляет открытым, а именно совпадает ли истинное при всякой оценке с выводимым, ведёт к метатеории. В итоговой проверке он повторяет навыки входной проверки и заканчивается шестью задачами повышенной трудности, более сложными, чем задачи уроков, которые требуют соединять средства нескольких из них.

Цели обучения

  1. Восстанавливать логический порядок результатов раздела, указывая предыдущие результаты, на которые опирается каждый из них, и урок, в котором он доказывается.
  2. Объяснять, как рекурсивное продолжение, лемма о совпадении, семантическая замена и обобщённые законы ведут к функциональной полноте, к существованию нормальных форм и к корректности и завершаемости их алгоритма.
  3. Отделять то, что раздел доказал, от того, что он взял из предыдущих, и от того, что он оставил метатеории, в частности совпадение семантического следования с выводимостью и компактность.
  4. Решать задачи, в которых соединяются вычисление значений, следование, равномерная подстановка, системы связок, нормальные формы и схемы.

Чего достиг раздел

Раздел ставил целью придать значение формулам языка, построенного в первом разделе, не затрагивая дедуктивной системы второго, и получить из этого значения процедуры для решения вопросов, которые логика задаёт о формулах: общезначима ли формула, выполнима ли она, следует ли она из других, говорит ли она то же, что другая. Цель достигнута с немногими оговорками, каждая из которых сделана на своём месте: двузначность и истинностная функциональность, которые не доказываются, а выбираются и цену которых показал урок о формализации; однозначность разбора, определение по рекурсии, индукция и официальные сокращения, которые были доказаны или зафиксированы в первом разделе и здесь используются; и необходимый минимум о множествах и функциях, о котором напоминалось там, где он был нужен. С этими оговорками пройденный путь можно прочесть как одну дедуктивную цепь из шести участков, по одному на урок.

Значение формулы

Урок о семантике логики высказываний определил оценку как функцию из переменных в {0,1}\{0, 1\} и доказал с помощью теоремы об определении по рекурсии на формулах, что она единственным образом продолжается на все формулы с помощью одного-единственного пункта: v((φ↓ψ))=(1−v(φ))(1−v(ψ))v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi)). Из официальных сокращений он вычислил, ничего больше не постулируя, значение каждой производной связки, записанное как многочлен от значений компонент, а вместе с тем и таблицу импликации, которая здесь есть теорема. Он доказал индукцией по сложности лемму о совпадении, из которой следует, что таблица истинности из 2n2^{n} строк содержит всё, что бесконечно многие оценки говорят о формуле от nn переменных; определил выполнение, общезначимость, выполнимость, противоречие и нейтральность, уточнил, что ⊭φ\not\models \varphi говорит, что φ\varphi не общезначима, а не что она противоречива, зафиксировал ⊤:=(v1→v1)\top := (v_{1} \rightarrow v_{1}) и ⊥:=¬⊤\bot := \neg\top и получил разрешимость общезначимости и выполнимости ценой экспоненциальных затрат, которые направленный поиск опровергающей оценки уменьшает, но не устраняет.

Следование и эквивалентность

Урок о семантическом следовании и эквивалентности определил следование из множества посылок, конечного или бесконечного, и доказал, что оно обладает структурными свойствами вывода (рефлексивностью, монотонностью, сечением и транзитивностью), причём доказательства перебирают оценки, вместо того чтобы оперировать строками. Семантическая теорема о дедукции, Γ∪{φ}⊨ψ⇔Γ⊨(φ→ψ)\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi), свелась к единственной ложной строке импликации, а следование свелось к невыполнимости: Γ⊨φ⇔Γ∪{¬φ}\Gamma \models \varphi \Leftrightarrow \Gamma \cup \{\neg\varphi\} невыполнимо. Семантическая эквивалентность, определённая как равенство значений, оказалась совпадающей со взаимным следованием и с общезначимостью эквиваленции. Две её рабочие теоремы были доказаны индукцией по сложности: замена одного вхождения подформулы на эквивалентную ей, со случаем полного вхождения, который нельзя опускать, и равномерная подстановка произвольных формул вместо переменных, которая сохраняет общезначимость, эквивалентность и следование. С их помощью законы каталога, проверенные как тождества многочленов, применяются в любом месте любой формулы и выстраиваются в цепи.

Законы для любого числа членов

Урок об обобщённых законах де Моргана и дистрибутивности определил по рекурсии, с ассоциированием влево, конъюнкцию и дизъюнкцию nn формул и доказал индукцией по числу членов лемму о значении, которая утверждает, что конъюнкция истинна тогда и только тогда, когда истинны все её члены, а дизъюнкция тогда и только тогда, когда истинен хотя бы один. С её помощью и с помощью согласованности связок с эквивалентностью он получил обобщённую ассоциативность, доказанную цепью эквивалентностей, чтобы она была верна и для доказуемой эквивалентности, независимость от порядка и от повторений, обобщённые законы де Моргана и обобщённую дистрибутивность, индукция по двум индексам для которой была построена так, чтобы предположение индукции охватывало все длины второго списка; двойственный закон был получен по закону де Моргана, без повторения двойной индукции.

Функции истинности

Урок о функциональной полноте прошёл обратный путь, от таблицы к формуле. Он подсчитал функции истинности от nn аргументов (их 22n2^{2^{n}}), показал, что каждая формула представляет ровно одну из них и что две формулы эквивалентны тогда и только тогда, когда представляют одну и ту же, и доказал теорему о функциональной полноте: конъюнкция строки истинна в точности в своей строке, а дизъюнкция конъюнкций тех строк, в которых функция равна 11, её представляет. Поскольку эта формула есть цепочка кружков и дисков, одной стрелки Пирса достаточно; по критерию стрелки Пирса достаточно также {¬,∧}\{\neg, \wedge\}, {¬,∨}\{\neg, \vee\}, {¬,→}\{\neg, \rightarrow\} и штриха Шеффера; а по принципу замыкания все формулы над {∧,∨,→,↔}\{\wedge, \vee, \rightarrow, \leftrightarrow\} сохраняют 11, так что этой системы недостаточно.

Нормальные формы

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

Алгоритм и схемы

Урок об алгоритме нормальных форм и его применениях превратил второе доказательство существования в процедуру, которая действует на записи: исключить связки, отличные от ¬\neg, ∧\wedge и ∨\vee, довести отрицания до переменных и распределить. Он доказал его корректность с помощью замены в записи, которая приспосабливает теорему о замене к сокращениям, и его завершаемость с помощью трёх мер, которые убывают на каждом шаге и последняя из которых читает конъюнкцию как произведение; он доказал также, что конъюнктивная форма формулы ⋁i=1n(pi∧qi)\bigvee_{i=1}^{n} (p_i \wedge q_i) необходимо имеет 2n2^{n} дизъюнктов, так что рост не есть недостаток алгоритма. Затем он получил нормальные формы чёрного ящика по его таблице, сократил их, склеивая соседние строки, и превратил их в схемы из переключателей, проводимость которых есть значение их формулы.

Следующий рисунок соединяет шесть участков в одну цепь. Каждый узел столбца есть определение или результат, пронумерованный в логическом порядке и соединённый дугой с предыдущими звеньями, которые использует его доказательство; вокруг расположены опоры, то есть принципы и средства, к которым цепь обращается снова и снова, и каждая соединена сплошной линией со звеньями, которые на неё опираются, и пунктирной со звеном, где она устанавливается, кроме тех, которые эта цепь не доказывает (однозначность разбора вместе с рекурсией, индукция и официальные сокращения из первого раздела): они изображены кольцами. Нажатие на опору выделяет все звенья, которые её используют, а каждое звено ведёт к уроку, где оно доказывается. Заметим, что индукция и значения связок являются опорами, к которым раздел обращается чаще всего, и что лемма о значении, хотя она доказывается в третьем уроке, поддерживает почти всё, что три последних урока говорят о конъюнкциях и дизъюнкциях.

Опоры цепи

  • AОднозначность разбора и рекурсия. Если ∙φψ=∙φ′ψ′\sigI\varphi\psi = \sigI\varphi'\psi', причём все четыре цепочки являются формулами, то φ=φ′\varphi = \varphi' и ψ=ψ′\psi = \psi'; откуда правило, которое вычисляет значение ∙φψ\sigI\varphi\psi по φ\varphi, по ψ\psi и по их значениям, определяет единственную функцию на формулах. Доказано в первом разделе. В этом модуле принимается без доказательства.
  • BИндукция. Простая и сильная по натуральным числам, а также по сложности формул, единственными случаями которой являются переменные и стрелка Пирса (φ↓ψ)(\varphi \downarrow \psi). Доказана в первом разделе. В этом модуле принимается без доказательства.
  • CОфициальные сокращения. ¬φ:=(φ↓φ)\neg\varphi := (\varphi \downarrow \varphi), (φ∨ψ):=¬(φ↓ψ)(\varphi \vee \psi) := \neg(\varphi \downarrow \psi), (φ∧ψ):=¬(¬φ∨¬ψ)(\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi), (φ→ψ):=(¬φ∨ψ)(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi), (φ↔ψ):=((φ→ψ)∧(ψ→φ))(\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)) и (φ⊻ψ):=¬(φ↔ψ)(\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi). Зафиксированы в первом разделе. В этом модуле принимается без доказательства.
  • DЗначения связок. При a=v(φ)a = v(\varphi) и b=v(ψ)b = v(\psi): v(¬φ)=1−av(\neg\varphi) = 1 - a, v((φ∨ψ))=a+b−abv((\varphi \vee \psi)) = a + b - ab, v((φ∧ψ))=abv((\varphi \wedge \psi)) = ab, v((φ→ψ))=1−a(1−b)v((\varphi \rightarrow \psi)) = 1 - a(1 - b), v((φ↔ψ))=ab+(1−a)(1−b)v((\varphi \leftrightarrow \psi)) = ab + (1 - a)(1 - b) и v((φ⊻ψ))=a+b−2abv((\varphi \veebar \psi)) = a + b - 2ab, где a2=aa^{2} = a. Устанавливается в: 1. Продолжение оценки.
  • EЛемма о совпадении. Если две оценки совпадают на переменных φ\varphi, они дают φ\varphi одно и то же значение; поэтому таблица из 2n2^{n} строк говорит всё. Устанавливается в: 2. Лемма о совпадении и таблицы.
  • FСемантическая замена. Если θ≡θ′\theta \eqsem \theta' и χ′\chi' получается заменой в χ\chi одного вхождения θ\theta на θ′\theta', то χ≡χ′\chi \eqsem \chi'. Устанавливается в: 7. Теорема о семантической замене.
  • GЗаконы эквивалентности. Двойное отрицание, идемпотентность, коммутативность, ассоциативность, дистрибутивность, законы де Моргана, поглощение, тождество, доминирование, исключённое третье и непротиворечие, для произвольных формул. Устанавливается в: 9. Законы эквивалентности.
  • HЛемма о значении. v(⋀i=1nφi)=1v\left( \bigwedge_{i=1}^{n} \varphi_i \right) = 1 тогда и только тогда, когда v(φi)=1v(\varphi_i) = 1 для всех ii; v(⋁i=1nφi)=1v\left( \bigvee_{i=1}^{n} \varphi_i \right) = 1 тогда и только тогда, когда v(φi)=1v(\varphi_i) = 1 для некоторого ii. Устанавливается в: 10. Лемма о значении и согласованность.

  1. Участок 1 Значение формулы

    • Вычислять значение формулы по пункту для стрелки Пирса и получать из сокращений значение каждой производной связки.
    • Доказывать лемму о совпадении и обосновывать с её помощью, что таблицы из 2n2^{n} строк достаточно.
    • Классифицировать формулы и множества, не путая ⊭φ\not\models \varphi с противоречием, и решать вопрос об общезначимости, ища опровергающую оценку.

    1. Продолжение оценки. Каждая оценка vv единственным образом продолжается на все формулы с помощью пункта v((φ↓ψ))=(1−v(φ))(1−v(ψ))v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi)); раскрывая сокращения, вычисляют значение ¬\neg, ∨\vee, ∧\wedge, →\rightarrow, ↔\leftrightarrow и ⊻\veebar.

      Опирается на: A (Однозначность разбора и рекурсия), C (Официальные сокращения). Доказывается в уроке: Семантика логики высказываний.

    2. Лемма о совпадении и таблицы. Если vv и v′v' совпадают на V(φ)V(\varphi), то v(φ)=v′(φ)v(\varphi) = v'(\varphi), индукцией по сложности; откуда значения φ\varphi при всех оценках являются в точности значениями в 2n2^{n} строках её таблицы.

      Использует: 1. Продолжение оценки. Опирается на: B (Индукция). Доказывается в уроке: Семантика логики высказываний.

    3. Классификация и разрешение. Каждая формула есть ровно одно из трёх: общезначимая, нейтральная или противоречие; φ\varphi общезначима тогда и только тогда, когда ¬φ\neg\varphi есть противоречие, и есть противоречие тогда и только тогда, когда ⊨¬φ\models \neg\varphi. ⊤\top и исключённое третье общезначимы, ⊥\bot есть противоречие, а общезначимость и выполнимость разрешаются перебором строк.

      Опирается на: D (Значения связок), E (Лемма о совпадении). Доказывается в уроке: Семантика логики высказываний.

  2. Участок 2 Следование и эквивалентность

    • Решать вопросы о следовании из конечных или бесконечных множеств, предъявляя контрмодель или доказывая, что её нет.
    • Применять семантическую теорему о дедукции и сведение следования к невыполнимости.
    • Отличать замену одного вхождения от равномерной подстановки и доказывать обе индукцией по сложности.
    • Устанавливать эквивалентности цепями, правильно называя каждый закон.

    1. Следование и его свойства. Γ⊨φ\Gamma \models \varphi, если всякая оценка, выполняющая Γ\Gamma, выполняет φ\varphi; ∅⊨φ\emptyset \models \varphi тогда и только тогда, когда ⊨φ\models \varphi; верны рефлексивность, монотонность, сечение и транзитивность, и невыполнимое множество имеет своим следствием любую формулу.

      Использует: 3. Классификация и разрешение. Доказывается в уроке: Семантическое следование и эквивалентность.

    2. Семантическая дедукция и невыполнимость. Γ∪{φ}⊨ψ⇔Γ⊨(φ→ψ)\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi) по единственной ложной строке импликации; {φ1,…,φn}⊨ψ⇔  ⊨(φ1→(φ2→⋯(φn→ψ)⋯ ))\{\varphi_1, \ldots, \varphi_n\} \models \psi \Leftrightarrow\; \models (\varphi_1 \rightarrow (\varphi_2 \rightarrow \cdots (\varphi_n \rightarrow \psi) \cdots)); и Γ⊨φ\Gamma \models \varphi тогда и только тогда, когда Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} невыполнимо.

      Использует: 4. Следование и его свойства. Опирается на: D (Значения связок). Доказывается в уроке: Семантическое следование и эквивалентность.

    3. Семантическая эквивалентность. φ≡ψ\varphi \eqsem \psi тогда и только тогда, когда φ⊨ψ\varphi \models \psi и ψ⊨φ\psi \models \varphi, и тогда и только тогда, когда ⊨(φ↔ψ)\models (\varphi \leftrightarrow \psi); эквивалентность рефлексивна, симметрична и транзитивна, и две эквивалентные формулы равноправны как посылки и как заключения.

      Использует: 4. Следование и его свойства. Опирается на: D (Значения связок). Доказывается в уроке: Семантическое следование и эквивалентность.

    4. Теорема о семантической замене. Если θ≡θ′\theta \eqsem \theta', то замена в χ\chi одного вхождения θ\theta на θ′\theta', включая полное вхождение, даёт формулу, эквивалентную χ\chi; и то же даёт одновременная подстановка во все вхождения.

      Использует: 1. Продолжение оценки, 6. Семантическая эквивалентность. Опирается на: A (Однозначность разбора и рекурсия), B (Индукция). Доказывается в уроке: Семантическое следование и эквивалентность.

    5. Равномерная подстановка. Если w(vn)=v(σ(vn))w(v_n) = v(\sigma(v_n)), то v(σ(χ))=w(χ)v(\sigma(\chi)) = w(\chi); откуда, если ⊨χ\models \chi, то и ⊨σ(χ)\models \sigma(\chi), а подстановка сохраняет эквивалентность и следование, но не выполнимость и не нейтральность.

      Использует: 1. Продолжение оценки, 4. Следование и его свойства, 6. Семантическая эквивалентность. Опирается на: A (Однозначность разбора и рекурсия), B (Индукция). Доказывается в уроке: Семантическое следование и эквивалентность.

    6. Законы эквивалентности. Законы каталога проверяются как тождества многочленов при a2=aa^{2} = a; с помощью замены и транзитивности они применяются к подформулам и выстраиваются в цепи.

      Использует: 3. Классификация и разрешение, 6. Семантическая эквивалентность. Опирается на: D (Значения связок), F (Семантическая замена). Доказывается в уроке: Семантическое следование и эквивалентность.

  3. Участок 3 Законы для любого числа членов

    • Раскрывать конъюнкции и дизъюнкции из nn членов как цепочки, ассоциированные влево, и вычислять их значение.
    • Доказывать индукцией по числу членов обобщённую ассоциативность, независимость от порядка и обобщённые законы де Моргана.
    • Доказывать обобщённую дистрибутивность индукцией по двум индексам и подсчитывать члены, которые она даёт.

    1. Лемма о значении и согласованность. Если α≡α′\alpha \eqsem \alpha' и β≡β′\beta \eqsem \beta', то ¬α≡¬α′\neg\alpha \eqsem \neg\alpha', (α∧β)≡(α′∧β′)(\alpha \wedge \beta) \eqsem (\alpha' \wedge \beta') и (α∨β)≡(α′∨β′)(\alpha \vee \beta) \eqsem (\alpha' \vee \beta'); конъюнкция из nn членов равна 11 тогда и только тогда, когда все члены равны 11, дизъюнкция тогда и только тогда, когда хотя бы один равен 11, и эквивалентные члены дают эквивалентные конъюнкции и дизъюнкции.

      Использует: 6. Семантическая эквивалентность. Опирается на: D (Значения связок), B (Индукция). Доказывается в уроке: Обобщённые законы де Моргана и дистрибутивности.

    2. Ассоциативность и порядок. Конъюнкция конъюнкций двух списков эквивалентна конъюнкции их конкатенации, и всякая группировка эквивалентна ассоциированной влево; два списка с одними и теми же членами дают эквивалентные конъюнкции и дизъюнкции, каковы бы ни были порядок и повторения.

      Опирается на: H (Лемма о значении), G (Законы эквивалентности), B (Индукция). Доказывается в уроке: Обобщённые законы де Моргана и дистрибутивности.

    3. Обобщённые законы де Моргана. ¬⋀i=1nφi≡⋁i=1n¬φi\neg \bigwedge_{i=1}^{n} \varphi_i \eqsem \bigvee_{i=1}^{n} \neg\varphi_i и ¬⋁i=1nφi≡⋀i=1n¬φi\neg \bigvee_{i=1}^{n} \varphi_i \eqsem \bigwedge_{i=1}^{n} \neg\varphi_i: закон для двух членов применяется к последнему соединению, а предположение индукции к тому, что остаётся внутри.

      Опирается на: H (Лемма о значении), G (Законы эквивалентности), B (Индукция). Доказывается в уроке: Обобщённые законы де Моргана и дистрибутивности.

    4. Обобщённая дистрибутивность. (⋁i=1nφi)∧(⋁j=1mψj)≡⋁i,j(φi∧ψj)\left( \bigvee_{i=1}^{n} \varphi_i \right) \wedge \left( \bigvee_{j=1}^{m} \psi_j \right) \eqsem \bigvee_{i,j} (\varphi_i \wedge \psi_j), с nmnm членами в лексикографическом порядке; и двойственный закон, который распределяет дизъюнкцию двух конъюнкций, по закону де Моргана.

      Использует: 11. Ассоциативность и порядок, 12. Обобщённые законы де Моргана. Опирается на: H (Лемма о значении), G (Законы эквивалентности), B (Индукция). Доказывается в уроке: Обобщённые законы де Моргана и дистрибутивности.

  4. Участок 4 Функции истинности

    • Подсчитывать функции истинности и решать вопрос об эквивалентности, сравнивая функции, которые представляют две формулы.
    • Строить формулу таблицы и записывать любую функцию одной лишь стрелкой Пирса.
    • Доказывать полноту системы связок по критерию стрелки Пирса или её неполноту с помощью свойства, которое сохраняют её формулы.

    1. Функции истинности. Существует 22n2^{2^{n}} функций истинности от nn аргументов; формула с переменными среди v1,…,vnv_1, \ldots, v_n представляет ровно одну из них, fφf_\varphi, и φ≡ψ⇔fφ=fψ\varphi \eqsem \psi \Leftrightarrow f_\varphi = f_\psi.

      Использует: 6. Семантическая эквивалентность. Опирается на: E (Лемма о совпадении). Доказывается в уроке: Функциональная полнота.

    2. Функциональная полнота. Конъюнкция строки равна 11 в точности в своей строке; дизъюнкция конъюнкций тех строк, в которых ff равна 11, или (v1∧¬v1)(v_{1} \wedge \neg v_{1}), если таких строк нет, представляет ff; и всякая формула эквивалентна формуле своей таблицы.

      Использует: 14. Функции истинности. Опирается на: H (Лемма о значении), D (Значения связок). Доказывается в уроке: Функциональная полнота.

    3. Полные и неполные системы. Стрелки Пирса достаточно, потому что сокращения раскрываются; если формулы над KK выражают значение (1−a)(1−b)(1 - a)(1 - b), то система KK полна, как {¬,∧}\{\neg, \wedge\}, {¬,∨}\{\neg, \vee\}, {¬,→}\{\neg, \rightarrow\} и {↑}\{\uparrow\}; формулы над {∧,∨,→,↔}\{\wedge, \vee, \rightarrow, \leftrightarrow\} равны 11, когда все переменные равны 11, и эта система не полна.

      Использует: 15. Функциональная полнота. Опирается на: C (Официальные сокращения), B (Индукция), D (Значения связок). Доказывается в уроке: Функциональная полнота.

  5. Участок 5 Нормальные формы

    • Распознавать литералы, дизъюнкты и нормальные формы, отличая форму цепочки от её значения.
    • Строить совершенные нормальные формы по таблице и доказывать их единственность.
    • Доказывать индукцией существование нормальных форм с предположением индукции, которое требует обеих.
    • Решать с первого взгляда вопрос об общезначимости конъюнктивной формы и о выполнимости дизъюнктивной.

    1. Литералы и двойственность. ¬ℓ≡ℓ∗\neg\ell \eqsem \ell^{*}; элементарная конъюнкция выполнима тогда и только тогда, когда не содержит контрарной пары, а дизъюнкт общезначим тогда и только тогда, когда содержит её; отрицание нормальной формы эквивалентно двойственной к ней, так что конъюнктивная форма формулы φ\varphi есть форма, двойственная к дизъюнктивной форме формулы ¬φ\neg\varphi.

      Использует: 12. Обобщённые законы де Моргана. Опирается на: G (Законы эквивалентности), F (Семантическая замена), H (Лемма о значении). Доказывается в уроке: Нормальные формы.

    2. Совершенные нормальные формы. Если φ\varphi выполнима, она эквивалентна своей совершенной дизъюнктивной нормальной форме, а если не общезначима, то совершенной конъюнктивной; при фиксированных переменных v1,…,vnv_1, \ldots, v_n две совершенные нормальные формы эквивалентны тогда и только тогда, когда они являются одной и той же цепочкой, и две выполнимые формулы эквивалентны тогда и только тогда, когда у них одна и та же совершенная дизъюнктивная нормальная форма.

      Использует: 15. Функциональная полнота, 17. Литералы и двойственность. Опирается на: H (Лемма о значении), E (Лемма о совпадении). Доказывается в уроке: Нормальные формы.

    3. Существование индукцией. (φ↓ψ)≡(¬φ∧¬ψ)(\varphi \downarrow \psi) \eqsem (\neg\varphi \wedge \neg\psi); нормальные формы сохраняются при взятии конъюнкции и дизъюнкции, дизъюнктивная форма конъюнкции и конъюнктивная форма дизъюнкции по обобщённой дистрибутивности; по индукции, с предположением индукции об обеих формах, всякая формула имеет дизъюнктивную и конъюнктивную форму.

      Использует: 17. Литералы и двойственность, 11. Ассоциативность и порядок, 13. Обобщённая дистрибутивность. Опирается на: B (Индукция), F (Семантическая замена). Доказывается в уроке: Нормальные формы.

    4. Что видно с первого взгляда. Конъюнктивная форма общезначима тогда и только тогда, когда каждый её дизъюнкт содержит контрарную пару; дизъюнктивная форма выполнима тогда и только тогда, когда некоторая элементарная конъюнкция не содержит ни одной.

      Использует: 17. Литералы и двойственность. Опирается на: H (Лемма о значении). Доказывается в уроке: Нормальные формы.

  6. Участок 6 Алгоритм и схемы

    • Применять алгоритм переписывания и выбирать подходящее исключение эквиваленции.
    • Доказывать его корректность и завершаемость и объяснять, почему конъюнктивная форма может расти экспоненциально.
    • Получать и упрощать нормальные формы чёрного ящика и строить по ним схемы из переключателей.

    1. Корректность и завершаемость алгоритма. Замена подзаписи на эквивалентную даёт эквивалентную запись; каждое правило есть эквивалентность, и неприводимая запись есть нормальная форма с той или иной группировкой; меры M1M_1, M2M_2, при M2(¬φ)=2M2(φ)M_2(\neg\varphi) = 2^{M_2(\varphi)}, и M3M_3, при M3(φ∧ψ)=M3(φ) M3(ψ)M_3(\varphi \wedge \psi) = M_3(\varphi)\,M_3(\psi), убывают на каждом шаге.

      Использует: 19. Существование индукцией, 11. Ассоциативность и порядок. Опирается на: G (Законы эквивалентности), D (Значения связок), B (Индукция). Доказывается в уроке: Алгоритм нормальных форм и его применения.

    2. Экспоненциальный рост. ⋁i=1n(pi∧qi)\bigvee_{i=1}^{n} (p_i \wedge q_i) эквивалентна конъюнктивной форме из 2n2^{n} дизъюнктов, и всякая эквивалентная ей конъюнктивная форма имеет не менее 2n2^{n} необщезначимых дизъюнктов.

      Использует: 19. Существование индукцией, 17. Литералы и двойственность. Опирается на: H (Лемма о значении). Доказывается в уроке: Алгоритм нормальных форм и его применения.

    3. Соседние строки и схемы. (κ∧ℓ)∨(κ∧ℓ∗)≡κ(\kappa \wedge \ell) \vee (\kappa \wedge \ell^{*}) \eqsem \kappa и двойственная эквивалентность; параллельно-последовательная схема проводит в состоянии vv тогда и только тогда, когда v(φC)=1v(\varphi_C) = 1, и всякую функцию истинности реализует некоторая схема.

      Использует: 15. Функциональная полнота, 18. Совершенные нормальные формы, 17. Литералы и двойственность, 11. Ассоциативность и порядок. Опирается на: G (Законы эквивалентности), F (Семантическая замена), D (Значения связок), B (Индукция). Доказывается в уроке: Алгоритм нормальных форм и его применения.

К метатеории. Цепь останавливается там, где семантика располагает процедурой для каждого вопроса о формулах. Остаётся узнать, совпадает ли то, что истинно при всякой оценке, в точности с тем, что выводится в системе: следующий раздел сравнит оба понятия.