НГУ

Форумы НГУ
Текущее время: Сб авг 24, 2019 10:25 pm

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




Начать новую тему Ответить на тему  [ Сообщений: 20 ]  На страницу Пред.  1, 2
Автор Сообщение
 Заголовок сообщения:
СообщениеДобавлено: Чт май 15, 2008 5:03 pm 
Не в сети
Частый гость

Зарегистрирован: Пт апр 11, 2008 4:38 am
Сообщения: 27
Всё, я нашел способ доказательства существования такой формулы!
Вещь оказалась тревиальная, достаточно было модернизировать
формулу P=(x-->y’)’ , что бы получить необходимый результат.
Понятно, что формула P=(x-->y’)’ - истинна, тогда и только тогда когда х истинно. Но х - сама может являться формулой, причём имеющей тот же вид, что и исходная т.е. P=(G-->y’)’ и
G=(z-->х’)’ , но G, как легко видеть, только тогда истинна, когда
z и x одновременно истинны. Потому, формула P=((z-->х’)’-->y’)’ истинна, тогда и только тогда, когда х,y,z - одновременно истинны.
* * * * * * *
У меня возникла теперь задача: доказать, что система аксиом - независима. Я читал, что это осуществляется при помощи построения, так называемой "модели". К сожалению, понятие "модель" - настолько абстрактое, что уловить его сущность я не смог. Потому, хотел бы попросить Вас, показать на любой из описанной в этой теме систем,
каким образом можно построить модель. Особенно меня интересует вопрос - почему именно существование модели доказывает независимость системы аксиом?

_________________
Единственный способ установить границы возможного - это выйти за них в невозможное.


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

Зарегистрирован: Пт апр 11, 2008 4:38 am
Сообщения: 27
Господа, помогите наконец доказать независимость системы аксиом
исчисления (XY_ИВ). Идей вообще никаких нет, как говорится -"общее состояние непонятности".

_________________
Единственный способ установить границы возможного - это выйти за них в невозможное.


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

Зарегистрирован: Пт апр 25, 2008 10:04 pm
Сообщения: 15
Признаюсь сразу, что читал ветку очень поверхностно. Но кое-что напишу. Если под независимостью аксион понимать: аксиомы независимы, если никакую из них нельзя вывести из остальных, --- то доказать независимость при помощи построения модели можно следующим способом. Пусть у нас есть система аксиом a_1, ..., a_n, нужно доказать, что аксиома a_0 из них не выводится. Строим модель, на котрой a_0 ложна, a_1, ..., a_n истинны. Из существования такой модели следует невыводимость.


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

Зарегистрирован: Пт апр 11, 2008 4:38 am
Сообщения: 27
Не могли бы Вы на примере показать как строится модель.
Возьмём например две аксиомы
1. X
2. (X-->(X'-->X))
Как можно построить здесь модель?

_________________
Единственный способ установить границы возможного - это выйти за них в невозможное.


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

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 435
Amigo писал(а):
Не могли бы Вы на примере показать как строится модель.
Возьмём например две аксиомы
1. X
2. (X-->(X'-->X))
Как можно построить здесь модель?

Поскольку формула (X-->(X'-->X)) является тавтологией, с доказательством ее невыводимости будет напряг, ибо классические модели тут не подойдут: она в них будет всегда истинной. (Неклассические -- найдутся, но у меня есть только пара минут. Кстати, заранее извините за опечатки: некогда перечитывать написанное.) А классическую модель, обосновывающую невыводимость X из (X-->(X'-->X)), построить очень легко. Модель состоит всего лишь из одного бита x. (Бит -- это 0 или 1.) Индукцией по сложности формулы Ф определяется истинность Ф в модели (x) (пишут (x)|=Ф). Индуктивное определение такое:

(x)|=X, если x=1
(x)|=(F)', если (x)|=F неверно
(x)|=(F->G), если (x)|=F неверно или (x)|=G верно.

Легко показать, что MP сохраняет истинность формул в модели. Поэтому, если формулы F и G таковы, что (x)|=F верно, а (x)|=G неверно, то G нельзя вывести из F. Осталось заметить, что (0)|=(X-->(X'-->X)) верно, а (0)|=X неверно.

Если сигнатура состоит из двух переменных X и Y, то в качестве модели уже надо взять упорядоченную пару битиков (x,y) и чуток изменить определение истинности:

(x,y)|=X, если x=1
(x,y)|=Y, если у=1
остальное -- как и раньше.

Тогда, например, (1,0)|=X верно, а (1,0)|=Y неверно, а значит, Y нельзя вывести из X.


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

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


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

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


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

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