Как доказать разрешимость полной теории первого порядка в конечной сигнатуре с перечислимым множеством теорем?

задан 28 Июн '19 14:18

Поскольку теория полна, для любой замкнутой формулы A доказуема или она сама, или её отрицание. Поэтому в процессе перечисления теорем за конечное время появится или A, или not(A). Алгоритм проверки A на выводимость состоит в том, чтобы дождаться появления одной из этих формул.

Тут можно ещё заметить, что если теория противоречива, то любая формула выводима, и есть алгоритм, всегда говорящий "да", поэтому можно ограничиться рассмотрением непротиворечивых теорий, когда выводима ровно одна из двух формул A, not(A).

(28 Июн '19 18:52) falcao
10|600 символов нужно символов осталось
Знаете, кто может ответить? Поделитесь вопросом в Twitter или ВКонтакте.

Ваш ответ

Если вы не нашли ответ, задайте вопрос.

Здравствуйте

Математика - это совместно редактируемый форум вопросов и ответов для начинающих и опытных математиков, с особенным акцентом на компьютерные науки.

Присоединяйтесь!

отмечен:

×1,113

задан
28 Июн '19 14:18

показан
176 раз

обновлен
28 Июн '19 18:52

Отслеживать вопрос

по почте:

Зарегистрировавшись, вы сможете подписаться на любые обновления

по RSS:

Ответы

Ответы и Комментарии

Дизайн сайта/логотип © «Сеть Знаний». Контент распространяется под лицензией cc by-sa 3.0 с обязательным указанием авторства.
Рейтинг@Mail.ru