исчисление высказываний

[chencho]

Доказать что формулы а также обратные к ним являются теоремами исчисления высказываний
$(A \to C)\wedge(B \to C)) \to ((A\vee B) \to C)$
$(¬A \wee ¬B) \to ¬(A \wedge B)$
А эту только в одну сторону
$(A \to B) \vee (B \to A)$
Для решения использовать 11 аксиом и Modus Ponens.
Попробую начать решать первую а вы мне подскажите где ошибка...
$(A \to C)\wedge(B \to C)) \to ((A\vee B) \to C)$
Применим Лемму о дедукции 2 раза
Получим: Г$,(A \to C)\wedge(B \to C)),((A\vee B)|-C$ извините не знаю, как написать символ "выводится" в описании как пользоваться тэгом math не нашел...
Дальше: из$(A \to C)\wedge(B \to C))$ можем по Лемме 3 получить$(A \to C)\wedge(B \to C))$ или по лемме 4$(B \to C)$
С другой стороны : Из$(A\vee B) \to C)$ мы можем получить $C$ по правилу разбора случаев, получив его из $ A $ и$B$
А вот что дальше делать не знаю....(

[Maslov]

chencho в сообщении #347266 писал(а):

Для решения использовать 11 аксиом и Modus Ponens.

Вы бы написали эти 11 аксиом в тему, а то разные системы аксиом исчисления высказываний бывают. Или хоть скажите, из какого учебника. Из Клини?

chencho в сообщении #347266 писал(а):

Применим Лемму о дедукции 2 раза

Насколько я понял из условия, Вам теоремой о дедукции нельзя пользоваться. Или можно?

chencho в сообщении #347266 писал(а):

извините не знаю, как написать символ "выводится"

Символ "выводится" пишется так: $\vdash$

$\vdash$

[chencho]

Maslov в сообщении #347296 писал(а):

chencho в сообщении #347266 писал(а):

Для решения использовать 11 аксиом и Modus Ponens.

Вы бы написали эти 11 аксиом в тему, а то разные системы аксиом исчисления высказываний бывают. Или хоть скажите, из какого учебника. Из Клини?

Из Верещагина, Шеня.
В статье в википедии нумерация точно совпадает с Верещагином Шенем.

Maslov в сообщении #347296 писал(а):

chencho в сообщении #347266 писал(а):

Применим Лемму о дедукции 2 раза

Насколько я понял из условия, Вам теоремой о дедукции нельзя пользоваться. Или можно?

А почему ей нельзя пользоваться?

Maslov в сообщении #347296 писал(а):

chencho в сообщении #347266 писал(а):

извините не знаю, как написать символ "выводится"

Символ "выводится" пишется так: $\vdash$

$\vdash$

спасибо , буду иметь ввиду

[Maslov]

По поводу первой формулы:
$((A \to C) \land (B \to C)) \to ((A \lor B) \to C)$

Посмотрите внимательно на следующие схемы аксиом:
$(3)~ (A \land B) \to A$
$(4)~ (A \land B) \to B$
$(8)~ (A \to C) \to ((B \to C) \to (A \lor B \to C))$

Никаких мыслей в голову не приходит?

[chencho]

Maslov в сообщении #347351 писал(а):

По поводу первой формулы:
$((A \to C) \land (B \to C)) \to ((A \lor B) \to C)$

Посмотрите внимательно на следующие схемы аксиом:
$(3)~ (A \land B) \to A$
$(4)~ (A \land B) \to B$
$(8)~ (A \to C) \to ((B \to C) \to (A \lor B \to C))$

Никаких мыслей в голову не приходит?

$((A \to C) \land (B \to C)) \to (A \to C)$ по лемме 3
$((A \to C) \land (B \to C)) \to (B \to C)$ по лемме 4
возникает вопрос как связать эти 2 действия чтобы из
$(A \to C)\to(B \to C)$
Или из$(A \to C)$ по 8 лемме уже автоматически можно получить что из $(A \to C)\to(B \to C)$
И как в конце получить вывод упростить по Modus ponens?

[Maslov]

1) $((A \to C) \land (B \to C)) \to (A \to C)$ (A3)
2) $(A \to C) \land (B \to C)$ (посылка)
3) $A \to C$ (1, 2, MP)
4) $(A \to C) \to ((B \to C) \to (A \lor B \to C)$ (A8)
5) $(B \to C) \to (A \lor B \to C)$ (3, 4, MP)
6) $((A \to C) \land (B \to C)) \to (B \to C)$ (A4)
...

