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

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

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

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

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

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

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

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

Разрешимость теории [ править ]

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

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

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

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

Некоторые разрешимые теории [ править ]

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

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

Некоторые неразрешимые теории [ править ]

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

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

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

Semidecidability [ edit ]

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

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

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

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

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

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

В контексте игр [ править ]

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

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

См. также [ править ]

Ссылки [ править ]

Примечания [ править ]

  1. ^ Трахтенброт , 1953.
  2. ^ Jump up to: Перейти обратно: а б Монк, Дональд (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 . }

Библиография [ править ]

Retrieved from "https://en.wikipedia.org/w/index.php?title=Decidability_(logic)&oldid=1222934151"