Является ли множество предложений логики первого порядка, имеющих модель, рекурсивно перечислимым?

В указаниях говорится об использовании $%\{x:\phi_x(\text{пустой аргумент})\text{ останавливается}\}$% и использовании $%m$%-приводимости

задан 12 Дек '19 5:04

Я не знаю, как это полагается делать при помощи указаний, но сам факт достаточно стандартен. По теореме Гёделя о полноте, формула Ф не имеет модели iff not(Ф) приводит к противоречию. Тогда Ф выводима, то есть является тавтологией. Таким образом, дополнение множества состоит из отрицаний тавтологий. Известно, что множество выводимых в ИП формул перечислимо. Если множество из условия перечислимо, то оно разрешимо. А это, как известно, не так (теорема Чёрча).

(12 Дек '19 9:29) falcao

А если не известно про перечислимость множества тавтологий (или это что-то простое?), можно ли вместо Вашего аргумента воспользоваться тем, что множество выполнимых предложений равно множеству конечно выполнимых предложений (finitely satisfiable), и как-то доказать, что множество конечно выполнимых предложений перечислимо?

(12 Дек '19 21:09) logic

@logic: я привык пользоваться наиболее известными предложениями. Теорема о полноте ИП -- это фундаментальная вещь. Из него следует вычислимость множества тавтологий. Кстати говоря, неразрешимость ИП -- факт более сложный.

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

(12 Дек '19 21:50) falcao

В смысле утверждение о равенстве множеств выполнимых и конечно выполнимых предложений неверно? Вроде тут написано, что множества равны https://proofwiki.org/wiki/Compactness_Theorem

(13 Дек '19 1:34) logic

@logic: если Вы про теорему компактности, то тогда всё понятно, но я не вижу, как это может помочь. Там ведь речь всего об одной формуле.

Такую терминологию надо использовать осторожно (или не использовать :)), потому что она путается с терминами из теоремы Трахтенброта, а там разница между одним и другим есть. Но это совсем отдельная тема.

(13 Дек '19 1:54) falcao

Почему там речь идет об одной формуле? По ссылке написано Пусть T - некоторое множество предложений логики предикатов, тогда Т выполнимо iff T конечно выполнимо.

(13 Дек '19 2:24) logic

@logic: в условии задачи рассматривается множество формул, имеющих модель. Каждая формула на этот предмет рассматривается по отдельности. См. первый комментарий.

(13 Дек '19 3:27) falcao

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

И что значит "приводит к противоречию"? Это понятие синтактическое или семантическое?

(17 Дек '19 0:16) logic

@logic: теорема именно эта. Если формула не истинна ни в одной модели, то её отрицание истинно во всех моделях, а потому выводимо. Надо иметь в виду, что таких формул очень мало -- это отрицания тавтологий. То есть всегда ложные формулы типа not(p->p).

Приводит к противоречию -- это синтаксическое условие. По правилам исчисления, можно вывести как A, так и not(A).

(17 Дек '19 3:42) falcao

Была формула ф, такая что not(ф) верно во восех моделях. Тогда not(ф) выводима. Почему выводимость not(ф) влечет то, что ф приводит к противоречию (что означает, как Вы сказали, что не только not(ф) выводима, но и сама ф тоже выводима)? Здесь как-то снова используется первое предложение настоящего комментария?

(17 Дек '19 5:10) logic
показано 5 из 10 показать еще 5
10|600 символов нужно символов осталось
Знаете, кто может ответить? Поделитесь вопросом в Twitter или ВКонтакте.

Ваш ответ

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

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

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

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

отмечен:

×865

задан
12 Дек '19 5:04

показан
103 раза

обновлен
17 Дек '19 5:10

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

по почте:

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

по RSS:

Ответы

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

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