Разрешимая теория

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

История вопроса и предпосылки

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

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

Когда понятия исчисления и алгоритма были уточнены, последовал ряд результатов о неразрешимости различных теорий. Одним из первых таких результатов была теорема, доказанная Новиковым, о неразрешимости проблемы слов в группах. Разрешимые же теории были известны задолго до этого.

Интуитивно понятно, что чем сложнее и выразительнее теория, тем больше шансов, что она окажется неразрешимой. Поэтому, грубо говоря, «неразрешимая теория» — синоним к «сложная теория».

Общие сведения

Формальное исчисление в общем случае должно определять язык, правила построения термов и формул, аксиомы и правила вывода. Таким образом, для каждой теоремы T, всегда можно построить цепочку A₁, A₂, … , A_n=T, где каждая формула A_i либо является аксиомой, либо выводима из предыдущих формул, по одному из правил вывода. Разрешимость означает, что существует алгоритм, который для каждого правильно построенного предложения T, за конечное время выдаёт однозначный ответ: да, данное предложение выводимо в рамках исчисления или нет — оно не выводимо.

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

Примеры разрешимых теорий

Примеры неразрешимых теорий

Полуразрешимость и автоматическое доказательство

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

Требование полуразрешимости эквивалентно возможности эффективно перечислить все теоремы данной теории. Иными словами, множество теорем должно быть рекурсивно-перечислимым. Такая процедура для логики первого порядка была описана ещё Гильбертом. На самом деле, теория будет полуразрешимой, если множество её аксиом и правил вывода будут рекурсивными перечислимыми множествами. Большинство, используемых на практике теорий, удовлетворяют этому требованию.

Большое практическое значение имеют эффективные полуразрешающие процедуры для логики первого порядка, так как они позволяют (полу)автоматически доказывать формализованные утверждения очень широкого класса. Прорывом в этой области было открытие Робинсоном в 1965 году метода резолюций. Другим важнейшим полуразрешающим алгоритмом на сегодняшний день является табло-метод.

Связь разрешимости и полноты

В математической логике, традиционно используется два понятия полноты: собственно полнота и полнота, относительно некоторого класса интерпретаций (или структур). В первом случае, теория полна, если любое предложение в ней является либо истинным, либо ложным. Во втором — если любое предложение, истинное при всех интерпретациях из данного класса выводимо. Например, натуральная арифметика неполна, согласно теоремам Гёделя о неполноте, но она полна относительно своей стандартной интерпретации — это следует из теоремы Гёделя о полноте.

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

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

Литература

• Мальцев А.И., Алгоритмы и рекурсивные функции, Наука, 1986.
• Ackermann W., Solvable Cases of the Decision Problem, North-Holland Publishing, Amsterdam, 1954.
• John Alan Robinson, Andrei Voronkov (Eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press 2001, ISBN 0-444-50813-9, ISBN 0-262-18223-8

См. также

• Полнота
• Непротиворечивость
• Тезис Чёрча — Тьюринга