Логика высказываний

[IvanEh]

Совсем не понимаю, как доказывать теоремы в системе аксиом L. Со стороны для это выглядит магией, в которой нужно иметь супер интуиции или же решать банальным перебором.
Мне нужно решить конкретно такой пример:
$(\overline{C}\implies \overline{A \wedge B}) \implies (\overline{C} \implies \overline{A}) \vee (\overline{C} \implies \overline {B})$

Система аксиом:

$A1: A \implies ( B \implies A)\\ A2: (A \implies ( B \implies C) \implies ((A \implies B) \implies (A \implies C)))\\ A3: (\lnot B \implice \lnot A) \implies ((\lnot B \implies A) \implies B) $

Можно использовать теоремы(10) MP и теорему о дедукции. Был бы рад комментариям, где бы были описаны причины выбора той или иной формулы

[Lia]

Тема перемещена из форума «Помогите решить / разобраться (М)» в форум «Карантин»
Тема перемещена в Карантин по следующим причинам:

1. Запишите формулы в соответствии с требованиями Правил форума, т.е. в $\TeX$.
Краткие инструкции можно найти здесь: topic8355.html и topic183.html.
Кроме этого, в теме Видео-пособия для начинающих форумчан можно посмотреть видео-ролик "Как записывать формулы".

2. Приведите свои попытки решения и/или укажите затруднения.

Исправьте все Ваши ошибки и сообщите об этом в теме Сообщение в карантине исправлено.
Настоятельно рекомендуется ознакомиться с темами Что такое карантин и что нужно делать, чтобы там оказаться и Правила научного форума.

[Lia]

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

[Sonic86]

IvanEh в сообщении #942706 писал(а):

Можно использовать теоремы(10)

Что за теоремы?

IvanEh в сообщении #942706 писал(а):

Мне нужно решить конкретно такой пример:
$(\overline{C}\implies \overline{A \wedge B}) \implies (\overline{C} \implies \overline{A}) \vee (\overline{C} \implies \overline {B})$

У Вас в формуле присутствуют связки $\vee, \wedge$, в указанных аксиомах они отсутствуют. Чего-то не хватает: определений связок или аксиом.
Еще нехорошо записывать отрицания разными символами.

Ну и

Lia в сообщении #942710 писал(а):

Приведите свои попытки решения или укажите затруднения.

[IvanEh]

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

IvanEh в сообщении #942706 писал(а):

Можно использовать теоремы(10)

Что за теоремы?

IvanEh в сообщении #942706 писал(а):

Мне нужно решить конкретно такой пример:
$(\overline{C}\implies \overline{A \wedge B}) \implies (\overline{C} \implies \overline{A}) \vee (\overline{C} \implies \overline {B})$

У Вас в формуле присутствуют связки $\vee, \wedge$, в указанных аксиомах они отсутствуют. Чего-то не хватает: определений связок или аксиом.
Еще нехорошо записывать отрицания разными символами.

Ну и

Lia в сообщении #942710 писал(а):

Приведите свои попытки решения или укажите затруднения.

Все операции нужно заменить на импликацию. Я пробовал использовать теоремы и аксиомы, но я не могу уловить сути, когда что нужно использовать

[Sonic86]

IvanEh в сообщении #946720 писал(а):

Все операции нужно заменить на импликацию.

Тогда я могу в общем посоветовать только применять MP, пока это возможно, а дальше уже пытаться комбинировать посылки и аксиомы.

IvanEh в сообщении #946720 писал(а):

Я пробовал использовать теоремы и аксиомы, но я не могу уловить сути, когда что нужно использовать

К сожалению, тут трудно советовать, для меня это тоже в основном перебор и телепатия. Попробуйте сначала применить MP, потом надо смотреть. Без MP было бы еще сложнее.

[vlad_light]

(Оффтоп)

А зачем вообще нужны такие задания, какая от них польза?

[Sonic86]

(Оффтоп)

vlad_light в сообщении #946835 писал(а):

А зачем вообще нужны такие задания, какая от них польза?

Применение аксиоматического метода в логике. Применение начинается с исчисления высказываний. Затем идет на исчисление предикатов. Про вторую теорему Геделя слыхали? Вот то-то и оно.

[arseniiv]

Вывод перестаёт быть магией, если выведены правила введения и удаления связок (например, для конъюнкции это

$$\begin{array}{ccc} \dfrac{A,\;B}{A\wedge B} \; (\wedge^+), & \dfrac{A\wedge B}A \; (\wedge^-_1), & \dfrac{A\wedge B}B \; (\wedge^-_2). \end{array}$$

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

Маленький и искуственный, но пример к методу: докажем коммутативность конъюнкции $A\wedge B\vdash B\wedge A$:
\begin{array}{rll} 1. & A\wedge B & \text{(гипотеза)} \\ 2. & A & \text{(}\wedge^-_1\text{, 1)} \\ 3. & B & \text{(}\wedge^-_2\text{, 1)} \\ 4. & B\wedge A & \text{(}\wedge^+\text{, 3, 2)} \\ \end{array}

Аксиомы Клини позволяют подобные правила выводить довольно легко. (Вы можете вывести эти аксиомы из своих, если захотите.) Например, $A,B\vdash A\wedge B$, что и рождает правило $\wedge^+$, показывается применением теоремы о дедукции к $\vdash A\to(B\to A\wedge B)$ (это аксиома 3): получим сначала $A\vdash B\to A\wedge B$, а потом и $A,B\vdash A\wedge B$. Выводимости $A\wedge B\vdash A$ и $A\wedge B\vdash B$ показываются однократным применением теоремы о дедукции к аксиомам 6, 7. И так практически с каждым правилом введения/удаления.

-- Пн дек 15, 2014 23:28:00 --

Кстати, можно заметить, что MP — это самое что ни на есть $\to^-$.