Разрешимость

Для высказываний программа есть, для кванторов её не существует. И это доказано

Разрешимость означает, что есть алгоритм, который за конечное время отвечает «следует / не следует» для любой формулы. Логика высказываний разрешима: таблица истинности и есть такой алгоритм. Логика предикатов неразрешима. Это доказали Чёрч и Тьюринг в 1936 году, и это предел, а не недоработка.

Open Logic Project, разделы о разрешимости. Чёрч и Тьюринг, 1936. Кук, 1971 · 24 мин · обновлено 06.09.2026

Аня написала программу: на вход она берёт аргумент логики высказываний, а на выход даёт «следует» или «не следует». Устроена программа просто: она строит таблицу истинности и ищет строку, где все посылки истинны, а заключение ложно. Нашла, значит не следует. Не нашла, значит следует.

Боря просит расширить программу на кванторы: «Все», «некоторые», модуль V. Логика ведь та же самая, только богаче. Просьба звучит скромно, а упирается она в один из главных результатов логики прошлого века.

Ответ придётся дать неприятный: такой программы не существует. Не «Аня не справится». Не «пока никто не придумал». Доказано, что её нет и быть не может, и доказано в 1936 году, двумя людьми независимо друг от друга. Этот урок про границу между «машине поручить можно» и «машине поручить нельзя», а ещё про то, во что обходится даже разрешённая сторона границы.

Логика высказываний: программа есть

Начнём с хорошей половины. Разбор по шагам: вот что делает программа Ани, и ни один шаг не пропускаю.

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

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

Заодно тут окончательно закрыта асимметрия из урока 3: раньше контрпример умели искать, но не умели доказывать, что его нет. Теперь умеют. Перебрали все строки, значит перебрали все случаи, и отсутствие провальной строки есть доказательство, а не отчёт о неудачных поисках. Стоит отметить и то, чего программе не требуется: она не знает, что такое дождь, экзамен и Мурка. Ей хватает устройства формулы, а устройство и есть то единственное, что проверяет логика. Урок 2 объявил это словами, а здесь оно стало программой.

Цена: каждая переменная удваивает таблицу

Разрешимость есть обещание, что ответ будет, а про то, когда он будет, обещания нет. Считаем: строк 2ⁿ.

Десять переменных дают 1024 строки. Двадцать дают больше миллиона. Тридцать дают больше миллиарда. Смотрите на рост: прибавили десять переменных и получили работы примерно в тысячу раз больше.

Это единственное место в курсе, где большое число не признак неудачного примера, а сам предмет разговора. На бумаге предел наступает раньше, чем кажется: таблица на пять переменных занимает 32 строки, и страница уже занята плотно. Отсюда и вырос модуль IV: вывод в двенадцать шагов помещается на пол-листа и заменяет таблицу, которую никто не станет выписывать.

Разница между двумя способами не в надёжности: оба дают правильный ответ, и урок 18 объяснил почему. Система корректна и полна, значит выводимое и следующее совпадают. Разница в цене. Таблица не требует умения и требует времени. Вывод требует умения и экономит время.

Задача о выполнимости

У той же таблицы есть близкий родственник, и вопрос задают чуть иначе: не «следует ли», а «бывает ли», то есть существует ли строка, в которой формула истинна? Урок 9 называл такие высказывания выполнимыми: в столбце есть хотя бы одна истина, значит, высказывание выполнимо. Это задача о выполнимости, по-английски SAT. По существу работа та же, и цена та же: строк 2ⁿ.

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

В 1971 году Стивен Кук доказал для неё NP-полноту, и задача о выполнимости стала первой задачей, для которой это доказано. Что такое NP-полнота, объясняет теория сложности, и разговор этот выходит далеко за рамки курса. Здесь достаточно одного наблюдения: место, где логика высказываний упирается в цену перебора, оказалось важным далеко за пределами логики.

Логика первого порядка: программы не существует

Теперь плохая половина.

Вопрос ставится так же: есть ли механический способ определить, следует ли φ из Γ, когда в языке есть кванторы? Ответ укладывается в два слова: способа нет. Доказали это в 1936 году Чёрч и Тьюринг, независимо друг от друга.

Слова «способа нет» надо читать буквально. Утверждение сделано не о тогдашних машинах и не о нынешних, а обо всех возможных механических способах сразу, включая те, которых никто ещё не придумал. Заметьте, насколько такое утверждение непривычно по виду. Обычно доказывают, что нечто существует: вот способ, вот он работает. Здесь доказано обратное: перебрать все возможные программы нельзя, значит рассуждать о них приходится разом, и это отдельная работа.

Почему знакомый приём здесь не годится, видно и без доказательства: таблица истинности для кванторов не строится. В логике высказываний случаев конечное число: 2ⁿ строк, и все они выписываются, а для кванторов пришлось бы перебирать наборы объектов, а их число ничем не ограничено. Это ещё не доказательство неразрешимости: доказательство Чёрча и Тьюринга устроено иначе и в курс не входит. Но видно, почему простой ход не срабатывает.

