Введение

Есть ли у решаемой задачи эффективный метод для получения ответа? В логике, задача принятия решения, имеющая ответ "истина" или "ложь", считается разрешимой, если существует эффективный метод для получения правильного ответа. Логика нулевого порядка (пропозициональная логика) разрешима, в то время как логика первого и высших порядков – нет. Логическая система считается разрешимой, если можно эффективно определить, принадлежит ли формула её множеству логически допустимых формул (или теорем). Теория (множество предложений, замкнутое относительно логического следования) в фиксированной логической системе разрешима, если существует эффективный метод для определения, принадлежит ли произвольная формула этой теории. Многие важные задачи являются неразрешимыми, то есть доказано, что для них не может существовать эффективного метода определения принадлежности (возвращающего правильный ответ за конечное, хотя и возможно очень большое, время во всех случаях).

Решимость логической системы

Каждая логическая система включает в себя как синтаксический компонент, который, в частности, определяет понятие доказуемости, так и семантический компонент, определяющий понятие логической истинности. Логически истинные формулы системы иногда называют теоремами системы, особенно в контексте логики первого порядка, где теорема о полноте Гёделя устанавливает эквивалентность семантического и синтаксического следования. В других случаях, таких как линейная логика, отношение синтаксического следования (доказуемости) может использоваться для определения теорем системы. Логическая система называется разрешимой, если существует эффективный метод для определения того, являются ли произвольные формулы теоремами этой логической системы. Например, пропозициональная логика разрешима, поскольку метод таблиц истинности можно использовать для определения логической истинности произвольной пропозициональной формулы. Логика первого порядка в общем случае не является разрешимой; в частности, множество логических истин в любой сигнатуре, включающей равенство и хотя бы один другой предикат с двумя или более аргументами, не является разрешимым. Логические системы, расширяющие логику первого порядка, такие как логика второго порядка и теория типов, также неразрешимы. Однако, разрешима задача проверки истинности монодической предикативной логики с тождеством. Эта система представляет собой логику первого порядка, ограниченную сигнатурами, не содержащими функциональных символов и чьи реляционные символы, отличные от равенства, никогда не принимают более одного аргумента. Некоторые логические системы не адекватно представляются только набором теорем. (Например, логика Клини вообще не имеет теорем.) В таких случаях часто используются альтернативные определения разрешимости логической системы, требующие эффективного метода для определения чего-то более общего, чем просто истинность формул; например, истинности секвенций или отношения следования {(Γ, A) | Γ ⊢ A} в данной логике.

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

Теория — это множество формул, часто предполагаемое замкнутым относительно логического следования. Решаемость теории касается наличия эффективной процедуры, определяющей, является ли данная формула элементом теории, для произвольной формулы в сигнатуре теории. Проблема решаемости возникает естественным образом, когда теория определяется как множество логических следствий фиксированного набора аксиом. Существует несколько основных результатов о решаемости теорий. Каждая (непарапоследовательная) противоречивая теория является разрешимой, поскольку каждая формула в сигнатуре теории будет логическим следствием и, следовательно, элементом теории. Каждая полная рекурсивно перечислимая теория первого порядка является разрешимой. Расширение разрешимой теории может быть неразрешимым. Например, в пропозициональной логике существуют неразрешимые теории, хотя множество тавтологий (наименьшая теория) является разрешимым. Согласованная теория, обладающая свойством, что каждое согласованное расширение является неразрешимым, называется по существу неразрешимой. Фактически, любое согласованное расширение будет по существу неразрешимым. Теория полей является неразрешимой, но не по существу неразрешимой. Арифметика Робинсона известна как по существу неразрешимая, и, следовательно, каждая согласованная теория, включающая или интерпретирующая арифметику Робинсона, также (по существу) неразрешима. Примеры разрешимых теорий первого порядка включают теорию вещественно замкнутых полей и арифметику Пресбургера, в то время как теория групп и арифметика Робинсона являются примерами неразрешимых теорий.

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

Свойство теории или логической системы, более слабое, чем разрешимость, называется полуразрешимостью. Теория полуразрешима, если существует чётко определённый метод, который для произвольной формулы выдаёт положительный результат, если формула является теоремой этой теории; в противном случае, метод может никогда не завершиться; иначе, выдаёт отрицательный результат. Логическая система полуразрешима, если существует чётко определённый метод для генерации последовательности теорем, при котором каждая теорема в конечном итоге будет сгенерирована. Это отличается от разрешимости, поскольку в полуразрешимой системе может не существовать эффективной процедуры для проверки того, что формула не является теоремой. Любая разрешимая теория или логическая система является полуразрешимой, но в общем случае обратное неверно: теория разрешима тогда и только тогда, когда она и её дополнение полуразрешимы. Например, множество логических истин V логики первого порядка является полуразрешимым, но не разрешимым. Это происходит из-за отсутствия эффективного метода определения для произвольной формулы A, является ли A не-истиной. Аналогично, множество логических следствий любого рекурсивно перечислимого множества аксиом первого порядка является полуразрешимым. Многие из вышеприведённых примеров неразрешимых теорий первого порядка имеют такую форму.

Связь с полнотой

Решимость не следует путать с полнотой. Например, теория алгебраически замкнутых полей является разрешимой, но неполной, в то время как множество всех истинных утверждений первого порядка о неотрицательных целых числах в языке с операциями + и × является полным, но неразрешимым. К сожалению, из-за терминологической неоднозначности термин "неразрешимое утверждение" иногда используется как синоним независимого утверждения.

Отношение к вычислимости

Как и в случае с понятием разрешимого множества, определение разрешимой теории или логической системы может быть дано либо в терминах эффективных методов, либо в терминах вычислимых функций. Эти подходы обычно считаются эквивалентными в соответствии с тезисом Черча. Действительно, доказательство неразрешимости логической системы или теории использует формальное определение вычислимости для демонстрации того, что соответствующее множество не является разрешимым, а затем апеллирует к тезису Черча, чтобы показать, что теория или логическая система неразрешима никаким эффективным методом (Enderton 2001, с. 206 и далее).