2014 dxdy logo

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

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


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


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

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

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

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

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



Начать новую тему Ответить на тему
 
 Мат. логика и теория алгоритмов
Сообщение12.03.2015, 19:29 


28/01/14
10
Доказать формально выражение $C \to (A   \wedge B   \to B   \vee C)$, используя правило подстановки, правило "модус поненс" и системы аксиом.
Пользуясь аксиомами
$A \to (B \to A)  (1)$
$(A \to (B \to C)) \to ((A \to B) \to (A \to C))  (2)$,
пришел в тупик.
Сделал подстановку $C$ вместо $A$, $A \wedge B$ вместо $B$, $B \vee C$ в аксиоме (2), получил
$(C \to (A \wedge B \to B \vee C)) \to ((C \to A \wedge B) \to (C \to B \vee C))$.
Подскажите, как можно получить выражение $C \to (A \wedge B \to B \vee C)$ в следствии после некоторых подстановок вместо пропозициональных переменных, чтобы по правилу вывода доказать выводимость выражения?
Составил таблицу истинности и выяснил, что формула есть тавтологией, значит она должна выводиться из аксиом.

 Профиль  
                  
 
 Posted automatically
Сообщение12.03.2015, 20:02 
Супермодератор
Аватара пользователя


20/11/12
5697
 i  Тема перемещена из форума «Помогите решить / разобраться (М)» в форум «Карантин»
Причина переноса: не приведены попытки решения, формулы неправильно оформлены $\TeX$ом

DonVito
Приведите попытки решения, укажите конкретные затруднения.
Наберите все формулы и термы $\TeX$ом правильно: каждая формула целиком заключается в одну пару долларов.
Инструкции по оформлению формул здесь или здесь (или в этом видеоролике).
См. также тему Что такое карантин, и что нужно делать, чтобы там оказаться.
После исправлений сообщите в теме Сообщение в карантине исправлено, и тогда тема будет возвращена.

 Профиль  
                  
 
 Posted automatically
Сообщение12.03.2015, 23:39 
Модератор


20/03/14
8218
 i  Тема перемещена из форума «Карантин» в форум «Помогите решить / разобраться (М)»

 Профиль  
                  
 
 Re: Мат. логика и теория алгоритмов
Сообщение13.03.2015, 01:13 
Аватара пользователя


01/12/06
535
мсср
Аксиом не хватает. План такой:
1. $C\to B\vee C$ - аксиома
2. $(C\to B\vee C)\to [A\wedge B\to (C\to B\vee C)]$ - аксиома
3. $A\wedge B\to (C\to B\vee C)$ - MP 1, 2
4. $[A\wedge B\to (C\to B\vee C)]\to [C\to (A\wedge B\to B\vee C)]$ - перестановка посылок
5. $C\to (A\wedge B\to B\vee C)$ - MP 3, 4
Теперь надо вставить в этот список доказательство формулы 4. Доказательство теоремы о дедукции содержит метод нахождения формальных доказательств.

 Профиль  
                  
 
 Re: Мат. логика и теория алгоритмов
Сообщение13.03.2015, 01:47 


28/01/14
10
gefest_md в сообщении #989567 писал(а):
Аксиом не хватает. План такой:
1. $C\to B\vee C$ - аксиома
2. $(C\to B\vee C)\to [A\wedge B\to (C\to B\vee C)]$ - аксиома
3. $A\wedge B\to (C\to B\vee C)$ - MP 1, 2
4. $[A\wedge B\to (C\to B\vee C)]\to [C\to (A\wedge B\to B\vee C)]$ - перестановка посылок
5. $C\to (A\wedge B\to B\vee C)$ - MP 3, 4
Теперь надо вставить в этот список доказательство формулы 4. Доказательство теоремы о дедукции содержит метод нахождения формальных доказательств.

Доказывается ли формула 4 как-то без теоремы о дедукции?

 Профиль  
                  
 
 Re: Мат. логика и теория алгоритмов
Сообщение13.03.2015, 03:11 
Заслуженный участник
Аватара пользователя


27/04/09
22977
Уфа
Теорема о дедукции — это метатеорема, говорящая о существовании одного вывода, если существует другой. Так что да.

 Профиль  
                  
 
 Re: Мат. логика и теория алгоритмов
Сообщение13.03.2015, 05:56 
Заслуженный участник
Аватара пользователя


20/07/09
3883
МФТИ ФУПМ
$A \to B, B \to C \vdash A \to C$ умеете доказывать?

$C \to (B \to C)$ — аксиома
$(B \to C) \to (\neg(A \to B) \to (B \to C))$ — аксиома
получаем $C \to (\neg(A \to B) \to (B \to C))$.
Вместо $B$ подставляем $\neg B$, получаем требуемую формулу: $A \vee B = \neg A \to B, A \wedge B= \neg(A \to \neg B)$
$$C \to (A \wedge B \to (B \vee C))$$

 Профиль  
                  
 
 Re: Мат. логика и теория алгоритмов
Сообщение13.03.2015, 13:09 
Аватара пользователя


01/12/06
535
мсср
Доказывать сразу формулу $C\to(A\wedge B\to B\vee C)$ не легко. Поэтому сначала можно доказать формулу $A\wedge B\to B\vee C$ из допущения $C$, т.е. $C\vdash A\wedge B\to B\vee C.$ Дальше есть две возможности:
1. Применяем теорему дедукции если это разрешается условием задачи.
2. Переделываем доказательство $C\vdash A\wedge B\to B\vee C$ в доказательство $\vdash C\to(A\wedge B\to B\vee C)$ так, как это показано в доказательстве теоремы о дедукции. Поэтому доказательство теоремы о дедукции полезно знать.

Итак вот доказательство формулы $A\wedge B\to B\vee C$ из допущения $C$ (данный вывод):

1. $C$ - допущение
2. $C\to B\vee C$ - аксиома
3. $B\vee C$ - МП, 1, 2.
4. $B\vee C\to(A\wedge B\to B\vee C)$ - аксиома (1)
5. $A\wedge B\to B\vee C$ - МП, 3, 4

Теперь повторяем доказательство теоремы о дедукции: приписываем спереди к каждой из формул данного вывода символы $C\to$:

...
$C\to C$
...
$C\to (C\to B\vee C)$
...
$C\to B\vee C$
...
$C\to (B\vee C\to(A\wedge B\to B\vee C))$
...
$C\to (A\wedge B\to B\vee C)$

Эта последовательность ещё не вывод формулы $C\to (A\wedge B\to B\vee C)$, но можно перед каждой формулой вставить дополнительные формулы так, чтобы она превратилась в вывод формулы $C\to (A\wedge B\to B\vee C)$.
(Предыдущий план можно оставить без внимания. Он ведёт к намного более длинному доказательству.)

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

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



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

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


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

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