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

Метатеория: итоги и задачи повышенной трудности

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

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

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

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

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

Раздел поставил целью сравнить два отношения, которые предыдущие разделы построили на одном и том же языке, выводимость Γ⊢φ\Gamma \vdash \varphi и семантическое следование Γ⊨φ\Gamma \models \varphi, и доказать, что они совпадают. Эта цель достигнута без оговорок в формулировках: оба отношения суть одно и то же для всякого множества посылок, конечного или бесконечного, а резолюция даёт третий способ, столь же корректный и полный, решать вопрос о следовании. Оговорки касаются методов, и каждая была сделана в своём месте: полнота из первого урока конструктивна, но не практична, поскольку даёт выводы такой же длины, как таблица; компактность гарантирует, что оценка существует, но не учит её находить; а резолюция решает вопрос, но её стоимость в худшем случае остаётся открытым вопросом. С этими оговорками пройденный путь можно прочесть как одну дедуктивную цепь из четырёх участков.

Корректность

Урок о корректности и полноте начал с того, что зафиксировал терминологию: система корректна, если Γ⊢φ⇒Γ⊨φ\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi, и полна, если верно обратное, причём в трёх степенях (слабая, для конечных множеств и сильная). Он разобрал круговое рассуждение, которое пытается получить полноту «из корректности», переходя от ⊬χ\nvdash \chi к ⊭χ\not\models \chi, тогда как этот переход есть контрапозиция слабой полноты, и показал, что оба свойства независимы. Затем он доказал, что всякий частный случай A1, A2 и A3 общезначим, предположив оценку, которая его опровергает, и придя через ложную строку импликации к невозможным значениям; и сильной индукцией по числу строк доказал корректность, с одним случаем для аксиом, другим для посылок, семантическим modus ponens и, для правила замены двойного отрицания, эквивалентностью θ≡¬¬θ\theta \eqsem \neg\neg\theta вместе с теоремой о семантической замене. Свойство, которое передаётся от строки к строке, есть не общезначимость, а выполнимость при фиксированной оценке, выполняющей посылки, и поэтому корректность имеет место и при посылках, в том числе бесконечных. Из неё получились непротиворечивость всякого выполнимого множества, в частности самой системы, и метод, которого не было у раздела о выводе: контрмодель доказывает, что вывода не существует.

Кальмар и конечная полнота

Тот же урок доказал обратное утверждение в два шага. Первый шаг есть лемма Кальмара: если переменные формулы φ\varphi находятся среди u1,…,unu_{1}, \ldots, u_{n}, то {u1v,…,unv}⊢φv\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v} для всякой оценки vv, где ψv\psi^{v} есть ψ\psi, если v(ψ)=1v(\psi) = 1, и ¬ψ\neg\psi в противном случае; система выводит из каждой строки то, что эта строка говорит о формуле. Её индукция по сложности имеет лишь один составной случай, (α↓β)(\alpha \downarrow \beta), поскольку стрелка Пирса является единственной исходной связкой, а в нём три подслучая, которые требуют двух лемм системы, второй в двух формах: ⊢(¬α→(¬β→(α↓β)))\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta))), выводимой с помощью введения конъюнкции, двойного отрицания и двух применений правила ЗДО, а также ⊢(α→¬(α↓β))\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta)) и ⊢(β→¬(α↓β))\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta)), выводимых с помощью введения дизъюнкции. Второй шаг устраняет посылки: если φ\varphi есть тавтология, она выводится из посылок всех 2n2^{n} строк, и разбор случаев устраняет литерал последней переменной, затем предпоследней и так далее, пока не будет получено ⊢φ\vdash \varphi, то есть слабая полнота. С помощью семантической теоремы о дедукции и обращения синтаксической полнота была распространена на конечные множества посылок; откуда для конечных посылок вывод и следование совпадают, доказуемая эквивалентность совпадает с семантической, а выводимость разрешима, поскольку за неё отвечает таблица.

