Доказать в исчислении высказываний

[eholot]

Доказать в исчислении высказываний (буквы обозначают произвольные формулы):
$(A\to B) \to((C \lor (A \to C)) \lor B)$
есть 3 аксиомы:
1. $ A \to (B \to A)$
2.$(A \to (B \to C)) \to ((A \to B) \to (A \to C))$
3.$(\neg B \to \neg A) \to ((\neg B \to A) \to B)$

и 9 сенкквенций:
1. $(A \to B, B \to C) \vdash A \to C $
2. $A \to (B \to C), B \vdash A \to C $
3. $ \vdash(\neg \neg A \to A)$
4. $\vdash(A \to \neg \neg A)$
5. $\vdash A \to (\neg A \to B)$
6. $ \vdash(\neg B \to \neg A) \to (A \to B)$
7. $\vdash (A \to B) \to (\neg B \to \neg A)$
8.$\vdash (A \to (\neg B \to \neg (A \to B)))$
9.$\vdash (A \to B) \to ((\neg A \to B) \to B)$

с чего хоть начать? какую из этих формул можно применить?
Спасибо.

[Sonic86]

eholot в сообщении #699830 писал(а):

и 9 сенкквенций:

В смысле приведенными выводимостями можно пользоваться для доказательства 1-й формулы? Или их тоже вывести нужно?
Можно ли пользоваться теоремой дедукции? Правило вывода modus ponens тоже есть?

eholot в сообщении #699830 писал(а):

с чего хоть начать? какую из этих формул можно применить?

Сначала надо хотя бы связку $\vee$ в формуле, которую хотите доказать, переписать через связку $\to$.

[eholot]

секвенциями можно пользоваться, выводить их не надо.
теоремой дедукции и модус понес тоже можно.

правильно ли я понимаю:
если $P \lor Q \Leftrightarrow Q \lor P$ и $P \lor Q \Leftrightarrow \neg P \to Q$

значит
$((C \lor (A \to C)) \lor B) \Leftrightarrow (B \lor (C \lor (A \to C))) \Leftrightarrow ( \neg B \to (C \lor (A \to C))) \Leftrightarrow $ ( \neg B \to ( \neg C \to (A \to C)))

[Sonic86]

eholot в сообщении #699849 писал(а):

теоремой дедукции и модус понес тоже можно.

О, хорошо.

eholot в сообщении #699849 писал(а):

значит
$((C \lor (A \to C)) \lor B) \Leftrightarrow (\neg B \to (\neg C \to (A \to C)))$

Согласно теореме дедукции, исходная формулы выводима тогда и только тогда, когда из гипотез выводима формула, получаемая из исходной формулы многократным применением теоремы дедукции до упора. Вот можно ее выписать и там видно, что она распадается на подзадачу и "остаток".
Это, конечно, не единственный способ (м.б. Вам надо явно вывод построить?)
Ну вообще простых алгоритмов вывода вроде нет. Можете сами попытаться сделать пару выводов, заметить какие-то закономерности, потом попытаться их применить...

[eholot]

честно говоря, не очень понял...

[Sonic86]

eholot в сообщении #699856 писал(а):

честно говоря, не очень понял...

теорема дедукции утверждает следующее: $X\vdash Y \Leftrightarrow \vdash (X\to Y)$. С помощью нее Вы можете доказывать не $\vdash (X\to Y)$, а $X\vdash Y$. Построение 2-го вывода мне кажется легче: увеличивается число посылок слева, укорачивается формула, которую надо вывести, посылки становятся "несимметричными", что помогает выбирать то, что можно пытаться выводить. Я Вам предлагаю из Вашей исходной формулы (запишите ее явно) построить с помощью теоремы дедукции записать выражение вида $X\vdash Y$.

[eholot]

Sonic86 в сообщении #699859 писал(а):

eholot в сообщении #699856 писал(а):

честно говоря, не очень понял...

теорема дедукции утверждает следующее: $X\vdash Y \Leftrightarrow \vdash (X\to Y)$. С помощью нее Вы можете доказывать не $\vdash (X\to Y)$, а $X\vdash Y$. Построение 2-го вывода мне кажется легче: увеличивается число посылок слева, укорачивается формула, которую надо вывести, посылки становятся "несимметричными", что помогает выбирать то, что можно пытаться выводить. Я Вам предлагаю из Вашей исходной формулы (запишите ее явно) построить с помощью теоремы дедукции записать выражение вида $X\vdash Y$.

$(A\to B) \to((C \lor (A \to C)) \lor B)$
$(A\to B)\vdash ((C \lor (A \to C)) \lor B)$
$(A\to B) \vdash (\neg B \to ( \neg C \to (A \to C)))$

[Sonic86]

eholot в сообщении #699876 писал(а):

