Корректность и полнота
Система не врёт и система ничего не упускает: это не одно свойство, а два
Корректность обещает, что всё доказуемое в системе действительно следует: система не врёт. Полнота обещает, что доказуемо всё следующее: система ничего не упускает. Для классической логики доказаны оба свойства, но это два разных утверждения с разными доказательствами.
Open Logic Project, разделы о корректности и полноте. forall x: Calgary, гл. 21 «Soundness and completeness». Гёдель, 1929/30 · 24 мин · обновлено 06.09.2026
После урока вы сможете
- Различать два обещания системы вывода: не выводить лишнего и не упускать нужного
- Читать записи «Γ ⊢ φ» и «Γ ⊨ φ» и не подменять одну другой
- Не смешивать обоснованность аргумента с корректностью системы
- Понимать, что совпадение выводимого и следующего есть теорема, а не определение
Аня закончила вывод: двенадцать строк, у каждой указано правило и ссылки на предыдущие строки, а в последней строке стоит то, что требовалось доказать. Боря смотрит и спрашивает: «А откуда ты знаешь, что твои правила не врут?» Вопрос выглядит придиркой. Он не придирка.
Посмотрите, что происходило все двенадцать строк: ни разу мы не спрашивали, бывает ли положение дел, где посылки истинны, а заключение ложно. Мы переставляли значки по разрешённым образцам. А вдруг среди образцов есть один плохой? Тогда безупречно оформленный вывод приведёт куда угодно, и по виду это будет незаметно.
Есть и встречный вопрос, ещё неприятнее: пусть заключение действительно следует из посылок, обязательно ли для него найдётся вывод? Может быть, правил просто не хватает, и часть настоящих следований остаётся без доказательства. Перед нами два вопроса и два разных обещания, и этот урок про них.
Два знака и два разных мира
Разговор станет короче, если ввести обозначения: пусть набор посылок называется Γ, греческая буква «гамма», а заключение называется φ, буква «фи». Так их записывают в книгах. Первая запись: Γ ⊢ φ. Читается: из Γ выводимо φ. Она означает вот что: существует список строк, в котором каждая получена по правилу, а последняя есть φ. Ровно то, что написала Аня.
Вторая запись: Γ ⊨ φ. Читается: из Γ следует φ. Она означает другое: не бывает случая, где все посылки из Γ истинны, а φ ложно. Ровно определение правильности из урока 2.
Разницу стоит проговорить вслух, иначе она сотрётся. Первый знак говорит про бумагу: список, правила, ссылки. Такое можно предъявить, проверить строчку за строчкой и убедиться самому. Второй знак про бумагу не говорит ничего, а говорит обо всех мыслимых положениях дел сразу, и предъявить их нельзя: их бесконечно много.
Разница видна и с практической стороны. У вывода есть первая строка и последняя, и его можно отдать другому человеку, а тот проверит его целиком, ничего не додумывая. Со случаями так не выйдет: в логике высказываний их 2ⁿ, и то много, а для кванторов положений дел столько, что перебрать их нельзя вовсе.
Здесь и лежит смысл всей затеи с выводом: вывод есть конечный предмет, которым распоряжаются вместо бесконечной проверки, и ради такой замены стоит потрудиться. Отсюда простое следствие, ради которого всё и затевалось: то, что эти два знака означают одно и то же, ниоткуда не вытекает, и это надо доказывать. И доказывают это двумя разными теоремами, по одной на каждое направление.
Корректность: система не врёт
Первое обещание такое: всё, что система выводит, действительно следует. Записывается коротко: если Γ ⊢ φ, то Γ ⊨ φ. Читается: если выводимо, то следует. Это свойство набора правил называется корректностью. Что оно запрещает, видно на выдуманном плохом правиле. Пусть кто-нибудь добавит к системе такое: из «если P, то Q» и из «Q» получаем «P».
Эта система выведет из «если шёл дождь, асфальт мокрый» и «асфальт мокрый» заключение «шёл дождь», и вывод будет оформлен идеально: строка, правило, ссылки. А следования нет: ночью проехала поливальная машина, и вот случай, где посылки истинны, а заключение ложно. Система с таким правилом некорректна: она врёт красиво и по форме. Как убеждаются, что система не врёт? Разбор по шагам. Ни один шаг не пропускаю.
Шаг 1. Берём одно правило и смотрим только на него.
Шаг 2. Спрашиваем: бывает ли случай, где всё, на что правило ссылается, истинно, а то, что оно даёт, ложно?
Шаг 3. Для modus ponens такого случая нет. Это проверено таблицей ещё в уроке 8: строки-провала у него не существует.
Шаг 4. То же самое проверяем для каждого правила по отдельности. Правил конечное число, так что работа кончается.
Шаг 5. Вывод есть цепочка таких шагов. Ни один шаг истинность не теряет, значит не теряет и вся цепочка.
Вот и всё доказательство корректности, если убрать аккуратность. Оно длинное, но не хитрое: проверка правил по одному и сложение результата. Обратите внимание, где именно сделана работа: мы проверили не тот вывод, который написала Аня. Мы проверили конечный список правил и получили обещание сразу про все возможные выводы, включая ещё не написанные.
Полнота: система ничего не упускает
Второе обещание обратное: всё, что следует, система умеет вывести. Записывается так: если Γ ⊨ φ, то Γ ⊢ φ. Читается: если следует, то выводимо, и это полнота системы вывода. Что она запрещает, тоже видно на примере: выбросим из системы modus ponens, а прочие правила оставим.
Система останется корректной: врать ей теперь нечем, лишних правил в ней нет, а прежних стало только меньше. Зато из «если Аня пришла, то Боря пришёл» и «Аня пришла» вывести «Боря пришёл» больше не получится.
Следование есть, вывода нет. Система неполна.
Отсюда наблюдение, которое многое объясняет. Корректность достаётся даром, ведь система без единого правила корректна безупречно: она ничего не выводит, значит и соврать ей нечем. Полноту даром не получишь никак: она требует, чтобы правил хватило на всё сразу. И разница в трудности не случайная: корректность проверяют правило за правилом, а правил конечное число, тогда как полнота говорит обо всех следованиях разом, а их перебрать нельзя. Поэтому корректность доказывают на семинаре, а полноту логики первого порядка доказал Гёдель, и это событие в истории науки.
Правила добавляют и убавляют
Из двух обещаний сразу видно, как устроен выбор при постройке системы. Убрали правило, и корректность в безопасности: ничего лишнего система вывести не сможет, возможностей у неё стало меньше. Зато полнота под ударом. Добавили правило, и всё наоборот: полнота растёт, ведь выводимого стало больше. Зато под ударом корректность: новое правило может оказаться плохим.
Два обещания тянут в разные стороны, и хорошая система есть та, где обе тяги уравновешены точно. Правил ровно столько, чтобы хватило на всё следующее и не хватило ни на что лишнее. На глаз такое равновесие не проверить, и отсюда две теоремы вместо честного слова автора системы. И отсюда же понятно, почему набор правил из модуля IV выглядит таким скупым. Скупость тут не от бедности: каждое лишнее правило есть риск потерять корректность, а её терять нельзя ни при каких обстоятельствах.
Сито и где оно ломается
Аналогия. Система вывода есть сито, сквозь которое сыплют утверждения. Корректность: мусор не проходит, то есть не пролезает ничего, что на самом деле не следует. Полнота: нужное не задерживается, то есть проходит всё, что следует. Сравнение удобное и в трёх местах неверное, и сказать, где именно, обязательно.
Первое. Сито разбирает готовую кучу. Систему вывода никто не просеивает: она не сортирует готовый список, а строит выводы, которых до неё не было.
Второе. Качество сита проверяют, просеяв всё, а здесь просеивать нечего: утверждений бесконечно много. Оба свойства не проверяют, а доказывают.
Третье, и самое важное. У сита оба свойства обеспечены одним устройством: сделал дырки нужного размера, получил и то и другое. Здесь это два разных утверждения с двумя разными доказательствами: одно берётся перебором правил, а другое даётся теоремой Гёделя 1929 года.
Если из аналогии унести только «сито», останется впечатление, что корректность и полнота настраиваются одной ручкой. Это неверно, и потому аналогия идёт с оговоркой.
Обоснованность и корректность: разные вещи
Теперь место, где путаются почти все и путаются надолго. В уроке 2 было слово обоснованный: обоснованный аргумент правилен, и вдобавок все его посылки истинны. В этом уроке появилось слово корректная: корректная система есть та, которая не выводит ничего лишнего. В английском и то и другое называется soundness, а русские переводы плавают, и склеить два понятия проще простого. Разводить их надо по трём признакам.
Первый: у свойства разный носитель. Обоснованность есть свойство одного конкретного аргумента. Корректность есть свойство набора правил, то есть всей системы целиком.
Второй: разное отношение к фактам. Обоснованность требует, чтобы посылки были истинны на самом деле: это вопрос к предмету, к данным, к специалисту. Корректность о действительности не спрашивает ничего.
Третий: разный способ проверки. Обоснованность проверяют, глядя на посылки конкретного аргумента. Корректность доказывают один раз, правило за правилом, и дальше ею пользуются.
Курс держится такого распределения слов до конца. Об аргументе говорим правильный и обоснованный. О системе говорим корректная и полная.
В уроке 5 полным назывался набор связок: через {¬, ∧} выражается любая истинностная функция. Это функциональная полнота, и к сегодняшнему разговору она отношения не имеет. А в уроке 19 появится третье употребление того же слова, уже про системы аксиом. Именно на этой тройной занятости слова стоит половина мистики вокруг Гёделя.
Где интуиция даёт другой ответ
Спросите себя быстро: полная система доказывает все истинные утверждения?
Почти все отвечают «да». Ответ неверный.
Полнота есть обещание про следование, а не про истину: она говорит, что если φ следует из данных посылок, то φ из них и выводимо. Про истину саму по себе не сказано ни слова. Возьмите утверждение «идёт дождь». Оно бывает истинным, но из пустого набора посылок оно не следует: есть случаи, где дождя нет.
Полная система его и не докажет, и правильно сделает, ведь доказать его значило бы соврать, а врать запрещает корректность. Что полная система выводит вообще без посылок, так это логические истины. «Идёт дождь или не идёт дождь» истинно при любой погоде, и вывод для него найдётся.
Разница выглядит мелкой. Она не мелкая: на ней держится половина недоразумений вокруг теорем Гёделя. Стоит проговорить её ещё раз, другими словами. Полнота говорит не про то, что система всеведуща, а про то, что она не теряет по дороге. Дать ей нечего, если посылок нет.
Когда оба обещания выполнены
Пусть система корректна и полна сразу, тогда два знака совпадают: выводимо ровно то, что следует, и ничего сверх того. Польза от этого прямая: проверять следование можно двумя способами, и они дают один ответ. Можно перебирать случаи таблицей, а можно строить вывод. Первое надёжно и дорого, второе быстро и требует умения. Выбор ваш, а результат один.
Ради этого совпадения модуль IV и затевался. Урок 10 обещал: ⊢ и ⊨ есть разные вещи, а то, что они совпадают, будет доказано позже. Сейчас это позже наступило. Логика высказываний полна, а вдобавок разрешима: для неё есть механический способ получить ответ. Про это урок 20. Логика первого порядка (та, где есть кванторы «все» и «некоторые») корректна и полна тоже.
И здесь надо назвать имя: полноту логики первого порядка доказал Курт Гёдель в диссертации 1929 года, а сама работа напечатана в 1930-м. Формулировка такая: всякое утверждение, истинное во всех моделях, доказуемо в исчислении. Коротко: если Γ ⊨ φ, то Γ ⊢ φ. Это хорошая новость: аппарат вывода ничего не упускает, за каждым следованием стоит вывод, который можно найти и предъявить.
Стоит сказать и о том, чего теорема не даёт. Она обещает, что вывод существует, а про его длину и про то, как его искать, она молчит. Разница ощутимая. Модуль IV показал, что вывод в двенадцать шагов ищется с тупиками и возвратами, даже когда заранее известно: он есть. И это совсем не то, о чём говорят популярные тексты со словом «Гёдель»: те говорят о другой его работе, написанной двумя годами позже.
Что дальше
Мы развели два обещания системы вывода и увидели, что они независимы: одно можно иметь без другого, и оба надо доказывать отдельно. Урок 19 разводит две теоремы Гёделя: о полноте и о неполноте. Первую вы уже знаете, а вторая про другой предмет и про другое свойство, и смешивают их постоянно.
Урок 20 отвечает на вопрос, который напрашивается сам собой. Раз всё так механично, нельзя ли поручить проверку машине? Для логики высказываний можно. Для кванторов нельзя, и это доказано.
Откуда это и кто доказал
| Курт Гёдель, теорема о полноте логики первого порядка | 1929 | Всякое утверждение, истинное во всех моделях, доказуемо в исчислении первого порядка: если Γ ⊨ φ, то Γ ⊢ φ. Диссертация 1929 года, публикация в 1930-м. |
| Герхард Генцен, натуральный вывод | 1934 | Набор правил, где у каждой связки своё правило введения и своё правило удаления. Именно про такой набор и спрашивают, корректен ли он и полон ли. |
Ловушки и теоремы
В английском оба понятия называются soundness, и отсюда путаница. Обоснованность есть свойство одного аргумента: он правилен и вдобавок его посылки истинны на самом деле. Корректность есть свойство набора правил: всё выводимое действительно следует. Обоснованность требует фактов о мире, корректность о мире не спрашивает ничего.
Естественный ответ «да» неверен. Полнота говорит о следовании: если φ следует из посылок, то φ из них выводимо. Истинное утверждение «идёт дождь» из пустого набора посылок не следует, и полная система его не докажет. Без посылок выводятся только логические истины вроде «идёт дождь или не идёт дождь».
Теорема о полноте: если Γ ⊨ φ, то Γ ⊢ φ. Доказана Куртом Гёделем в диссертации 1929 года, напечатана в 1930-м. Обратное направление, то есть корректность («если выводимо, то следует»), доказывается проще, проверкой правил по одному. Совпадение двух знаков не определение и не соглашение: это две теоремы.
Корректность: если Γ ⊢ φ, то Γ ⊨ φ. Доказывается перебором правил по одному: у каждого спрашивают, бывает ли случай, где всё, на что оно ссылается, истинно, а то, что оно даёт, ложно. У modus ponens такого случая нет, и это проверено таблицей ещё в уроке 8. Правил конечное число, поэтому работа кончается, а вывод есть цепочка шагов, ни один из которых истинности не теряет. Условие видно прямо из доказательства: обещание относится к этому списку правил, а не к системам вообще. Добавьте правило «из P → Q и Q получаем P», и система начнёт выводить то, что не следует, оформляя это идеально по форме. Корректность не даёт полноты: это два разных утверждения с двумя разными доказательствами.
Термины
- корректность системы выводаsoundness of a proof system
- Свойство набора правил: всё, что в системе выводимо, действительно следует. Записывается «если Γ ⊢ φ, то Γ ⊨ φ». Доказывается проверкой каждого правила по отдельности.
- полнота системы выводаcompleteness of a proof system
- Свойство набора правил: всё, что следует, в системе выводимо. Записывается «если Γ ⊨ φ, то Γ ⊢ φ». Про истину саму по себе ничего не обещает.
- непротиворечивая системаconsistent system
- Система, которая не доказывает утверждение вместе с его отрицанием. Противоречивая система доказывает всё подряд, поэтому непротиворечивость требуется во всех теоремах о неполноте.
- теорема о полнотеcompleteness theorem
- Результат Курта Гёделя 1929/30 года: всякое утверждение, истинное во всех моделях, доказуемо в исчислении первого порядка. Коротко: если Γ ⊨ φ, то Γ ⊢ φ.
- металогикаmetalogic
- Утверждения не внутри логической системы, а о ней самой: корректна ли она, полна ли, разрешима ли. Доказываются такие утверждения обычными рассуждениями, а не средствами самой системы.
- правильный аргументvalid argument
- Аргумент, для которого невозможен случай, где все посылки истинны, а заключение ложно. Свойство формы: проверяется без всякого знания о предмете.
- обоснованный аргументsound argument
- Правильный аргумент, у которого вдобавок все посылки истинны. Только он гарантирует истинность заключения.
- логическая истинаlogical truth
- Высказывание, истинное при любом положении дел: «идёт дождь или не идёт дождь». Аргумент с таким заключением правилен при любых посылках.
Практикум · Испортить правило и поймать поломку
Корректность не абстракция: её ловят руками. Задача занимает пятнадцать минут и даёт проверяемый результат, строку таблицы, на которую можно показать пальцем.
- Выпишите три правила, которыми вы пользовались в модуле IV: modus ponens, дизъюнктивный силлогизм и удаление конъюнкции. Каждое запишите схемой: что дано, что получается.
- Для каждого постройте таблицу на две переменные, всего четыре строки. Отметьте строки, где всё данное истинно, и проверьте, истинно ли в них полученное.
- Убедитесь, что строки-провала нет ни у одного. Это и есть проверка корректности трёх правил.
- Теперь испортите одно правило нарочно: в дизъюнктивном силлогизме замените «P или Q, не P, значит Q» на «P или Q, P, значит не Q». Постройте таблицу заново.
- Найдите строку, где посылки испорченного правила истинны, а вывод ложен, и выпишите её отдельно. Эта строка есть доказательство некорректности, и одной такой строки достаточно, чтобы забраковать правило навсегда.
Вопросы для самопроверки
Система вывода корректна. Что это значит?
- Все её аксиомы истинны в действительности
- Всё, что в ней выводимо, действительно следует из посылок
- Всё, что следует из посылок, в ней выводимо
- Она даёт ответ на любой вопрос за конечное число шагов
Из системы выбросили все правила до единого. Какой она стала?
- Корректной, но крайне неполной
- Полной, но некорректной
- И корректной, и полной сразу
- Ни корректной, ни полной
Почему совпадение «выводимо» и «следует» приходится доказывать?
- Потому что таково соглашение о записи, принятое ради удобства
- Потому что доказательство требуется всякому утверждению без исключений
- Потому что определения у них совершенно разные: одно про список строк по правилам, другое про все мыслимые случаи
- Потому что в некоторых логиках они не совпадают, а в классической совпадение заложено прямо в определение и доказывать его незачем
Чем корректность системы отличается от обоснованности аргумента?
- Ничем: это два перевода одного английского слова soundness
- Корректность относится к логике первого порядка, а обоснованность относится к логике высказываний: в языке с кванторами об истинности посылок уже не спрашивают
- Корректность проверяют таблицей, а обоснованность выводом
- Обоснованность есть свойство одного аргумента и требует истинных посылок, а корректность есть свойство набора правил и о фактах не спрашивает
Логика первого порядка полна. Следует ли отсюда, что в ней доказуемо утверждение «идёт дождь»?
- Да, ведь полнота означает доказуемость всего истинного
- Нет: из пустого набора посылок это утверждение не следует, а полнота обещает только выводимость следующего
- Да, но лишь при условии, что дождь действительно идёт
- Нет, потому что «идёт дождь» не логическое утверждение, и в языке первого порядка ему не находится ни предиката, ни имени
Ответы и разбор открываются в самопроверке урока: она считает результат и отмечает урок пройденным. Пройти самопроверку.
Что читать
- Open Logic Project, разделы о корректности и полноте: Открытый учебник по металогике под лицензией CC BY 4.0. Здесь оба доказательства даны целиком. Читать после курса: техника там начинается сразу, зато видно, насколько разной длины эти два доказательства.
- forall x: Calgary, гл. 21 «Soundness and completeness»: Доказательство корректности разобрано по правилам, ровно тем способом, который в уроке дан на пальцах. Хорошая проверка себе: если пять шагов из урока понятны, глава читается без остановок.