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

[KondorB]

Нужно построить вывод в исчислении высказываний

$\vdash ((A \vee B) \wedge C) \leftrightarrow \lnot ((A \rightarrow \lnot C) \wedge (B \rightarrow \lnot C))$

Можно пользоваться аксиомами (Гильбертовская аксиоматика), Modus Popens и теоремой о дедукции.

Пока что я понимаю только что надо расписать двойную импликацию на две с конъюнкцией и выводить отдельно, а потом свести по аксиоме. Как эти отдельные выводы строить ума не приложу.

[arseniiv]

А что было выведено до этого, что можно было бы использовать? Доступны ли теорема о дедукции и вывод из гипотез?

-- Вт дек 17, 2013 00:51:10 --

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

[KondorB]

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

А что было выведено до этого, что можно было бы использовать? Доступны ли теорема о дедукции и вывод из гипотез?

-- Вт дек 17, 2013 00:51:10 --

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

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

[arseniiv]

Если увидеть там де Моргана с дистрибутивностью, придётся увидеть и двойное отрицание. И выражение импликации через дизъюнкцию. Возможно, разбитие на именно такие части приводит к выводу длиннее, чем какая-то другая идея — не знаю.

Итак, если вам такое нравится, можете приступать к $((A\vee B)\wedge C)\vdash((A\wedge C)\vee(B\wedge C))$ (или найти, если всё-таки было; а в обратную сторону нужно будет потооом). А что дальше — вдруг сами догадаетесь!

(Если хочется другого, то я пас. Других идей у меня не было. Подождите тогда кого-нибудь. Да и сам уже собираюсь уходить до завтра.)