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

Корректность и полнота

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

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

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

  1. Сформулировать корректность и полноту в их слабой, конечной и сильной формах, различать их как независимые свойства и объяснить, почему рассуждение, получающее полноту «из корректности», содержит порочный круг.
  2. Доказать корректность сильной индукцией по числу строк, включая случай правила замены двойного отрицания, и применить её для доказательства непротиворечивости системы и невыводимости конкретных формул.
  3. Вывести в системе курса две леммы о стрелке Пирса и доказать с их помощью, индукцией по сложности, лемму Кальмара.
  4. Доказать слабую полноту, устраняя гипотезы разбором случаев, и полноту для конечных множеств посылок с помощью двух теорем о дедукции.
  5. Применять совпадение выводимости и следования, чтобы решать вопросы о выводимости, доказуемой эквивалентности и непротиворечивости и чтобы анализировать, что происходит при добавлении правил к системе.

Два вопроса о системе курса

Раздел о выводе зафиксировал систему курса: схемы аксиом A1, A2 и A3 Лукасевича и два правила, modus ponens (MP) и замену двойного отрицания (ЗДО), которую урок о четырёх приёмах вывода добавил после доказательства двойного отрицания. Вывод из множества Γ\Gamma есть конечная последовательность формул, в которой каждая является аксиомой, элементом Γ\Gamma, результатом modus ponens, применённого к двум предыдущим формулам, или результатом ЗДО, применённой к одной предыдущей; Γ⊢φ\Gamma \vdash \varphi означает, что существует вывод из Γ\Gamma, последняя формула которого есть φ\varphi. Раздел о семантике, со своей стороны, определил в уроке о семантическом следовании и эквивалентности отношение Γ⊨φ\Gamma \models \varphi: всякая оценка, выполняющая все формулы из Γ\Gamma, выполняет φ\varphi. Оба отношения записываются по одному образцу, множество слева и формула справа; однако их природа противоположна. Первое синтаксическое и экзистенциальное: оно утверждает, что существует конечный объект, вывод, который можно проверить символ за символом. Второе семантическое и универсальное: оно утверждает нечто обо всех оценках, которых бесконечно много и каждая из которых придаёт значения бесконечному числу переменных.

Таким образом, о системе возникают два вопроса. Первый: выводит ли она только то, что должна? Система называется корректной, если для всякого множества Γ\Gamma и всякой формулы φ\varphi из Γ⊢φ\Gamma \vdash \varphi следует Γ⊨φ\Gamma \models \varphi: то, что выводится из посылок, истинно при всякой оценке, при которой истинны посылки. Второй: выводит ли она всё, что должна? Система называется полной, если из Γ⊨φ\Gamma \models \varphi следует Γ⊢φ\Gamma \vdash \varphi. Полнота допускает три степени, в зависимости от того, какие множества посылок она охватывает:

  • слабая полнота: если ⊨φ\models \varphi, то ⊢φ\vdash \varphi; всякая тавтология есть теорема;
  • полнота для конечных множеств: если {γ1,…,γk}⊨φ\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi, то {γ1,…,γk}⊢φ\{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi;
  • сильная полнота: если Γ⊨φ\Gamma \models \varphi, то Γ⊢φ\Gamma \vdash \varphi, для произвольного множества Γ\Gamma, в том числе бесконечного.

Этот урок доказывает корректность и две первые степени полноты. Третья доказывается в уроке о теореме компактности, а причина такого разделения будет объяснена в конце урока.

Чего не следует говорить

В испанском языке корректность иногда называют «solvencia», калькой с английского soundness; испанский термин «corrección», и по-русски курс говорит «корректность». Не следует также определять её как свойство системы «выводить выражение из множества выражений»: это сама выводимость, а не свойство системы. Ошибки по существу, однако, другие, и их две.

Первая состоит в утверждении, что корректность и полноту «можно вывести одну из другой». Это независимые свойства: система Лукасевича без правила ЗДО корректна (доказательство этого урока это показывает, если опустить один случай) и не полна (урок о формальных дедуктивных системах предъявил тавтологию, которую она не выводит); а система, принявшая бы все формулы за аксиомы, была бы полной, не будучи корректной. Решённая задача 2 разбирает оба примера.

Вторая ошибка серьёзнее, поскольку выдаёт за доказательство полноты рассуждение, содержащее порочный круг. По существу оно гласит: если φ⊬ψ\varphi \nvdash \psi, то по теореме о дедукции ⊬(φ→ψ)\nvdash (\varphi \rightarrow \psi); «по корректности» ⊭(φ→ψ)\not\models (\varphi \rightarrow \psi); и по семантической теореме о дедукции φ⊭ψ\varphi \not\models \psi. Однако корректность говорит, что выводимое общезначимо, а её контрапозиция, что необщезначимое невыводимо:

⊢χ  ⇒  ⊨χ,⊭χ  ⇒  ⊬χ\vdash \chi \;\Rightarrow\; \models \chi, \qquad \not\models \chi \;\Rightarrow\; \nvdash \chi

Шаг рассуждения идёт в обратном направлении, от ⊬χ\nvdash \chi к ⊭χ\not\models \chi, а это контрапозиция утверждения ⊨χ⇒⊢χ\models \chi \Rightarrow \vdash \chi, то есть слабой полноты. Если это так, рассуждение предполагает то, что намерено доказать. Отсюда следует, что полнота не «выводится простым способом»: это самый глубокий результат курса, и её доказательство занимает большую часть этого урока. Наконец, неточно резюмировать полноту словами «все истинные выражения имеют доказательство»; доказательство имеет общезначимое, истинное при всякой оценке, а не истинное при некоторой: переменная v1v_{1} истинна при многих оценках и не является теоремой.