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