Задача по логике высказываний

[coper]

Дано
$\mathrm{Tr} (A \to B) & & (B \to A)$
$\mathrm{Tr} (B \to C) $
$\mathrm{Tr} (C \to D) $
$\mathrm{Tr} (\overline{A} \to D) $

$?\mathrm{Tr} D $ ?
Мое решение
1. $\mathrm{Tr} (B \to C) $ , $\mathrm{Tr} (C \to D) $, влечет $\mathrm{Tr} (B \to D) $ (cир)
2. $\mathrm{Tr} (A \to B) & & (B \to A)$, влечет $\mathrm{Tr} (A \to B) $ (3а)
3. из 1,2 следует $\mathrm{Tr} (A \to D) $
4. получаем, что
$ \left\{ \begin{array}{l} \mathrm{Tr} (A \to D)\\ \mathrm{Tr} (\overline{A} \to D) \end{array} \right. $
5. Вот теперь казалось бы все очевидно, но не могу понять как строго показать что $\mathrm{Tr} D $.
6.Получилось вывести $\mathrm{Tr} (\overline{D} \to D) и с-но $\mathrm{Tr} (D\cup D)
Но вот чтото я не припомню аксиомы которая дает из этого ответ:(

[Xaositect]

У вас сильно нестандартные обозначения, но вроде бы это что-то типа натурального вывода.
А значит, из $D\vee D$ можно вывести $D$с помощью удаления дизъюнкции. Не было чего-то, что позволяет от $A\to C$, $B\to C$, $A\vee B$ перейти к $C$?

[coper]

http://ru.wikipedia.org/wiki/%D0%9B%D0% ... 0%B8%D0%B9
В середине 11 аксиом + Modus Pones.
Это все.

[Xaositect]

Ну так восьмая же.
С заменой $A$,$B$ и $C$ на $D$

[coper]

Xaositect в сообщении #381567 писал(а):

Ну так восьмая же.
С заменой $A$,$B$ и $C$ на $D$

!! спасибо!! что-то я тупил сидел.

[coper]

Нет стоп, тогда нужно еще условие Tr$D \to D$

[Xaositect]

А его не было? Сиилогизм же Вы используете, я думал, $A\to A$ Вам тоже доказали

[coper]

Можно еще раз мысль?

[Maslov]

$A \to A$ доказывается из аксиом 1 и 2:
Сначала подставляем $A \to A$ вместо $B$ и $A$ вместо $C$
Затем в первую аксиому подставляем $A$ вместо $B$.

А что означает $\mathrm{Tr}$?

[coper]

Все ясно, спс!
TR это значок Выводимости; У нас обозначается как |- , но я не нашел такой здесь. Использовал TR(Theorem).

[Maslov]

(Оффтоп)

Синтаксическая выводимость: $\vdash$

$\vdash$

Семантическая выводимость: $\models$

$\models$