Полуразрешимость

И всё-таки не всё потеряно: кое-что машине поручить можно, и устроено это «кое-что» непривычно. Логика первого порядка полуразрешима. Разберём медленно, потому что с первого раза не укладывается.

Пусть φ действительно следует из Γ, тогда машина рано или поздно найдёт вывод. Почему найдёт, уже известно из урока 19. Логика первого порядка полна: если следует, то выводимо, значит, вывод существует. А раз он существует, его можно найти перебором. Выводов данной длины конечное число: машина перебирает сначала все короткие, потом всё более длинные, и нужный рано или поздно встретится.

Теперь другой случай. Пусть φ из Γ не следует, тогда вывода нет, и перебор не кончится никогда. Машина будет работать, работать и работать, а сказать «я всё перебрала, вывода нет» она не сможет: перебирать ей всегда есть что дальше. Вот и вся асимметрия. Ответ «да» приходит обязательно, хотя неизвестно когда. Ответ «нет» может не прийти вовсе.

И самое неприятное: глядя на работающую машину, нельзя понять, в каком мы случае. Она ещё ищет или искать нечего? По виду это одно и то же. Практический вывод отсюда простой и невесёлый: машине можно поручить поиск доказательства, а вердикт «доказательства не существует» поручить ей нельзя.

Ключи в тёмной комнате

Аналогия. Похоже на поиск ключей в тёмной комнате: если ключи там, рано или поздно нащупаешь. Если их там нет, будешь искать бесконечно, и по самому поиску одно от другого не отличишь.

Где аналогия ломается. В комнате конечное число мест, и, обыскав все, можно честно объявить: ключей нет. С выводами так не выйдет: их бесконечно много, и «обыскать все» нельзя никогда. Именно поэтому отрицательного ответа не бывает, а вовсе не потому, что машина недостаточно старается.

Если унести из аналогии одну комнату, останется впечатление, что дело в терпении. Дело не в терпении, и это главное, что стоит запомнить.

Три вопроса об одной системе

К одному и тому же набору правил можно подойти с тремя разными вопросами. Их стоит развести: путают их постоянно.

Первый: не врёт ли система? Всё ли выводимое действительно следует. Это корректность, урок 18.

Второй: не упускает ли система? Всё ли следующее выводимо. Это полнота, тот же урок.

Третий: можно ли поручить проверку машине? Есть ли способ получить ответ за конечное число механических шагов. Это разрешимость, урок сегодняшний.

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

Где интуиция даёт другой ответ

Слово «неразрешима» интуиция читает как «пока не разрешили». Прочтение неверное. Разница та же, что между «я не нашёл» и «его не существует» из урока 3, только на этот раз доказана вторая, сильная часть. Чёрч и Тьюринг доказали не то, что подходящей программы нет сегодня. Они доказали, что её не может быть никогда.

Такие утверждения встречаются реже, чем кажется, и стоят дорого. Обычно наука говорит «не нашли». Здесь сказано «нет», и это доказано.

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

Что можно и чего нельзя: итог модуля

Соберём модуль в короткий список.

Логика высказываний. Полна. Разрешима: таблица всегда даёт ответ. Цена составляет 2ⁿ строк.

Логика первого порядка. Корректна и полна: теорема Гёделя 1929/30 года. Неразрешима: Чёрч и Тьюринг, 1936. Полуразрешима: вывод найдётся, если он есть.

Формальная арифметика. Неполна, если она непротиворечива и эффективно аксиоматизируема: теорема Гёделя 1931 года.

Три строчки, и в них весь ответ на вопрос «что можно и чего нельзя». Заметьте, что ни одна из них не звучит как «логика бессильна». Каждая говорит точнее: вот эта работа делается механически, вот эта не делается, а вот у этой есть цена. Разница между «бессильна» и «вот граница, и вот где она проходит» и есть разница между разговором и доказательством.

Что дальше

Модуль закончен. Границы очерчены, и очерчены доказательствами, а не впечатлениями. Дальше курс возвращается к живой речи. Урок 21 показывает эксперимент, где одну и ту же по устройству задачу решают верно то 19 человек из ста, то 72 из ста, в зависимости от того, о чём в ней говорится. Оттуда и берётся ответ на вопрос из урока 1: зачем формальная запись человеку, который и так умеет рассуждать.

Вопросы для самопроверки

Что читать

• Open Logic Project, разделы о разрешимости и вычислимости: Открытый учебник по металогике под лицензией CC BY 4.0. Там доказательство неразрешимости дано целиком. Чтобы его читать, понадобится сначала разобраться, что такое вычислимая функция.
• Open Logic Project, разделы о разрешимости: Обе стороны цены рядом: механический перебор и путь, который надо искать. Полезно перечитать именно теперь, когда видно, зачем в курсе понадобились оба способа.