Компактность и сильная полнота

Урок о теореме компактности занялся бесконечным случаем, которого лемма Кальмара не достигает, поскольку бесконечное число посылок нельзя перенести в импликацию. Он доказал, не упоминая никакого вывода, что множество выполнимо тогда и только тогда, когда выполнимо каждое из его конечных подмножеств. Последовательность значений для v1,…,vnv_{1}, \ldots, v_{n} хорошая, если всякое конечное подмножество множества выполняется некоторой оценкой, которая её продолжает; лемма о двух свидетелях гарантирует, что хорошая последовательность продолжается до хорошей, поскольку, если бы ни одно из двух продолжений не было хорошим, объединение двух конечных свидетелей противоречило бы тому, что последовательность хорошая; а оценка, которая получается, если всегда предпочитать 11, когда это возможно, выполняет каждую формулу по лемме о совпадении, поскольку каждая формула содержит конечное число переменных. Построение не нуждается в аксиоме выбора, поскольку переменные занумерованы и у каждого шага есть правило. Из компактности последовали её эквивалентные формы, форма невыполнимости и форма следования; из последней, из полноты для конечных посылок и из монотонности, сильная полнота; а из неё и из корректности полное совпадение: Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi для всякого Γ\Gamma, и множество непротиворечиво тогда и только тогда, когда оно выполнимо. Урок предупредил, что этот порядок не есть дело вкуса: получать компактность из сильной полноты, которой ещё нет, было бы порочным кругом. Он завершился раскраской счётных графов, которая переводит бесконечную задачу в множество формул, конечные части которого выполнимы, и пределами того, что может выразить множество формул.

Резолюция

Урок о методе резолюций заменил множества формул множествами дизъюнктов, каждый из которых есть конечное множество литералов, с двумя представлениями: клаузальной формой, у которой те же модели, и определительной формой, которая вводит новую переменную для каждой составной подзаписи, сохраняет лишь выполнимость и растёт как формула, а не как степень двойки. На дизъюнкты действует одно-единственное правило: из CC и DD, где ℓ∈C\ell \in C и ℓ∗∈D\ell^{*} \in D, выводится (C∖{ℓ})∪(D∖{ℓ∗})(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\}), а опровержение есть порождение, которое приходит к □\Box. Корректность была доказана так же, как корректность системы, индукцией по порождению, с резольвентой как следствием её посылок; полнота опровержения доказана индукцией по числу переменных, с помощью исключения переменной, которое сохраняет выполнимость и доказательство которого строит модель; а для бесконечных множеств снова с помощью компактности. Отсюда получилось, что Γ⊨φ\Gamma \models \varphi тогда и только тогда, когда клаузальная форма множества Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} имеет опровержение, и что насыщение, конечное, поскольку при nn переменных дизъюнктов не больше 4n4^{n}, решает вопрос о выполнимости без таблиц. Урок изложил проблему выполнимости, стоимость решения которой в худшем случае никому не известна, и два случая, решаемых быстро: дизъюнкты Хорна и дизъюнкты из двух литералов.

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

