Разрешимость (логика)
Имеет ли проблема принятия решения эффективный метод получения ответа

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Ссылки

Примечания

  1. ↑ Борис Трахтенброт (1953). «О рекурсивной отделимости». Доклады АН СССР . 88 : 935–956 .
  2. ^ ab Monk, Donald (1976). Математическая логика . Springer. ISBN 9780387901701.
  3. ^ Тарский, А.; Мостовский, А.; Робинсон, Р. (1953), Неразрешимые теории, Исследования по логике и основания математики, Северная Голландия, Амстердам, ISBN 9780444533784
  4. ^ Гуревич, Юрий (1976). «Проблема принятия решений для стандартных классов». J. Symb. Log . 41 (2): 460– 464. CiteSeerX 10.1.1.360.1517 . doi :10.1017/S0022481200051513. S2CID  798307. Получено 5 августа 2014 г. 
  5. ^ Stack Exchange Computer Science. «Разрешим ли ход шахматной партии TM?»
  6. ^ Неразрешимая шахматная задача?
  7. ^ Mathoverflow.net/Разрешимость-шахмат-на-бесконечной-доске Разрешимость-шахмат-на-бесконечной-доске
  8. ^ Brumleve, Dan; Hamkins, Joel David; Schlicht, Philipp (2012). «Проблема мата в n ходах бесконечных шахмат разрешима». Конференция по вычислимости в Европе . Конспект лекций по информатике. Том 7318. Springer. С.  78–88 . arXiv : 1201.5597 . doi :10.1007/978-3-642-30870-3_9. ISBN 978-3-642-30870-3. S2CID  8998263.
  9. ^ "Lo.logic – Мат в $\omega$ ходах?".
  10. ^ Poonen, Bjorn (2014). "10. Неразрешимые проблемы: пример: §14.1 Абстрактные игры". В Kennedy, Juliette (ред.). Интерпретация Гёделя: критические эссе . Cambridge University Press. стр. 211–241 См. стр. 239. arXiv : 1204.0299 . CiteSeerX 10.1.1.679.3322 . ISBN  9781107002661.

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

  • Барвайз, Джон (1982), «Введение в логику первого порядка», в Барвайз, Джон (ред.), Справочник по математической логике , Исследования по логике и основаниям математики, Амстердам: Северная Голландия, ISBN 978-0-444-86388-1
  • Кантоне, Д.; Омодео, Э.Г.; Поликрити, А. (2013) [2001], Теория множеств для вычислений. От процедур принятия решений к логическому программированию с множествами, Монографии по информатике, Springer, ISBN 9781475734522
  • Чагров, Александр; Захарьящев, Михаил (1997), Модальная логика , Oxford Logic Guides, т. 35, Oxford University Press, ISBN 978-0-19-853779-3, г-н  1464942
  • Дэвис, Мартин (2013) [1958], Вычислимость и неразрешимость, Довер, ISBN 9780486151069
  • Эндертон, Герберт (2001), Математическое введение в логику (2-е изд.), Academic Press , ISBN 978-0-12-238452-3
  • Кейслер, Х. Дж. (1982), «Основы теории моделей», в книге Барвайза, Джона (ред.), Справочник по математической логике , Исследования по логике и основаниям математики, Амстердам: Северная Голландия, ISBN 978-0-444-86388-1
  • Монк, Дж. Дональд (2012) [1976], Математическая логика , Springer-Verlag , ISBN 9781468494525
Retrieved from "https://en.wikipedia.org/w/index.php?title=Decidability_(logic)&oldid=1267345062#Decidability_of_a_theory"