Разрешимость (логика)
В логике «истина/ложь» проблема принятия решения разрешима , если существует эффективный метод получения правильного ответа. Логика нулевого порядка (логика высказываний) разрешима, тогда как логика первого порядка и высшего порядка — нет. Логические системы разрешимы, если принадлежность к их множеству логически действительных можно эффективно определить формул (или теорем). Теория ) в фиксированной логической системе разрешима , (множество предложений , замкнутых с логическим следствием если существует эффективный метод определения того, включены ли в теорию произвольные формулы. Многие важные проблемы неразрешимы , то есть доказано, что для них не может существовать никакого эффективного метода определения принадлежности (возвращения правильного ответа по истечении конечного, хотя во всех случаях, возможно, очень длительного времени).
Разрешимость логической системы [ править ]
Каждая логическая система имеет как синтаксический компонент , который, среди прочего, определяет понятие доказуемости , так и семантический компонент , который определяет понятие логической достоверности . Логически действительные формулы системы иногда называют теоремами системы, особенно в контексте логики первого порядка, где теорема Гёделя о полноте устанавливает эквивалентность семантических и синтаксических следствий. В других ситуациях, таких как линейная логика , отношение синтаксического следствия (доказуемости) может использоваться для определения теорем системы.
Логическая система разрешима, если существует эффективный метод определения того, являются ли произвольные формулы теоремами логической системы. Например, логика высказываний разрешима, поскольку метод таблицы истинности можно использовать для определения того, является ли произвольная формула высказывания логически допустимой.
Логика первого порядка вообще неразрешима; в частности, набор логических допустимостей в любой сигнатуре , которая включает равенство и хотя бы один другой предикат с двумя или более аргументами, неразрешим. [1] Логические системы, расширяющие логику первого порядка, такие как логика второго порядка и теория типов , также неразрешимы.
Однако обоснованность монадического исчисления предикатов с тождеством разрешима. Эта система представляет собой логику первого порядка, ограниченную теми сигнатурами, которые не имеют функциональных символов и чьи символы отношения, кроме равенства, никогда не принимают более одного аргумента.
Некоторые логические системы не могут быть адекватно представлены одним лишь набором теорем. (Например, в логике Клини вообще нет теорем.) В таких случаях часто используются альтернативные определения разрешимости логической системы, которые требуют эффективного метода определения чего-то более общего, чем просто справедливость формул; например, достоверность секвенций или отношение следствий {(Г, A ) | Г ⊧ A } логики.
Разрешимость теории [ править ]
Теория логического — это набор формул, которые часто считаются замкнутыми с точки зрения следствия . Разрешимость теории касается того, существует ли эффективная процедура, которая решает, является ли формула членом теории или нет, учитывая произвольную формулу в сигнатуре теории. Проблема разрешимости возникает естественным образом, когда теория определяется как совокупность логических следствий фиксированного набора аксиом.
Существует несколько основных результатов о разрешимости теорий. Любая (непаранепротиворечивая ) противоречивая теория разрешима, поскольку каждая формула в сигнатуре теории будет логическим следствием теории и, следовательно, ее членом. Любая полная рекурсивно перечислимая теория первого порядка разрешима. Расширение разрешимой теории может быть неразрешимым. Например, в логике высказываний существуют неразрешимые теории, хотя множество истинностей (наименьшая теория) разрешимо.
Непротиворечивая теория, обладающая тем свойством, что каждое непротиворечивое расширение неразрешимо, называется по существу неразрешимой . Фактически, каждое непротиворечивое расширение будет по существу неразрешимым. Теория полей неразрешима, но не является по существу неразрешимой. Арифметика Робинсона, как известно, по существу неразрешима, и поэтому каждая непротиворечивая теория, которая включает или интерпретирует арифметику Робинсона, также (по существу) неразрешима.
Примеры разрешимых теорий первого порядка включают теорию действительных замкнутых полей и арифметику Пресбургера , а теория групп и арифметика Робинсона являются примерами неразрешимых теорий.
Некоторые разрешимые теории [ править ]
Некоторые разрешимые теории включают (Monk 1976, стр. 234): [2]
- Набор логических достоверностей первого порядка в сигнатуре только с равенством, установленный Леопольдом Левенхаймом в 1915 году.
- Набор логических достоверностей первого порядка в сигнатуре с равенством и одной унарной функцией, установленный Эренфойхтом в 1959 году.
- Теория первого порядка натуральных чисел в сигнатуре с равенством и сложением, также называемая арифметикой Пресбургера . Полноту установил Мойжеш Пресбургер в 1929 году.
- Теория первого порядка натуральных чисел в сигнатуре с равенством и умножением, также называемая скулемской арифметикой .
- Теория булевых алгебр первого порядка , созданная Альфредом Тарским в 1940 году (найдена в 1940 году, но объявлена в 1949 году).
- Теория первого порядка алгебраически замкнутых полей заданной характеристики , созданная Тарским в 1949 году.
- Теория первого порядка вещественно-замкнутых упорядоченных полей , созданная Тарским в 1949 году (см. также проблему Тарского с показательной функцией ).
- Теория первого порядка евклидовой геометрии , созданная Тарским в 1949 году.
- Теория абелевых групп первого порядка , созданная Шмелевым в 1955 году.
- Теория гиперболической геометрии первого порядка , созданная Швабхойзером в 1959 году.
- Конкретные разрешимые подъязыки теории множеств, изучаемые с 1980-х годов по сегодняшний день (Cantone et al. , 2001) .
- Монадическая второго порядка теория деревьев (см. S2S ).
Методы, используемые для установления разрешимости, включают исключение кванторов , полноту модели и тест Лоша-Вота .
Некоторые неразрешимые теории [ править ]
Некоторые неразрешимые теории включают (Монк 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]
См. также [ править ]
Ссылки [ править ]
Примечания [ править ]
- ^ Трахтенброт , 1953.
- ^ Перейти обратно: а б Монк, Дональд (1976). Математическая логика . Спрингер. ISBN 9780387901701 .
- ^ Тарский, А.; Мостовский А.; Робинсон, Р. (1953), Неразрешимые теории , Исследования по логике и основам математики, Северная Голландия, Амстердам, ISBN 9780444533784
- ^ Гуревич, Юрий (1976). «Проблема принятия решений для стандартных классов» . Дж. Симб. Бревно . 41 (2): 460–464. CiteSeerX 10.1.1.360.1517 . дои : 10.1017/S0022481200051513 . S2CID 798307 . Проверено 5 августа 2014 г.
- ^ Информатика Stack Exchange. «Разрешимо ли шахматное движение ТМ?»
- ^ Неразрешимая шахматная задача?
- ^ Mathoverflow.net/Разрешимость шахмат на бесконечной доске Разрешимость шахмат на бесконечной доске
- ^ Брюмлеве, Дэн; Хэмкинс, Джоэл Дэвид; Шлихт, Филипп (2012). «Проблема мата в бесконечных шахматах разрешима» . Конференция по вычислимости в Европе . Конспекты лекций по информатике. Том. 7318. Спрингер. стр. 78–88. arXiv : 1201.5597 . дои : 10.1007/978-3-642-30870-3_9 . ISBN 978-3-642-30870-3 . S2CID 8998263 .
- ^ «Lo.logic – Мат в $\omega$ ходах?» .
- ^ Пунен, Бьорн (2014). «10. Неразрешимые проблемы: Сэмплер: §14.1 Абстрактные игры» . В Кеннеди, Джульетта (ред.). Интерпретация Гёделя: критические очерки . Издательство Кембриджского университета. стр. 211–241 См. стр. 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, vol. 35, Издательство Оксфордского университета, 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
