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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  • Шахматы разрешимы. То же самое верно и для всех других конечных игр для двух игроков с точной информацией.
  • Mate в п в бесконечной шахматы (с ограничениями по правилам и gamepieces) разрешим. Однако есть позиции (с конечным числом фигур), которые являются принудительными выигрышами, но не матом по n для любого конечного n .
  • Некоторые командные игры с несовершенной информацией на конечной доске (но с неограниченным временем) неразрешимы.
  • «Игра жизни» Конвея неразрешима.

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

использованная литература

Примечания

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

  • Барвайз, Джон (1982), «Введение в логику первого порядка», в Барвайз, Джон (редактор), Справочник по математической логике , Исследования по логике и основам математики, Амстердам: Северная Голландия, 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-е изд.), Бостон, Массачусетс: Academic Press , ISBN 978-0-12-238452-3
  • Кейслер, HJ (1982), «Основы теории моделей», в Барвайз, Джон (редактор), Справочник по математической логике , Исследования по логике и основам математики, Амстердам: Северная Голландия, ISBN 978-0-444-86388-1
  • Монк, Дж. Дональд (1976), математическая логика , Берлин, Нью-Йорк: Springer-Verlag