Опоры цепи

  • AИндукция и рекурсия. Сильная индукция по натуральным числам, индукция по сложности формул, с единственным составным случаем (α↓β)(\alpha \downarrow \beta), и определение рекурсией. Доказаны в первом разделе. В этом модуле принимается без доказательства.
  • BСистема курса. A1, A2 и A3, modus ponens и правило ЗДО; рефлексивность, монотонность, modus ponens для выводов, конечность и Γ∪{φ}⊢ψ⇔Γ⊢(φ→ψ)\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi). Зафиксированы во втором разделе. В этом модуле принимается без доказательства.
  • CПроизводные приёмы. Двойное отрицание из урока о четырёх приёмах; введение конъюнкции и дизъюнкции и разбор случаев (если Γ∪{ψ}⊢χ\Gamma \cup \{\psi\} \vdash \chi и Γ∪{¬ψ}⊢χ\Gamma \cup \{\neg\psi\} \vdash \chi, то Γ⊢χ\Gamma \vdash \chi) из урока о приёмах классической логики. Доказаны во втором разделе. В этом модуле принимается без доказательства.
  • DОценки и совпадение. v((α↓β))=(1−v(α))(1−v(β))v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta)); если две оценки совпадают на V(φ)V(\varphi), они придают φ\varphi одно и то же значение; общезначимость устанавливается по 2n2^{n} строкам. Доказаны в третьем разделе. В этом модуле принимается без доказательства.
  • EСемантическое следование. Ложная строка импликации, монотонность, Γ∪{φ}⊨ψ⇔Γ⊨(φ→ψ)\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi), Γ⊨φ\Gamma \models \varphi тогда и только тогда, когда Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} невыполнимо, и теорема о семантической замене. Доказаны в третьем разделе. В этом модуле принимается без доказательства.
  • FКонъюнктивные формы. Лемма о значении; всякая формула эквивалентна конъюнктивной нормальной форме, которой может потребоваться 2n2^{n} дизъюнктов; дизъюнкция литералов общезначима тогда и только тогда, когда содержит контрарную пару. Доказаны в третьем разделе. В этом модуле принимается без доказательства.
  • GКорректность. Если Γ⊢φ\Gamma \vdash \varphi, то Γ⊨φ\Gamma \models \varphi, для всякого множества Γ\Gamma; контрмодель доказывает, что вывода не существует. Устанавливается в: 2. Корректность.
  • HКомпактность. Множество формул выполнимо тогда и только тогда, когда выполнимо всякое его конечное подмножество; откуда невыполнимое множество невыполнимо уже в некоторой конечной части. Устанавливается в: 11. Теорема компактности.

  1. Участок 1 Корректность

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

    1. Общезначимость аксиом. Всякий частный случай A1, A2 и A3 общезначим: оценка, которая бы его опровергала, требовала бы через ложную строку импликации невозможных значений.

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

    2. Корректность. Если Γ⊢φ\Gamma \vdash \varphi, то Γ⊨φ\Gamma \models \varphi, для всякого Γ\Gamma: сильной индукцией по числу строк, с одним случаем для аксиом, другим для посылок, семантическим modus ponens и, для правила ЗДО, эквивалентностью θ≡¬¬θ\theta \eqsem \neg\neg\theta вместе с семантической заменой.

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

    3. Непротиворечивость и контрмодели. Всякое выполнимое множество непротиворечиво; система непротиворечива и ⊬v1\nvdash v_{1}; если оценка выполняет Γ\Gamma и опровергает φ\varphi, то Γ⊬φ\Gamma \nvdash \varphi, и таблица удостоверяет, что то, что не общезначимо, не есть теорема.

      Опирается на: G (Корректность), D (Оценки и совпадение). Доказывается в уроке: Корректность и полнота.

  2. Участок 2 Кальмар и конечная полнота

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

    1. Введение стрелки Пирса. {¬α,¬β}⊢(α↓β)\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta) и ⊢(¬α→(¬β→(α↓β)))\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta))): конъюнкция отрицаний есть ¬¬(¬¬α↓¬¬β)\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta); двойное отрицание снимает внешнее, а правило ЗДО два внутренних.

      Опирается на: B (Система курса), C (Производные приёмы). Доказывается в уроке: Корректность и полнота.

    2. Отрицание стрелки Пирса. ⊢(α→¬(α↓β))\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta)) и ⊢(β→¬(α↓β))\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta)), поскольку ¬(α↓β)\neg(\alpha \downarrow \beta) есть (α∨β)(\alpha \vee \beta) и достаточно введения дизъюнкции.

      Опирается на: B (Система курса), C (Производные приёмы). Доказывается в уроке: Корректность и полнота.

    3. Лемма Кальмара. Если V(φ)⊆{u1,…,un}V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}, то {u1v,…,unv}⊢φv\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v} для всякой оценки vv; шаг индукции имеет лишь один случай, (α↓β)(\alpha \downarrow \beta), с тремя подслучаями в зависимости от значений α\alpha и β\beta.

      Использует: 4. Введение стрелки Пирса, 5. Отрицание стрелки Пирса. Опирается на: A (Индукция и рекурсия), D (Оценки и совпадение), B (Система курса). Доказывается в уроке: Корректность и полнота.

    4. Слабая полнота. Если ⊨φ\models \varphi, то ⊢φ\vdash \varphi: лемма Кальмара выводит φ\varphi из каждой строки, а разбор случаев устраняет литералы от последней переменной к первой, с 2n2^{n} применениями леммы и 2n−12^{n} - 1 применениями разбора случаев.

      Использует: 6. Лемма Кальмара. Опирается на: C (Производные приёмы). Доказывается в уроке: Корректность и полнота.

    5. Полнота для конечных посылок. {γ1,…,γk}⊨φ⇒{γ1,…,γk}⊢φ\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi: семантическая теорема о дедукции приводит к тавтологии, слабая полнота её выводит, а обращение теоремы о дедукции возвращает посылки.

      Использует: 7. Слабая полнота. Опирается на: E (Семантическое следование), B (Система курса). Доказывается в уроке: Корректность и полнота.

    6. Конечное совпадение и разрешимость. Для конечного Γ\Gamma Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi и φ⊣⊢ψ⇔φ≡ψ\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi; откуда выводимость из конечных посылок разрешима с помощью таблицы.

      Использует: 8. Полнота для конечных посылок. Опирается на: G (Корректность), D (Оценки и совпадение). Доказывается в уроке: Корректность и полнота.

  3. Участок 3 Компактность и сильная полнота

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

    1. Лемма о двух свидетелях. Если последовательность ss зафиксированных значений хорошая (всякое конечное подмножество множества выполняется оценкой, которая её продолжает), то хорошая (s,1)(s, 1) или (s,0)(s, 0): если бы ни одна не была хорошей, объединение двух конечных свидетелей противоречило бы тому, что ss хорошая.

      Опирается на: D (Оценки и совпадение). Доказывается в уроке: Теорема компактности.

    2. Теорема компактности. Γ\Gamma выполнимо тогда и только тогда, когда выполнимо всякое конечное подмножество: vn+1v_{n + 1} полагается равным 11, если (sn,1)(s_{n}, 1) хорошая, и равным 00 в противном случае, и получившаяся оценка выполняет каждую формулу по лемме о совпадении. Аксиома выбора не нужна, поскольку переменные занумерованы.

      Использует: 10. Лемма о двух свидетелях. Опирается на: A (Индукция и рекурсия), D (Оценки и совпадение). Доказывается в уроке: Теорема компактности.

    3. Эквивалентные формы. Γ\Gamma невыполнимо тогда и только тогда, когда невыполнима некоторая его конечная часть; Γ⊨φ\Gamma \models \varphi тогда и только тогда, когда Γ0⊨φ\Gamma_{0} \models \varphi для некоторого конечного Γ0⊆Γ\Gamma_{0} \subseteq \Gamma; и эта последняя форма в свою очередь влечёт теорему.

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

    4. Сильная полнота. Если Γ⊨φ\Gamma \models \varphi, то Γ⊢φ\Gamma \vdash \varphi, для всякого Γ\Gamma: форма следования даёт конечное Γ0\Gamma_{0}, полнота для конечных посылок даёт Γ0⊢φ\Gamma_{0} \vdash \varphi, а монотонность Γ⊢φ\Gamma \vdash \varphi.

      Использует: 8. Полнота для конечных посылок, 12. Эквивалентные формы. Опирается на: B (Система курса). Доказывается в уроке: Теорема компактности.

    5. Вывод есть следование. Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi для всякого Γ\Gamma; теоремы суть в точности тавтологии, и множество непротиворечиво тогда и только тогда, когда оно выполнимо.

      Использует: 13. Сильная полнота. Опирается на: G (Корректность). Доказывается в уроке: Теорема компактности.

    6. Раскраска счётных графов. С переменной xi,cx_{i,c} для каждой вершины и каждого цвета и формулами, которые говорят, что у каждой вершины есть один и только один цвет и что соседние вершины различаются, счётный граф допускает раскраску в kk цветов, если её допускает каждый конечный подграф.

      Опирается на: H (Компактность), F (Конъюнктивные формы). Доказывается в уроке: Теорема компактности.

  4. Участок 4 Резолюция

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

    1. Клаузальная форма. Дизъюнкт есть конечное множество литералов, выполненное, если какой-либо из них равен 11, и □\Box невыполним; клаузальная форма множества Γ\Gamma имеет те же модели, что и оно, и Γ⊨φ\Gamma \models \varphi тогда и только тогда, когда клаузальная форма множества Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} невыполнима.

      Опирается на: F (Конъюнктивные формы), E (Семантическое следование). Доказывается в уроке: Метод резолюций.

    2. Определительная клаузальная форма. С новой переменной для каждой подзаписи и её определяющими дизъюнктами T(φ)T(\varphi) равновыполнимо с φ\varphi и содержит не более 4k+14k + 1 дизъюнктов, каждый не более чем из трёх литералов; определительные формы решают вопрос о следовании из конечных посылок.

      Использует: 16. Клаузальная форма. Опирается на: A (Индукция и рекурсия), D (Оценки и совпадение). Доказывается в уроке: Метод резолюций.

    3. Корректность резолюции. {C,D}⊨Rℓ(C,D)\{C, D\} \models R_{\ell}(C, D), разбором случаев по значению ℓ\ell; сильной индукцией по порождению S⊨CS \models C для всякого дизъюнкта CC, порождённого из SS, и если SS имеет опровержение, оно невыполнимо.

      Использует: 16. Клаузальная форма. Опирается на: A (Индукция и рекурсия). Доказывается в уроке: Метод резолюций.

    4. Исключение переменной. Ep(S)E_{p}(S), которое сохраняет дизъюнкты без pp и без ¬p\neg p и добавляет резольвенты по pp, не содержит pp и равновыполнимо с SS; из его модели получается модель множества SS выбором значения pp.

      Использует: 18. Корректность резолюции. Опирается на: D (Оценки и совпадение). Доказывается в уроке: Метод резолюций.

    5. Конечная полнота опровержения. Всякое конечное невыполнимое множество дизъюнктов имеет опровержение, по индукции по числу переменных: исключается последняя и вставляются посылки каждой резольвенты.

      Использует: 19. Исключение переменной. Опирается на: A (Индукция и рекурсия). Доказывается в уроке: Метод резолюций.

    6. Полнота опровержения. Множество дизъюнктов, конечное или бесконечное, невыполнимо тогда и только тогда, когда оно имеет опровержение; откуда Γ⊨φ\Gamma \models \varphi тогда и только тогда, когда клаузальная форма множества Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} имеет опровержение.

      Использует: 16. Клаузальная форма, 18. Корректность резолюции, 20. Конечная полнота опровержения. Опирается на: H (Компактность). Доказывается в уроке: Метод резолюций.

    7. Насыщение решает. При nn переменных множество порождённых дизъюнктов содержит не более 4n4^{n} элементов; насыщение завершается и решает вопрос о выполнимости без таблиц, хотя и не всегда быстрее, чем они.

      Использует: 18. Корректность резолюции, 20. Конечная полнота опровержения. Доказывается в уроке: Метод резолюций.

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