И не путайте леммы и аксиомы.

[Padawan]

Maslov в сообщении #347401 писал(а):

1) $((A \to C) \land (B \to C)) \to (A \to C)$ (A3)
2) $(A \to C) \land (B \to C)$ (посылка)
3) $A \to C$ (1, 2, MP)
4) $(A \to C) \to ((B \to C) \to (A \lor B \to C)$ (A8)
5) $(B \to C) \to (A \lor B \to C)$ (3, 4, MP)
6) $((A \to C) \land (B \to C)) \to (B \to C)$ (A4)
...

И не путайте леммы и аксиомы.

Посылки нет, должны быть только аксиомы использованы.

[chencho]

Maslov в сообщении #347401 писал(а):

$ 3) A \to C$ (1, 2, MP)

Просто цифрами вы обозначаете номера лемм?
Как здесь используются лемма 1 $D\to D$ и лемма о дедукции?
может быть у нас нумерация лемм различается?

Maslov в сообщении #347401 писал(а):

5) $(B \to C) \to (A \lor B \to C)$ (3, 4, MP)

Аналогично как здесь используются Леммы 3 и 4 ? $(A\wedge B)\vdash A $ $(A\wedge B)\vdash B $ Конъюнкцию же вроде отбросили при помощи MP...
Разве не стоит попробовать воспользовать леммами 6 $A\vdash(A\vee B) $ и 7 $B\vdash(A\vee B)$
Дальше я так понимаю надо действовать аналогично, но начинать с аксиомы 4
Спасибо вам большое за ваши советы.
Я вас не утомил еще?

[Maslov]

Padawan в сообщении #347439 писал(а):

Посылки нет, должны быть только аксиомы использованы.

Хорошо, пусть будет не "посылка", а "допущение".

chencho в сообщении #347444 писал(а):

Просто цифрами вы обозначаете номера лемм?

Ещё раз: я не понимаю, что Вы называете "леммами". "Просто цифрами" я обозначаю номера строк вывода:
1) $(A \to C) \land (B \to C)$ (допущение)
2) $((A \to C) \land (B \to C)) \to (A \to C)$ (аксиома 3)
3) $A \to C$ (1, 2, MP)[из строки 1 и строки 2 по правилу modus ponens выводим $A \to C$]

chencho в сообщении #347444 писал(а):

Как здесь используются лемма 1 $D\to D$ и лемма о дедукции?
...
Аналогично как здесь используются Леммы 3 и 4 ? $(A\wedge B)\vdash A $ $(A\wedge B)\vdash B $

Никак не используются. Вы думаете, что если в условии написано "использовать аксиомы", то надо обязательно использовать все аксиомы?

Не знаю, как ещё Вам объяснить. Единственный выход -- пойти на нарушение правил и выложить полное решение :

$(1)~ (A \to C) \land (B \to C)$ (допущение)
$(2)~ ((A \to C) \land (B \to C)) \to (A \to C)$ (A3)
$(3)~ A \to C$ (1, 2, MP)
$(4)~ (A \to C) \to ((B \to C) \to (A \lor B \to C)$ (A8)
$(5)~ (B \to C) \to (A \lor B \to C)$ (3, 4, MP)
$(6)~ ((A \to C) \land (B \to C)) \to (B \to C)$ (A4)
$(7)~ B \to C$ (1, 6, MP)
$(8)~ A \lor B \to C$ (5, 7, MP)
An - n-я аксиома из Верещагина и Шеня
Просто цифры - номера строк вывода
MP - modus ponens

[Padawan]

Maslov
Вы доказали, что $ (A \to C) \land (B \to C)\vdash A \lor B \to C$, а требуется $\vdash ((A \to C)\wedge(B \to C)) \to ((A\vee B) \to C)$. Можно сослаться, конечно, на теорему о дедукции, но непосредственного вывода не предоставлено.

[Maslov]

Padawan в сообщении #347508 писал(а):

непосредственного вывода не предоставлено

Padawan, согласен. Извините, что не понял Вас с первого раза.

[chencho]

спасибо.
В Верещагине Шене есть аксиомы, а есть леммы.
В аксиомах стрелочки в леммах знак "выводится".