Исчисление выссказываний, как избавляться от отрицания

[shkololo]

Здравствуй, дорогой форум! Помоги доказать выводимость в исчислении выссказываний этой формулы:

$((A\vee B)\wedge C) \leftrightarrow \neg ((A \rightarrow \neg C) \wedge (B \rightarrow \neg C))$

Слева-направо доказывается просто (сделал это самостоятельно). Справа-налево, наверное, тоже просто... Но я не могу понять, как в этом случае избавиться от отрицания в предпосылке? Заранее благодарен за помощь.

[xmaister]

$A\Rightarrow B\Leftrightarrow \neg A\vee B$

[Maslov]

Какая у Вас система аксиом исчисления высказываний?

[shkololo]

Maslov


Гильбертовские 11 аксиом (те, что перечислены на википедии)

[Maslov]

shkololo в сообщении #505591 писал(а):

Справа-налево, наверное, тоже просто... Но я не могу понять, как в этом случае избавиться от отрицания в предпосылке?

Можно в подобных случаях от противного доказывать.

Т. е. если надо доказать выводимость
$\vdash \neg\Phi_1 \to \Phi_2$,
то можно попытаться найти такую формулу $\Phi_3$, что
$\neg\Phi_1, \Phi_2 \vdash \Phi_3$
$\neg\Phi_1, \Phi_2 \vdash \neg\Phi_3$
ну а дальше по правилу введения $\neg$ получаем $\neg \Phi_1 \vdash \Phi_2$, и по теореме о дедукции, $\vdash \neg \Phi_1 \to \Phi_2$

Но в Вашем примере, по-моему, проще все-таки начать с
$\vdash \neg (A \land B) \to (\neg A \lor \neg B) $

[shkololo]

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

если надо доказать выводимость
$\vdash \neg\Phi_1 \to \Phi_2$,
то можно попытаться найти такую формулу $\Phi_3$, что
$\neg\Phi_1, \Phi_2 \vdash \Phi_3$
$\neg\Phi_1, \Phi_2 \vdash \neg\Phi_3$

ну а дальше по правилу введения $\neg$ получаем $\neg \Phi_1 \vdash \Phi_2$

Каким образом из этого:
$\neg\Phi_1, \Phi_2 \vdash \Phi_3$
$\neg\Phi_1, \Phi_2 \vdash \neg\Phi_3$

следует выводимость
$\neg \Phi_1 \vdash \Phi_2$?

По 10-ой аксиоме из этого следует
$\neg \Phi_1 \vdash \neg \Phi_2$. Или я неправ?

[Maslov]

shkololo в сообщении #505947 писал(а):

Или я неправ?

Конечно, правы :) Я отрицание потерял. Правильно так:

Т. е. если надо доказать выводимость
$\vdash \neg\Phi_1 \to \Phi_2$,
то можно попытаться найти такую формулу $\Phi_3$, что
$\neg\Phi_1, \neg \Phi_2 \vdash \Phi_3$
$\neg\Phi_1, \neg \Phi_2 \vdash \neg\Phi_3$
ну а дальше по правилу введения $\neg$ получаем $\neg \Phi_1 \vdash \neg \neg \Phi_2$, и по снятию двойного отрицания и теореме о дедукции, $\vdash \neg \Phi_1 \to \Phi_2$

[shkololo]

Хм, понял) Огромное спасибо, попробую сделать так.

[Maslov]

Почитайте Клини. Математическая логика. Там довольно много подобных штук доказывается.

Лучше, конечно, задачник Игошина, но у него другие аксиомы.