д-во с помощью теоремы о дедукции

[tgg]

помогите, пожалуйста, доказать с помощью теоремы о дедукции:
(A->B) <-> (||AVB) где || это отрицание
это расписывается как
[(A->B) -> (||AVB)] & [(||AVB) ->(A->B)] ?, формулы с импликацией могу доказывать, а с остальными связками никак не разберусь.

[Toucan]

Чтобы тема не уехала в Карантин, оформите формулы в соответствии с требованиями Правил форума: topic8355.html , topic183.html

И выпишите используемую систему аксиом исчисления высказываний.

[maxmatem]

запишите так $\[(A \to B) \leftrightarrow (\bar A \vee B)\]$

[Maslov]

Аксиомы все равно нужны.

[maxmatem]

наверняка аксиомы стандартные....

[Maslov]

maxmatem в сообщении #301951 писал(а):

наверняка аксиомы стандартные....

Есть "стандартные" Мендельсона, есть "стандартные" Клини, есть "стандартные" Гильберта, есть еще другие "стандартные". Какие конкретно?

Пусть автор хоть немного пошевелится (заодно и TeX освоит).

[maxmatem]

стандартные Гильберта!

-- Ср мар 24, 2010 21:48:04 --

стандартные Гильберта!(ну я надеюсь, что автор имел их ввиду, но он кажется уснул )

[tgg]

стандартные аксиомы по Мендельсону

[Maslov]

Определения связок $\lor$ и $\leftrightarrow$ напишите, пожалуйста.

(Оффтоп)

maxmatem, это не Вам вопрос

[tgg]

$\vee $ - дизъюнкция,
$\leftrightarrow $ в этом примере заменяется на конъюнкцию & (так преподаватель сказал):
$\[(A\to B)\leftrightarrow(\bar A\vee B)\]$
то есть надо доказать что следующая формула выводима:
$\[(A\to B)\rightarrow(\bar A\vee B)\]$ & $\[(\bar A\vee B)\rightarrow(A\to B)\]$

[Maslov]

Еще раз: напишите, пожалуйста, в тему все аксиомы и определения связок $\lor$, $\land$ и $\leftrightarrow$ (у Мендельсона в аксиомах определены только связки $\to$ и $\lnot$, остальные вводятся вспомогательными определениями. Вот эти определения и напишите)
И скобки расставьте в формуле, которую надо доказать.

[tgg]

$\[[(A \to B)\rightarrow (\bar A\vee B)]\]$ & $\[[(\bar A\vee B)\rightarrow (A\to B)]\]$
аксиомы по мендельсону
A&B $\rightarrow A $
A&B $\rightarrow B $
$\[A \rightarrow (B \rightarrow($A&B))
$\[A \rightarrow (A \vee B))$
$\[B \rightarrow (A \vee B))$
$\[(A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow ((A \vee B) \rightarrow C))$

[Maslov]

Не, это не Мендельсон. У Мендельсона всего три схемы аксиом. Больше всего это похоже на краткое изложение (6 из 13) аксиом, используемых Клини.
Как Вы собираетесь с их помощью доказывать свою формулу, если отрицание в них вообще ни разу не встречается?
Подумайте еще.

А амперсанд в TeX набирается так: $\&$

 $\&$ 

[tgg]

есть еще несколько: (все из мендельсона аксиоматизации)
$\[(A \rightarrow B) \rightarrow ((A\rightarrow \bar B) \rightarrow \bar A)$
$\[\bar\bar A \rightarrow A$
$\[(A\rightarrow B) \rightarrow (\bar (B\&C)\rightarrow \bar (C\&A))$ по теории L2.
у него просто обозначения другие
не получается доказать потому что нет аксиомы со связками $\vee$ и отрицания одновременно

спасибо за $\&$

[Maslov]

tgg, в книге Мендельсона приведены несколько систем аксиом исчисления высказываний, а Вы их смешали в одну кучу.

Насколько я понимаю, речь идет все-таки о системе, используемой Клини:
$A1 : A \supset (B \supset A)$
$A2 : (A \supset B) \supset ((A \supset (B \supset C)) \supset (A \supset C))$
$A3 : (A \land B) \supset A$
$A4 : (A \land B) \supset B$
$A5 : A \supset (B \supset (A \land B))$
$A6 : A \supset (A \lor B)$
$A7 : B \supset (A \lor B)$
$A8 : (A \supset C) \supset ((B \supset C) \supset ((A \lor B) \supset C))$
$A9 : (A \supset B) \supset ((A \supset \overline{B} ) \supset \overline{A})$
$A10 : \overline{\overline{A}} \supset A $
$A11 : (A\equiv B) \supset (A \supset B)$
$A12 : (A\equiv B) \supset (B \supset A)$
$A13 : (A \supset B) \supset ((B \supset A) \supset (A\equiv B))$

Итак, Вам надо доказать следующую выводимость:

$ \vdash ((A \to B) \to (\bar A \lor B)) \land ((\bar A \lor B)\to (A\to B))$

Для этого можно отдельно доказать выводимость формул
$ \vdash (A \to B) \to (\bar A \lor B)$ и $ \vdash (\bar A \lor B) \to (A \to B)$
(или, пользуясь теоремой о дедукции,
$ A \to B \vdash \bar A \lor B$ и $ \bar A \lor B \vdash A \to B$),
а потом воспользоваться аксиомой $A5$.

Ну а теперь почитайте вот эту тему: topic28135.html