В логике проблема принятия решения «истина/ложь» разрешима , если существует эффективный метод получения правильного ответа. Логика нулевого порядка (пропозициональная логика) разрешима, тогда как логика первого и высшего порядка — нет. Логические системы разрешимы, если принадлежность к их множеству логически допустимых формул (или теорем) может быть эффективно определена. Теория (множество предложений, замкнутых относительно логического следствия ) в фиксированной логической системе разрешима, если существует эффективный метод определения того, включены ли произвольные формулы в теорию. Многие важные проблемы неразрешимы , то есть было доказано, что для них не может существовать эффективного метода определения принадлежности (возвращения правильного ответа после конечного, хотя, возможно, очень длительного времени во всех случаях).
Каждая логическая система имеет как синтаксический компонент , который, помимо прочего, определяет понятие доказуемости , так и семантический компонент , который определяет понятие логической валидности . Логически валидные формулы системы иногда называют теоремами системы , особенно в контексте логики первого порядка, где теорема Гёделя о полноте устанавливает эквивалентность семантического и синтаксического следствия. В других условиях, таких как линейная логика , отношение синтаксического следствия (доказуемости) может использоваться для определения теорем системы.
Логическая система разрешима, если существует эффективный метод определения того, являются ли произвольные формулы теоремами логической системы. Например, пропозициональная логика разрешима, поскольку метод таблицы истинности может быть использован для определения того, является ли произвольная пропозициональная формула логически допустимой.
Логика первого порядка в общем случае неразрешима; в частности, множество логических действительности в любой сигнатуре , которая включает равенство и по крайней мере один другой предикат с двумя или более аргументами, неразрешимо. [1] Логические системы, расширяющие логику первого порядка, такие как логика второго порядка и теория типов , также неразрешимы.
Однако валидности монадического исчисления предикатов с тождеством разрешимы. Эта система является логикой первого порядка, ограниченной теми сигнатурами, которые не имеют функциональных символов и чьи символы отношений, отличные от равенства, никогда не принимают более одного аргумента.
Некоторые логические системы не могут быть адекватно представлены одним лишь набором теорем. (Например, логика Клини вообще не имеет теорем.) В таких случаях часто используются альтернативные определения разрешимости логической системы, которые требуют эффективного метода для определения чего-то более общего, чем просто истинность формул; например, истинность секвенций или отношение следования {(Г, A ) | Г ⊧ A } логики.
Теория — это набор формул, часто предполагаемый замкнутым относительно логического следствия . Разрешимость теории касается того, существует ли эффективная процедура, которая решает, является ли формула членом теории или нет, учитывая произвольную формулу в сигнатуре теории. Проблема разрешимости возникает естественным образом, когда теория определяется как набор логических следствий фиксированного набора аксиом.
Существует несколько основных результатов о разрешимости теорий. Каждая (непаранепротиворечивая ) непротиворечивая теория разрешима, поскольку каждая формула в сигнатуре теории будет логическим следствием и, таким образом, членом теории. Каждая полная рекурсивно перечислимая теория первого порядка разрешима. Расширение разрешимой теории может быть неразрешимым. Например, в пропозициональной логике существуют неразрешимые теории, хотя множество валидностей (наименьшая теория) разрешимо.
Непротиворечивая теория, которая обладает свойством, что каждое непротиворечивое расширение неразрешимо, называется существенно неразрешимой . Фактически, каждое непротиворечивое расширение будет существенно неразрешимым. Теория полей неразрешима, но не существенно неразрешима. Известно, что арифметика Робинсона существенно неразрешима, и, таким образом, каждая непротиворечивая теория, которая включает или интерпретирует арифметику Робинсона, также (существенно) неразрешима.
Примерами разрешимых теорий первого порядка являются теория вещественных замкнутых полей и арифметика Пресбургера , тогда как теория групп и арифметика Робинсона являются примерами неразрешимых теорий.
Некоторые разрешимые теории включают (Monk 1976, стр. 234): [2]
Методы, используемые для установления разрешимости, включают исключение квантификаторов , полноту модели и тест Лоса-Воота .
Некоторые неразрешимые теории включают (Monk 1976, стр. 279): [2]
Метод интерпретируемости часто используется для установления неразрешимости теорий. Если существенно неразрешимая теория T интерпретируема в непротиворечивой теории S , то S также существенно неразрешима. Это тесно связано с концепцией редукции многих единиц в теории вычислимости .
Свойство теории или логической системы, более слабое, чем разрешимость, — это полуразрешимость . Теория полуразрешима, если существует четко определенный метод, результат которого при заданной произвольной формуле оказывается положительным, если формула есть в теории; в противном случае может вообще не оказаться; в противном случае оказывается отрицательным. Логическая система полуразрешима, если существует четко определенный метод для генерации последовательности теорем, такой, что каждая теорема в конечном итоге будет сгенерирована. Это отличается от разрешимости, поскольку в полуразрешимой системе может не быть эффективной процедуры для проверки того, что формула не является теоремой.
Каждая разрешимая теория или логическая система полуразрешима, но в общем случае обратное неверно; теория разрешима тогда и только тогда, когда и она сама, и ее дополнение полуразрешимы. Например, множество логических истин V логики первого порядка полуразрешимо, но не разрешимо. В этом случае это происходит потому, что не существует эффективного метода определения для произвольной формулы A, принадлежит ли A V . Аналогично, множество логических следствий любого рекурсивно перечислимого множества аксиом первого порядка полуразрешимо. Многие из примеров неразрешимых теорий первого порядка, приведенных выше, имеют такую форму.
Разрешимость не следует путать с полнотой . Например, теория алгебраически замкнутых полей разрешима, но неполна, тогда как множество всех истинных утверждений первого порядка о неотрицательных целых числах в языке с + и × полно, но неразрешимо. К сожалению, из-за терминологической двусмысленности термин «неразрешимое утверждение» иногда используется как синоним независимого утверждения .
Как и в случае с понятием разрешимого множества , определение разрешимой теории или логической системы может быть дано либо в терминах эффективных методов , либо в терминах вычислимых функций . Они, как правило, считаются эквивалентными согласно тезису Чёрча . Действительно, доказательство того, что логическая система или теория неразрешима, будет использовать формальное определение вычислимости, чтобы показать, что соответствующее множество не является разрешимым множеством, а затем ссылаться на тезис Чёрча, чтобы показать, что теория или логическая система неразрешима никаким эффективным методом (Enderton 2001, стр. 206 и далее ).
Некоторые игры были классифицированы по степени их разрешимости:
