НГУ

Форумы НГУ
Текущее время: Вс апр 21, 2019 9:26 pm

Часовой пояс: UTC + 7 часов




Начать новую тему Ответить на тему  [ Сообщений: 18 ]  На страницу 1, 2  След.
Автор Сообщение
 Заголовок сообщения: Важны ли аксиомы?
СообщениеДобавлено: Ср мар 01, 2006 10:01 pm 
Не в сети
Весьма плодовитый автор

Зарегистрирован: Чт сен 27, 2001 7:00 am
Сообщения: 1637
Тема звучит весьма глобально, хе-хе. Речь же пойдёт о скромной задачке. Рассмотрим исчисление секвенций для логики высказываний - например, в том виде, который изложен в задачнике И.А. Лаврова и Л.Л. Максимовой по мат. логике. Напомним, что аксиомы этого исчисления имеют вид
"A|-A"
для некоторой формулы A.

Зафиксируем какую-то переменную P и удалим из исчисления единственную аксиому P|-P. Вопрос: будет ли новое исчисление эквивалентно исходному? Т.е. останутся ли доказуемыми все тождественно истинные секвенции? Задача возникла после вопроса одного из студентов на семинаре.

_________________
Не беги от снайпера - умрёшь усталым


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Вт мар 07, 2006 11:02 am 
Не в сети
Постоянный посетитель

Зарегистрирован: Вт дек 14, 2004 4:37 pm
Сообщения: 177
Откуда: Вдовин Евгений Петрович
Павел, а сама аксиома P|-P выводиться будет?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Вт мар 07, 2006 6:30 pm 
Не в сети
Весьма плодовитый автор

Зарегистрирован: Чт сен 27, 2001 7:00 am
Сообщения: 1637
veprus писал(а):
Павел, а сама аксиома P|-P выводиться будет?

Это эквивалентная постановка задачи - если недостающая аксиома выводится, то и всё остальное тоже выводится. Если же нет, то исчисления неравносильны.

_________________
Не беги от снайпера - умрёшь усталым


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: аксиомы
СообщениеДобавлено: Ср мар 08, 2006 1:07 pm 
Не в сети
Редкий гость

Зарегистрирован: Пт сен 29, 2006 8:35 am
Сообщения: 3
Логично ответить, что навряд ли. Хотя вопрос довольно странный. Почему, к примеру, было тогда уж не спросить о минимальности правил вывода (т.е. их количества)? Решение этого вопроса не даёт нам существенных подвижек. Проще - так, как есть.

И это не отмазка. Само ИС в том виде, в котором оно введено - это удобство. Ясно, что секвенция - это по сути обобщённая импликация. И эквивалентна ей как в плане семантическом, так и в синтаксическом (в нашем исчислении, разумеется): A1,...,An|-B <=> |-(A1&...&An)->B. Импликация - вспомогательный символ при v,& и -, которые в свою очередь - для стрелки Пирса (или штриха Шеффера).

Но всё же - вопрос интересный. Проблема - доказательство. Т.к. я уверен, что НЕТ.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: аксиомы
СообщениеДобавлено: Ср мар 08, 2006 3:16 pm 
Не в сети
Весьма плодовитый автор

Зарегистрирован: Чт сен 27, 2001 7:00 am
Сообщения: 1637
S.O. Smerdov писал(а):
... вопрос довольно странный. Почему, к примеру, было тогда уж не спросить о минимальности правил вывода (т.е. их количества)?

Вы полагаете, что с повышением сложности вопроса его странность понижается? :)
Вопросы о правилах тоже хорошие - можно поразмышлять и над ними. Просто для некоторых правил я доказательство их необходимости давно знаю.

_________________
Не беги от снайпера - умрёшь усталым


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Ср мар 08, 2006 4:39 pm 
Не в сети
Весьма плодовитый автор

Зарегистрирован: Чт сен 27, 2001 7:00 am
Сообщения: 1637
Некоторое дополнение:
(1) система правил вывода в задачнике Лаврова&Максимовой не является минимальной - некоторые правила можно убрать, и исчисление останется эквивалентным.
(2) доказательство существенности некоторых правил можно найти в книге: Ю.Л. Ершов, Е.А. Палютин "Математическая логика", глава 1, параграф 7.

Вообще, полезно было бы для задачника составить точный список - какие правила можно убрать, а какие нет.

_________________
Не беги от снайпера - умрёшь усталым


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Ср мар 08, 2006 7:13 pm 
Не в сети
Редкий гость

Зарегистрирован: Пт сен 29, 2006 8:35 am
Сообщения: 3
Дело не в "страности", а в том, настолько ли это важно для нас? Опять же при составлении дерева вывода мы не устраиваем соревнований: у кого вывод короче. В теории алгоритмов: не так уж важно, во сколько строк получилась программа для машины Шёнфилда, к примеру. Так что поиск оптимизации подобного рода не всегда оправдан. Хотя разумеется, весьма интересен вопрос о минимальности выбора достоверных оснований (на начальном этапе это признак приемлимости системы вообще). Конечно же, не в конкретном данном случае, так как корректность правил ИС достаточно очевидна.
/* Полнота - совсем иной вопрос. */


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Пт мар 10, 2006 9:56 am 
Не в сети
Постоянный посетитель

