2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


В этом разделе нельзя создавать новые темы.

Если Вы хотите задать новый вопрос, то не дописывайте его в существующую тему, а создайте новую в корневом разделе "Помогите решить/разобраться (М)".

Если Вы зададите новый вопрос в существующей теме, то в случае нарушения оформления или других правил форума Ваше сообщение и все ответы на него могут быть удалены без предупреждения.

Не ищите на этом форуме халяву, правила запрещают участникам публиковать готовые решения стандартных учебных задач. Автор вопроса обязан привести свои попытки решения и указать конкретные затруднения.

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



Начать новую тему Ответить на тему
 
 Доказать теорему в теории L4
Сообщение15.06.2013, 20:20 


13/01/13
30
Доброго времени суток. Помогите, пожалуйста, доказать следующую теорему в теории $L_4$:

$\vdash _L_4  \neg B \rightarrow (B \rightarrow C)$

Собственно, с решением совсем глухо, ибо формализованного четкого подхода к решениям такого типа задач нет, а опыт - пара с грехом пополам доказанных теорем в теории $L$. Для $L_4$ имею перед собой только набор аксиом, попытки применить их ни к чему хорошему не привели, по этой причине и обращаюсь к более сведущим с просьбой о помощи.

 Профиль  
                  
 
 Re: Доказать теорему в теории L4
Сообщение15.06.2013, 20:35 
Заслуженный участник


08/04/08
8556
YgolovnicK в сообщении #737068 писал(а):
в теории $L_4$
А что это за теория? Или эквивалентный вопрос: какие у нее аксиомы?

 Профиль  
                  
 
 Re: Доказать теорему в теории L4
Сообщение15.06.2013, 21:37 


13/01/13
30
Теория $L_4$:
Примитивными связками служат $\rightarrow , \& , \vee, \neg $
Набор аксиом:
1)$ A \rightarrow (B \rightarrow A)$
2) $ (A \rightarrow (B \rightarrow C )) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$
3) $A \& B \rightarrow A$
4) $A \& B \rightarrow B$
5) $A \rightarrow (B \rightarrow (A \& B))$
6) $A \rightarrow (A \vee B)$
7) $B \rightarrow (A \vee B) $
8) $(A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow ((A \vee B) \rightarrow C))$
9) $(A \rightarrow B) \rightarrow (( A \rightarrow \neg B) \rightarrow \neg A)$
10) $\neg \neg A \rightarrow A$

$A \equiv B$ означает $(A \rightarrow B) \& (B \rightarrow A)$

 Профиль  
                  
 
 Re: Доказать теорему в теории L4
Сообщение15.06.2013, 21:53 
Заслуженный участник


08/04/08
8556
(Если не ошибаюсь, то $L_4$ - исчисление высказываний с системой аксиом Гильберта.)

Теоремой дедукции пользоваться можно?

 Профиль  
                  
 
 Re: Доказать теорему в теории L4
Сообщение15.06.2013, 22:17 


13/01/13
30
На счет того, что такое $L_4,$ ничего конкретного сказать не могу, не в курсе.
Полагаю, что теорема дедукции работает и здесь, т.к. для доказательства её работы в теории $L$ потребовались лишь первые 2 аксиомы, которые идентичны первым двум в теории $L_4$

 Профиль  
                  
 
 Re: Доказать теорему в теории L4
Сообщение16.06.2013, 07:49 
Заслуженный участник


08/04/08
8556
YgolovnicK в сообщении #737090 писал(а):
Полагаю, что теорема дедукции работает и здесь, т.к. для доказательства её работы в теории $L$ потребовались лишь первые 2 аксиомы, которые идентичны первым двум в теории $L_4$
Значит пользуемся. Тогда так: Примените к искомой формуле теорему дедукции - получите вывод, который Вам надо найти. Теперь подсказка: достаточно пользоваться аксиомами 1,2,9. И еще подсказка: Вам надо вывести из одного утверждения совершенно другое. Посмотрите, какие аксиомы позволяют новое утверждение, хотя и в связи старым, а какие аксиомы позволяют эту разорвать связь одного утверждения с другим?

 Профиль  
                  
 
 Re: Доказать теорему в теории L4
Сообщение16.06.2013, 09:40 


