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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  • Набор логических значений в любой сигнатуре первого порядка с равенством и либо: символ отношения арности не менее 2, либо два унарных функциональных символа, либо один функциональный символ арности не менее 2, установленный Трахтенброт в 1953 г.
  • Теория первого порядка натуральных чисел со сложением, умножением и равенством, установленная Тарским и Анджей Мостовски в 1949 г.
  • Теория первого порядка рациональных чисел со сложением, умножением и равенством, установленная Джулия Робинсон в 1949 г.
  • Теория групп первого порядка, установленная Альфред Тарский в 1953 г.[3] Примечательно, что неразрешима не только общая теория групп, но и несколько более конкретных теорий, например (как было установлено Мальцевым 1961 г.) теория конечных групп. Мальцев также установил неразрешимость теории полугрупп и теории колец. Робинсон установил в 1949 г. неразрешимость теории полей.
  • Арифметика Робинсона (и, следовательно, любое последовательное расширение, такое как Арифметика Пеано ) по существу неразрешима, как установлено Рафаэль Робинсон в 1950 г.
  • Теория первого порядка с равенством и двумя функциональными символами[4]

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

Полурастворимость

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

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

Отношение к полноте

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

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

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

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

Немного игры классифицированы по разрешимости:

  • Шахматы разрешима.[5][6] То же самое справедливо для всех других конечных игр двух игроков с точной информацией.
  • Товарищ в п в бесконечные шахматы (с ограничениями по правилам и элементам игры) разрешима.[7][8] Однако есть позиции (с конечным числом фигур), которые являются принудительными выигрышами, но не матом. п для любого конечного п.[9]
  • Некоторые командные игры с несовершенной информацией на конечной доске (но с неограниченным временем) неразрешимы.[10]

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

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

Примечания

  1. ^ Трахтенброт, 1953
  2. ^ а б Дональд Монк (1976). Математическая логика. Springer-Verlag. ISBN  9780387901701.
  3. ^ Тарский, А .; Мостовский, А .; Робинсон, Р. (1953), Неразрешимые теории, Исследования по логике и основам математики, Северная Голландия, Амстердам
  4. ^ Гуревич, Юрий (1976). «Проблема решения для стандартных классов». J. Symb. Бревно. 41 (2): 460–464. CiteSeerX  10.1.1.360.1517. Дои:10.1017 / S0022481200051513. Получено 5 августа 2014.
  5. ^ Стек обмена информатики. «Разрешимо ли движение ТМ в шахматы?»
  6. ^ Нерешимая шахматная проблема?
  7. ^ Mathoverflow.net/Decidability-of-chess-on-an-infinite-board Разрешимость-шахмат на-бесконечной-доске
  8. ^ Дэн Брамлев, Джоэл Дэвид Хэмкинс, Филипп Шлихт, Проблема взаимопонимания в бесконечных шахматах разрешима, Лекционные заметки по информатике, том 7318, 2012 г., стр. 78–88, Springer [1], доступны на arXiv:1201.5597.
  9. ^ "Lo.logic - Мат в ходах $ omega $?".
  10. ^ Неразрешимые проблемы: пробоотборник Бьорн Пунен (Раздел 14.1, «Абстрактные игры»).

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

  • Барвайз, Джон (1982), «Введение в логику первого порядка», в Barwise, Jon (ed.), Справочник по математической логике, Исследования по логике и основам математики, Амстердам: Северная Голландия, ISBN  978-0-444-86388-1
  • Кантоне, Д., Э. Г. Омодео и А. Поликрити, "Теория множеств для вычислений. От процедур принятия решений до логического программирования с множествами", Монографии по компьютерным наукам, Springer, 2001.
  • Чагров Александр; Захарящев, Михаил (1997), Модальная логика, Oxford Logic Guides, 35, The Clarendon Press Oxford University Press, ISBN  978-0-19-853779-3, МИСТЕР  1464942
  • Дэвис, Мартин (1958), Вычислимость и неразрешимость, McGraw-Hill Book Company, Inc, Нью-Йорк
  • Эндертон, Герберт (2001), Математическое введение в логику (2-е изд.), Бостон, Массачусетс: Академическая пресса, ISBN  978-0-12-238452-3
  • Кейслер, Х. Дж. (1982), «Основы теории моделей», в Барвайз, Джон (ред.), Справочник по математической логике, Исследования по логике и основам математики, Амстердам: Северная Голландия, ISBN  978-0-444-86388-1
  • Монк, Дж. Дональд (1976), Математическая логика, Берлин, Нью-Йорк: Springer-Verlag