stringtranslate.com

Разрешимость (логика)

В логике проблема принятия решения «истина/ложь» разрешима , если существует эффективный метод получения правильного ответа. Логика нулевого порядка (логика высказываний) разрешима, тогда как логика первого порядка и высшего порядка — нет. Логические системы разрешимы, если можно эффективно определить принадлежность к их множеству логически действительных формул (или теорем). Теория (множество предложений, замкнутых с логическим следствием ) в фиксированной логической системе разрешима, если существует эффективный метод определения того, включены ли в теорию произвольные формулы . Многие важные проблемы неразрешимы , то есть доказано, что для них не может существовать никакого эффективного метода определения принадлежности (возвращения правильного ответа через конечное, хотя, возможно, очень долгое время во всех случаях).

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

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

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

Логика первого порядка вообще неразрешима; в частности, набор логических допустимостей в любой сигнатуре , которая включает равенство и хотя бы один другой предикат с двумя или более аргументами, неразрешим. [1] Логические системы, расширяющие логику первого порядка, такие как логика второго порядка и теория типов , также неразрешимы.

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

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

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

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

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

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

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

Некоторые разрешимые теории

Некоторые разрешимые теории включают (Monk 1976, стр. 234): [2]

Методы, используемые для установления разрешимости, включают исключение кванторов , полноту модели и тест Лоша-Вота .

Некоторые неразрешимые теории

Некоторые неразрешимые теории включают (Монк 1976, стр. 279): [2]

Метод интерпретируемости часто используется для установления неразрешимости теорий. Если существенно неразрешимая теория T интерпретируется в непротиворечивой теории S , то S также существенно неразрешима. Это тесно связано с концепцией редукции «многие единицы» в теории вычислимости.

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

Свойством теории или логической системы, более слабым, чем разрешимость, является полуразрешимость . Теория является полуразрешимой, если существует четко определенный метод, результат которого для произвольной формулы оказывается положительным, если эта формула содержится в теории; в противном случае он может вообще не прийти; в противном случае он будет отрицательным. Логическая система является полуразрешимой, если существует четко определенный метод генерации последовательности теорем, при котором каждая теорема в конечном итоге будет генерироваться. Это отличается от разрешимости, поскольку в полуразрешимой системе может не быть эффективной процедуры проверки того, что формула не является теоремой.

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

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

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

Связь с вычислимостью

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

В контексте игр

Некоторые игры классифицируются по разрешимости:

Смотрите также

Рекомендации

Примечания

  1. ^ Трахтенброт , 1953.
  2. ^ аб Монк, Дональд (1976). Математическая логика . Спрингер. ISBN 9780387901701.
  3. ^ Тарский, А.; Мостовский А.; Робинсон, Р. (1953), Неразрешимые теории, исследования в области логики и основы математики, Северная Голландия, Амстердам, ISBN 9780444533784
  4. ^ Гуревич, Юрий (1976). «Проблема принятия решений для стандартных классов». Дж. Симб. Бревно . 41 (2): 460–464. CiteSeerX 10.1.1.360.1517 . дои : 10.1017/S0022481200051513. S2CID  798307 . Проверено 5 августа 2014 г. 
  5. ^ Информатика Stack Exchange. «Разрешимо ли шахматное движение ТМ?»
  6. ^ Неразрешимая шахматная задача?
  7. ^ Mathoverflow.net/Разрешимость шахмат на бесконечной доске Разрешимость шахмат на бесконечной доске
  8. ^ Брамлеве, Дэн; Хэмкинс, Джоэл Дэвид; Шлихт, Филипп (2012). «Проблема мата в бесконечных шахматах разрешима». Конференция по вычислимости в Европе . Конспекты лекций по информатике. Том. 7318. Спрингер. стр. 78–88. arXiv : 1201.5597 . дои : 10.1007/978-3-642-30870-3_9. ISBN 978-3-642-30870-3. S2CID  8998263.
  9. ^ "Lo.logic - Мат в ходах $\omega$?".
  10. ^ Пунен, Бьорн (2014). «10. Неразрешимые проблемы: Сэмплер: §14.1 Абстрактные игры». В Кеннеди, Джульетта (ред.). Интерпретация Гёделя: критические очерки . Издательство Кембриджского университета. стр. 211–241 См. стр. 211–241. 239. arXiv : 1204.0299 . CiteSeerX 10.1.1.679.3322 . ISBN  9781107002661.}

Библиография