alt text

Тут нужно провести доказательство этого факта.

задан 21 Ноя 3:15

@falcao, помогите, пожалуйста, с доказательством этого факта.

(21 Ноя 11:24) Pointer
1

@Pointer: это хорошая задача, и я на уровне общей идеи представляю, как её можно было бы решать, но до деталей пока не продумывал. Можете пока посмотреть описание процедуры элиминации кванторов для похожей теории, которая встречается в учебнике Мендельсона на стр. 106 - 107. Этого может быть пока не достаточно, но в любом случае будет полезно, так как многие применяемые приёмы являются общими.

(21 Ноя 11:34) falcao

@falcao, спасибо, сейчас ознакомлюсь.

(21 Ноя 11:52) Pointer

@Pointer: я вроде бы продумал детали доказательства. Но то рассуждение из Мендельсона лучше иметь в виду как отправную точку.

(21 Ноя 16:18) falcao

@falcao, я уже ознакомился, будет очень интересно увидеть доказательство от Вас, так как я к нему не пришел, пока что ничего не складывается.

(21 Ноя 17:46) Pointer
10|600 символов нужно символов осталось
1

Попробую изложить.

Для начала избавляемся от кванторов всеобщности по правилу замены (Ax)Ф на not((Ex)not(Ф)). Будем постепенно элиминировать кванторы. Приводить к предварённой нормальной форме не обязательно.

Отрицания атомарных формул также преобразуем: not(u=v) заменяем на (u < v) or (v < u); not (u < v) на (u=v) or (v < u).

Рассмотрим подформулу вида (Ex)Ф, где Ф бескванторная. Записываем Ф в виде дизъюнкции конъюнкций атомарных. Пользуясь тем, что (Ex)(A V B V ...) заменяется на (Ex)A V (Ex) B V ... , сводим всё к случаю, когда Ф -- конъюнкция.

Временно разрешим все термы вида x+k, где k -- любая целая константа. В конце от них можно будет избавиться, прибавляя к обеим частям достаточно большое натуральное число, а при m>=0 терм x+m превращается в S...Sx, где S применено m раз.

Если переменная x не входит в Ф, то квантор отбрасываем. Если x входит в состав равенства, то записываем его как x=y+k при целом k. В случае y=x получаем или тождественную истину, или тождественную ложь, и формулу упрощаем. Если y -- какая-то другая переменная, то заменяем все вхождения x в Ф на y+k, отбрасывая квантор.

Неравенства, для которых x фигурирует и слева, и справа, то есть x+s < x+t, также превращаются в истину или ложь. Считаем, что такого у нас нет.

Пусть теперь x входит только в состав неравенств. Разрешаем их относительно x. Допустим, что все неравенства имеют вид y+k < x, где x находится только в правой части. При фиксированных значениях остальных переменных, x можно всегда выбрать достаточно большим, чтобы все они выполнялись. Квантор по x убираем, все неравенства с участием x тоже.

Если у всех неравенств x встречается только в левой части, то поступаем аналогично.

Основной случай: имеется несколько неравенства вида a(i) < x, и несколько вида x < b(j), где a(i), b(j) -- термы. Удовлетворяющее им значение x существует тогда и только тогда, когда max a(i) как минимум на 2 меньше min b(j). Берём такие неравенства по всем парам i, j, записывая их в виде S(a(i)) < S(b(j)) по всем парам, убирая x и квантор.

После нескольких шагов процесса формула становится бескванторной. Там, где берётся отрицание полученной бескванторной формулы, мы её обрабатываем как выше: сначала по законам де Моргана, потом избавляемся от отрицаний атомарных.

ссылка

отвечен 22 Ноя 4:08

10|600 символов нужно символов осталось
Ваш ответ

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

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

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

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

отмечен:

×928

задан
21 Ноя 3:15

показан
64 раза

обновлен
22 Ноя 4:08

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

по почте:

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

по RSS:

Ответы

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

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