Алгоритмическая разрешимость
Алгоритмическая разрешимость — свойство
История вопроса и предпосылки
Понятия алгоритма и аксиоматической системы имеют давнюю историю. И то и другое известно ещё со времён античности. Достаточно вспомнить постулаты геометрии Евклида и алгоритм нахождения наибольшего общего делителя того же Евклида. Несмотря на это, чёткого математического определения исчисления и особенно алгоритма не существовало очень долгое время. Особенность проблемы, связанной с формальным определением неразрешимости состояла в том, что для того, чтобы показать, что некоторый алгоритм существует, достаточно его просто найти и продемонстрировать. Если же алгоритм не находится, возможно его не существует и это тогда требуется строго доказать. А для этого нужно точно знать, что такое алгоритм.
Большой прогресс в формализации этих понятий был достигнут в начале
Когда понятия исчисления и алгоритма были уточнены, последовал ряд результатов о неразрешимости различных теорий. Одним из первых таких результатов была теорема, доказанная Новиковым, о неразрешимости проблемы слов в группах. Разрешимые же теории были известны задолго до этого.
Интуитивно понятно, что чем сложнее и выразительнее теория, тем больше шансов, что она окажется неразрешимой. Поэтому, грубо говоря, «неразрешимая теория» — «сложная теория».
Общие сведения
Формальное исчисление в общем случае должно определять язык, правила построения термов и формул, аксиомы и правила вывода. Таким образом, для каждой теоремы T всегда можно построить цепочку A1, A2, … , An=T, где каждая формула Ai либо является аксиомой, либо выводима из предыдущих формул по одному из правил вывода. Разрешимость означает, что существует алгоритм, который для каждого правильно построенного предложения T за конечное время выдаёт однозначный ответ: да, данное предложение выводимо в рамках исчисления или нет — оно невыводимо.
Очевидно, что противоречивая теория разрешима, так как любая формула будет выводимой. С другой стороны, если исчисление не обладает
Примеры разрешимых теорий
 | Этот раздел статьи ещё не написан. |
Примеры неразрешимых теорий
| Этот раздел статьи ещё не написан. |
Полуразрешимость и автоматическое доказательство
Разрешимость — очень сильное свойство, и большинство полезных и используемых на практике теорий им не обладают. В связи с этим было введено более слабое понятие полуразрешимости. Полуразрешимость означает наличие алгоритма, который за конечное время всегда подтвердит, что предложение истинно, если это действительно так, но если нет — может работать бесконечно.
Требование полуразрешимости эквивалентно возможности эффективно перечислить все теоремы данной теории. Иными словами, множество теорем должно быть
Большое практическое значение имеют эффективные полуразрешающие процедуры для логики первого порядка, так как они позволяют
Связь разрешимости и полноты
В математической логике традиционно используется два понятия полноты: собственно полнота и полнота относительно некоторого класса интерпретаций (или структур). В первом случае, теория полна, если любое предложение в ней является либо истинным, либо ложным. Во втором — если любое предложение, истинное при всех интерпретациях из данного класса, выводимо.
Оба понятия тесно связаны с разрешимостью. Например, если множество аксиом полной теории первого порядка рекурсивно перечислимо, то она разрешима. Это следует из известной теоремы Поста, утверждающей, что если множество и его дополнение оба рекурсивно перечислимы, то они также разрешимы. Интуитивно, аргумент, показывающий истинность приведённого утверждения, следующий: если теория полна, и множество её аксиом рекурсивно перечислимо, то существуют полуразрешающие процедуры для проверки истинности любого утверждения, равно как и его отрицания. Если запустить обе эти процедуры параллельно, то учитывая полноту теории, одна из них должна когда-нибудь остановиться и выдать позитивный ответ.
Если теория полна относительно некоторого класса интерпретаций, это можно использовать для построения разрешающей процедуры. Например
См. также
- Полнота формальной системы
- Непротиворечивость
- Тезис Чёрча — Тьюринга
- Вычислимая функция
- Разрешимое множество
- Алгоритмически неразрешимая задача
- Трансвычислительная задача
Литература
- Мальцев А. И. . Алгоритмы и рекурсивные функции. — М.: Наука, 1986.
- Ackermann, Wilhelm. Solvable cases of the decision problem. — Amsterdam: North-Holland Publishing, 1954.
- Handbook of Automated Reasoning (in 2 volumes) / John Alan Robinson, Andrei Voronkov. — Elsevier and MIT Press, 2001. — ISBN 0-262-18223-8.
 | Для улучшения этой статьи желательно:
|