$(A\to B) \to((C \lor (A \to C)) \lor B)$
$(A\to B)\vdash ((C \lor (A \to C)) \lor B)$

Ага.

eholot в сообщении #699876 писал(а):

$(A\to B)\vdash ((C \lor (A \to C)) \lor B)$
$(A\to B) \vdash (\neg B \to ( \neg C \to (A \to C)))$

А этот переход откуда? Если Вы воспользовались коммутативностью дизъюнкции, то у Вас вообще-то этой коммутативности нету. Либо ее надо выводить и там применять (было бы очень удобно, кстати)
После преобразования удобно применить теорему дедукции еще раз.

[eholot]

Sonic86 в сообщении #699895 писал(а):

А этот переход откуда?

если $P \lor Q \Leftrightarrow Q \lor P$ и $P \lor Q \Leftrightarrow \neg P \to Q$
значит
$((C \lor (A \to C)) \lor B) \Leftrightarrow (B \lor (C \lor (A \to C))) \Leftrightarrow ( \neg B \to (C \lor (A \to C))) \Leftrightarrow $ ( \neg B \to ( \neg C \to (A \to C)))

или это неправильно?

Sonic86 в сообщении #699895 писал(а):

После преобразования удобно применить теорему дедукции еще раз.

то есть правильно я понимаю:
$(A\to B) \vdash (\neg B \to ( \neg C \to (A \to C)))$
$\neg B \vdash (\neg C \to (A \to C))$

[Sonic86]

eholot в сообщении #699901 писал(а):

$P \lor Q \Leftrightarrow Q \lor P$

Ну я и говорю: Вы пользуетесь коммутативностью дизъюнкции, но у нас она разве есть? У нас же ничего кроме MP, теоремы дедукции, аксиом и 9 секвенций нету. Впрочем, у нас есть секвенции 6 и 7, но тогда надо попытаться применить их предварительно.

eholot в сообщении #699901 писал(а):

или это неправильно?

Кстати, знака $\Leftrightarrow$ в ИВ тоже нет (т.е. в выводе его не должно быть). В ИВ формула $A\vee B$ - это просто обозначение $\neg A\to B$, причем никаких свойств этого обозначения мы не знаем (хотя они есть). Если мы какие-то его свойства хотим использовать, то их доказать нужно.

eholot в сообщении #699901 писал(а):

то есть правильно я понимаю:
$(A\to B) \vdash (\neg B \to ( \neg C \to (A \to C)))$
$\neg B \vdash (\neg C \to (A \to C))$

Если Вы до 1-й формулы дойдете (пока явно не дошли), то не так: у Вас 1-я гипотеза слева пропала, должно получиться две гипотезы:
$(A\to B) \vdash (\neg B \to ( \neg C \to (A \to C)))$ выводимо тогда и только тогда, когда выводимо $(A\to B), \neg B \vdash \neg C \to (A \to C)$. Опять же, если до исходной точки дойдем, то можем применить теорему дедукции уже 3-й раз.

[eholot]

спасибо большое за помощь, сейчас как раз на лекцию по логике иду ) уточню можно ли применять коммутативность дизьюнкции

[Sonic86]

eholot в сообщении #699917 писал(а):

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

там еще нужно учесть следующее: в алгебре высказываний мы не просто знаем, что дизъюнкция коммутативна, мы еще и можем заменять в формуле любую подформулу на эквивалентную (в частности, если где-то внутри длинной формулы у нас появилась дизъюнкция, мы можем внутри переставить ее члены). В исчислении высказываний такого явно нет: преобразовать подформулу в формуле можно лишь преобразовывая всю формулу явно (что, естественно, сложнее), либо надо использовать специальные правила вывода для этого.

[arseniiv]

Sonic86 в сообщении #699915 писал(а):

В ИВ формула $A\vee B$ - это просто обозначение $\neg A\vee B$

Опечатка, $\neg A\to B$ ведь.

[Sonic86]

arseniiv в сообщении #699949 писал(а):

Опечатка, $\neg A\to B$ ведь.

Ой, действительно, сейчас исправлю.

[Cort]

Здравствуйте! У меня аналогичный пример.
Вот к чему я пришел.
(A\to B)\to ((C\vee (A\to C))\vee B)
Было разрешено делать преобразование конъюнкции и дизъюнкции в импликации и обратно во внутренних импликации.
Таким образом
(A\to B)\to (\neg (C\vee (A\to C))\to B)
1) (A\to B) -гипотеза
2) \neg (C\vee (A\to C)) -гипотиза
3) \neg C\wedge \neg(A\to C) -по де Моргану
4) \neg C -свойство конъюнкции
5) \neg(A\to C) -свойство конъюнкции

Подскажите куда мне двигаться. Я же должен в итоге получить B?