Зарегистрирован: Вт дек 14, 2004 4:37 pm
Сообщения: 177
Откуда: Вдовин Евгений Петрович
Павел, я понимаю, что это эквивалентные формулировки. И по-моему, P|-P не выводится. Если бы вывод был, то его было бы легко построить, как это всегда бывает в ИВ. А вот как доказать, что вывода не существует - не соображу.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Пт мар 10, 2006 1:13 pm 
Не в сети
Частый гость

Зарегистрирован: Чт апр 08, 2004 3:33 pm
Сообщения: 38
Мне тоже кажется, что секвенция P|-P не выводима в "обедненном" исчислении. Как это можно доказывать? Можно попробовать определить какую-нибудь числовую характеристику для каждой секвенции так, чтобы эта характеристика не уменьшалась при переходах сверху вниз по правилам вывода, и чтобы у секвенции P|-P эта характеристика была минимальной.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Вс мар 12, 2006 8:35 pm 
Не в сети
Весьма плодовитый автор

Зарегистрирован: Чт сен 27, 2001 7:00 am
Сообщения: 1637
Решение: ответ и правда отрицательный. Причём отрицательный для любой аксиомы вида A|-A, где A - некоторая формула. Чтобы это понять, нужно индукцией по длине вывода секвенции доказывать одновременно два утверждения:
(1) если секвенция вида
Г1,А,Г2,А,...,А,Гn |- B
выводима, то и секвенция
Г1,Г2,...,Гn |- B
тоже выводима;
(2) если секвенция вида
Г1,А,Г2,А,...,А,Гn |-
выводима, то и секвенция
Г1,Г2,...,Гn |-
тоже выводима.

Для аксиом это очевидно, для правил разбор несложен (Гi - конечные наборы формул). Решение, надо бы отметить, было найдено в беседе с моим соседом О.В.Кудиновым. Из задачи можно вывести любопытное следствие: если мы ищем вывод секвенции
A1,...,An |- B
и при этом ни одну из формул Ai из посылок убрать нельзя (чтобы секвенция осталась выводимой), то в дереве вывода обязательно появятся аксиомы
Ai |- Ai. Задача возникла после вопроса Дмитрия Луппова из гр. 5116.

P.S. У меня вопрос к модераторам: я выше написал ответ Станиславу Смердову, а теперь не могу найти его вопроса. У пользователей форума что, есть возможность удалять свои посты?

_________________
Не беги от снайпера - умрёшь усталым


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Пн мар 13, 2006 4:07 am 
Не в сети
Опытный автор

Зарегистрирован: Пн сен 13, 2004 12:08 am
Сообщения: 406
Павел, по-моему Вы под (1) и (2) написали что-то не то. Я, по крайней мере, ничерта не понимаю...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Пн мар 13, 2006 2:06 pm 
Не в сети
Весьма плодовитый автор

Зарегистрирован: Чт сен 27, 2001 7:00 am
Сообщения: 1637
SMS писал(а):
Павел, по-моему Вы под (1) и (2) написали что-то не то. Я, по крайней мере, ничерта не понимаю...

A - выбранная фиксированная формула, из исчислений удалена аксиома A|-A, Гi - произвольные наборы формул, возможно, пустые, B - произвольная формула, возможно, равная A. Смысл в том, что из правой части секвенции всегда можно выбросить A, и выводимость не утратится.

_________________
Не беги от снайпера - умрёшь усталым


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Пн мар 13, 2006 2:29 pm 
Не в сети
Непрерывный писатель

Зарегистрирован: Пт сен 07, 2001 7:00 am
Сообщения: 2844
Откуда: Станислав Березнюк
Павел, запись "Г1, А, Г2" принципиальна, или "А" между "Г1" и "Г2" вставилась случайно?

_________________
Мордор жил, Мордор жив, Мордор будет жить!


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Пн мар 13, 2006 6:13 pm 
Не в сети
Весьма плодовитый автор

Зарегистрирован: Чт сен 27, 2001 7:00 am
Сообщения: 1637
slb писал(а):
Павел, запись "Г1, А, Г2" принципиальна, или "А" между "Г1" и "Г2" вставилась случайно?

Принципиальна. Например, секвенция может иметь вид
Г1,А,Г2,А,Г3 |- B

_________________
Не беги от снайпера - умрёшь усталым


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Пн мар 13, 2006 6:42 pm 
Не в сети
Непрерывный писатель

Зарегистрирован: Пт сен 07, 2001 7:00 am
Сообщения: 2844
Откуда: Станислав Березнюк
Т.е. набор формул Гi - это "конечный непустой набор формул"?

_________________
Мордор жил, Мордор жив, Мордор будет жить!


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 18 ]  На страницу 1, 2  След.

Часовой пояс: UTC + 7 часов


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 3


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Перейти:  
Создано на основе phpBB® Forum Software © phpBB Group
Русская поддержка phpBB