13/01/13
30
Вот меня как то смущает тот факт, что получается 2 гипотезы, $B, \neg B$, которые противоречивы. Или не надо так брать? взять только $\neg B$? До того, как увидел Ваш пост, получилось нечто такое:
1) $\neg B$ гипотеза
2) $B$ гипотеза
3) $B \rightarrow (B \vee C)$ 6 аксиома
4) 2 к 3 MP $B \vee C$
5) $B \vee C$ есть то же самое, что и $( \neg A) \rightarrow C$
6) 1 к 5 MP, $C$
Получили $C$. 2 раза теорему дедукции к $ \neg B, B \vdash C$, получаем искомое $\vdash  \neg B \rightarrow (B \rightarrow C)$

 Профиль  
                  
 
 Re: Доказать теорему в теории L4
Сообщение16.06.2013, 10:12 
Заслуженный участник


08/04/08
8556
YgolovnicK в сообщении #737193 писал(а):
Вот меня как то смущает тот факт, что получается 2 гипотезы, $B, \neg B$, которые противоречивы. Или не надо так брать? взять только $\neg B$?
Все правильно! Т.е. мы должны доказать, $B,\neg B\vdash C$, т.е., что из противоречивых гипотез следует, что угодно. Из одной гипотезы такого мы, естественно, не получим.

YgolovnicK в сообщении #737193 писал(а):
До того, как увидел Ваш пост, получилось нечто такое:
1) $\neg B$ гипотеза
2) $B$ гипотеза
3) $B \rightarrow (B \vee C)$ 6 аксиома
4) 2 к 3 MP $B \vee C$
5) $B \vee C$ есть то же самое, что и $( \neg A) \rightarrow C$
Ага, я тоже сначала так начал :-) Это обычная ошибка - вносить в ИВ факты или инструменты из АВ. Дело в том, что мы не знаем того, что
YgolovnicK в сообщении #737193 писал(а):
5) $B \vee C$ есть то же самое, что и $( \neg A) \rightarrow C$
В аксиомах это не прописано. А доказать просто это не получается - у меня получилось, что требуется для этого сначала доказать $\vdash B\to(\neg B \to C)$ :-) Сразу также скажу, что заменять одну подформулу на ей эквивалентную в ИВ тоже нельзя - нет соответствующих правил. Т.е. в ИВ технически сложнее работать, чем в АВ: у нас есть только схемы аксиом и MP и больше ничего.
Все-таки, попробуйте воспользоваться только 1,2 и 8.

 Профиль  
                  
 
 Re: Доказать теорему в теории L4
Сообщение16.06.2013, 11:19 


13/01/13
30
Пока не придумал, как использовать только 1,2,9 (полагаю, в последнем сообщении у Вас, Sonic86, опечатка).
Рассуждения привели меня к следующему:
1)$\neg B$ гипотеза
2)$B$ гипотеза
3) $B \rightarrow ( \neg C \rightarrow B)$ 1 аксиома
4) 2 к 3 MP, $\neg C \rightarrow B$
5)$(\neg C \rightarrow B) \rightarrow (( \neg C \rightarrow \neg B) \rightarrow \neg \neg C)$ 9 аксиома
6) 4 к 5 MP, $( \neg C \rightarrow \neg B) \rightarrow \neg \neg C$
7) $\neg B \rightarrow (\neg C \rightarrow \neg B)$, 1 аксиома
8) 1 к 7 MP, $ \neg C \rightarrow \neg B$
9) 8 к 6 MP, $\neg \neg C$
10) $\neg \neg C \rightarrow C$ 10 аксиома
11) 9 к 10 MP, $C$

 Профиль  
                  
 
 Re: Доказать теорему в теории L4
Сообщение16.06.2013, 11:27 
Заслуженный участник


08/04/08
8556
Ну вот, поздравляю, мучения были не напрасны :-)

YgolovnicK в сообщении #737228 писал(а):
Пока не придумал, как использовать только 1,2,9 (полагаю, в последнем сообщении у Вас, Sonic86, опечатка).
Да, опечатка

 Профиль  
                  
 
 Re: Доказать теорему в теории L4
Сообщение16.06.2013, 11:29 


13/01/13
30
т.е. мои суждения верны, и вывод построен верно?

 Профиль  
                  
 
 Re: Доказать теорему в теории L4
Сообщение16.06.2013, 11:55 
Заслуженный участник


08/04/08
8556
YgolovnicK в сообщении #737232 писал(а):
т.е. мои суждения верны, и вывод построен верно?
Да. Еще надо указать, что пользовались теоремой дедукции (самой теоремой, или обратной к ней - я не помню)

 Профиль  
                  
 
 Re: Доказать теорему в теории L4
Сообщение16.06.2013, 12:07 


13/01/13
30
Ура!
Благодарю за помощь :D

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 13 ] 

Модераторы: Модераторы Математики, Супермодераторы



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

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


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

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group