Построение вывода в ИВ

[dimaudi]

надо построить такой вывод $\supset(A\supset B)\supset(\overline{A\wedge \overline B)}$
в Исчислении высказываний, используя аксиомы Клини и такую подсказку A\wedge \overline B\supset A$, $A\subset B$ по транзитивности $A\wedge \overline B \supset B$ и $A\wedge\overline B\supset \overline B$
в формуле вначале стоит знак вывода а не \supset
Помогите построить хотябы вспомогательный вывод, кстати известно что он будет из 11 формул...

[gefest_md]

$\vdash$ - читать "выводится"

Цитата:

Историческая справка: Россер предложил использовать $``\vdash для выражения выводимости посредством правил вывода, а Клини - включать также выводимость из предложений, принятых за аксиомы.

\vdash

dimaudi писал(а):

Помогите построить хотя бы вспомогательный вывод...

$$ \begin{enumerate} \item 1.\ $A\,\&\,\neg\,B\to A\qquad\mbox{--- схема аксиом 4a}$ \item 2.\ $A\to B\qquad\mbox{--- допущение}$ \item 3.\ $(A\,\&\,\neg\,B\to A)\to((A\to B)\to(A\,\&\,\neg\,B\to B))\qquad\mbox{--- Ваша подсказка}$ \item 4.\ $(A\to B)\to(A\,\&\,\neg\,B\to B)\qquad\mbox{--- правило 2, 1, 3}$ \item 5.\ $A\,\&\,\neg\,B\to B\qquad\mbox{--- правило 2, 2, 4}$ \item 6.\ $(A\,\&\,\neg\,B\to B)\to((A\,\&\,\neg\,B\to \neg\,B)\to\neg\,(A\,\&\,\neg\,B))\qquad\mbox{--- схема аксиом 7}$ \item 7.\ $A\,\&\,\neg\,B\to\neg\,B\qquad\mbox{--- схема аксиом 4b}$ \item 8.\ $(A\,\&\,\neg\,B\to \neg\,B)\to\neg\,(A\,\&\,\neg\,B)\qquad\mbox{--- правило 2, 5, 6}$ \item 9.\ $\neg\,(A\,\&\,\neg\,B)\qquad\mbox{--- правило 2, 7, 8}$ \end{enumerate} $$

Последняя, девятая формула выводится из остальных восьми. Но согласно свойствам $\vdash$ (Теорема 9, Клини), и учитывая что $\vdash(A\to B)\to((B\to C)\to(A\to C))$, можно писать только $A\to B\vdash\neg\,(A\,\&\,\neg\,B).$

[dimaudi]

gefest_md спасибо огромное...