Доказательство основной выводимости.

[Overt]

Доброго времени суток!

Необходимо доказать основную выводимость:
$V_7$ A $\vee$ B $\vdash$ B $\vee$ А

Для доказательства пользуюсь системой аксиом:
$\alpha$ 1. А $\supset$ ( B $\supset$ А)
$\alpha$ 2. (А $\supset$ B) $\supset$ ((A $\supset$ (B $\supset$ C)) $\supset$ (A $\supset$ C))
$\alpha$ 3. А $\wedge$ B $\supset$ A
$\alpha$ 4. А $\wedge$ B $\supset$ B
$\alpha$ 5. А $\supset$ (B $\supset$ A $\wedge$ B)
$\alpha$ 6. А $\supset$ A $\vee$ B
$\alpha$ 7. B $\supset$ A $\vee$ B
$\alpha$ 8. (А $\supset$ C) $\supset$ (( B $\supset$ C) $\supset$ (A $\vee$ B $\supset$ C))
$\alpha$ 9. (А $\supset$ B) $\supset$ (( A $\supset$ $\lnot$ B) $\supset$ $\lnot$ A )
$\alpha$10. $\lnot \lnot$А $\supset$ A

Док-во:
$B_1=$ А $\vee$ В
$B_2=$ B $\supset$ A $\vee$ B
$B_3=$ A $\supset$ B $\vee$ A
могу ли я воспользоваться ранее доказанной основной выводимостью V_3 A $\land$ B $\vdash$ А
для использования MP?
т.е. можно ли далее писать так:
$B_4=$ A $\land$ B $\vdash$ А - $V_3$
$B_5=$ A
$B_6=$ B $\vee$ A - MP, $B_3$

и еще вопрос, по правилу:
1. Правило подстановки.
Пусть U – формула, содержащая высказывательную переменную A. Тогда если U – истинная формула в исчислении высказываний, то, заменяя в ней переменную A всюду, куда она входит, произвольной формулой B, мы также получим истинную формулу.
Чем я имею право заменять переменную А всюду?

Спасибо за внимание.

[Maslov]

Overt в сообщении #399462 писал(а):

Док-во:
$B_1=$ А $\vee$ В
$B_2=$ B $\supset$ A $\vee$ B
$B_3=$ A $\supset$ B $\vee$ A
могу ли я воспользоваться ранее доказанной основной выводимостью $V_3$ A $\land$ B $\vdash$ А
для использования MP?
т.е. можно ли далее писать так:
$B_4=$ A $\land$ B $\vdash$ А - $V_3$
$B_5=$ A
$B_6=$ B $\vee$ A - MP, $B_3$

А строку $B_5$ Вы как получили?
Единственное правило вывода, которое у нас есть, -- это MP, поэтому для того чтобы воспользоваться выводимостью $V_3$, надо сначала из $A \lor B$ вывести $A \land B$, что невозможно.

Здесь всё проще. На аксиому $\alpha.8$ посмотрите внимательно:
$\alpha.8~ (A \supset C) \supset (( B \supset C) \supset (A \vee B \supset C))$
Так и хочется вместо $C$ подставить ...

Overt в сообщении #399462 писал(а):

Пусть U – формула, содержащая высказывательную переменную A. Тогда если U – истинная формула в исчислении высказываний

В исчислении высказываний нет понятия истинности, а есть понятие выводимости (доказуемости). Выводимые (доказуемые) формулы называются теоремами.
А истинность -- это из области интерпретации (алгебры высказываний).

Overt в сообщении #399462 писал(а):

Чем я имею право заменять переменную А всюду?

В теореме имеете право заменить пропозициональную переменную на произвольную формулу.

[Overt]

Спасибо за ответ, Максим.
Попробую продолжить.

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

Здесь всё проще. На аксиому $\alpha 8$ посмотрите внимательно: Так и хочется вместо подставить ...

$\alpha 8$. (A $\supset$ C) $\supset$ ((B $\supset$ C) $\supset$ (A $\lor$ B $\supset$ C))
$B_4$= (A $\supset$ B $\lor$ A) $\supset$ ((B $\supset$ B $\lor$ A) $\supset$ (A $\lor$ B $\supset$ B $\lor$ A)); вмсесто C подставляю B $\lor$ A
$B_5$= ((B $\supset$ B $\lor$ A) $\supset$ (A $\lor$ B $\supset$ B $\lor$ A)); $B_4$ MP $B_3$
$B_6$= A $\supset$ A $\lor$ B; $\alpha 6$.
$B_7$= B $\supset$ B $\lor$ A; Замена А на В, В на А.
$B_8$= (A $\lor$ B $\supset$ B $\lor$ A)); $B_5$ MP $B_7$
$B_9$= B $\lor$ A; $B_8$ MP $B_1$

То есть, вместо пропозициональной переменной имею право поставить совершенно любую верную формулу, да же которой у меня не было до начала доказательства, но в результат должен получить посредством МР. Я правильно понял?
У меня возникала такая идея доказательства, просто записать
$B_1$= А $\lor$ В; и произвести А на В, В на А.
$B_1$= B $\lor$ A; сразу же приходим к нужному виду.
и все, вроде бы, соответствует:
"Доказательством или выводом формулы F из множества Г называется конечная последовательность $B_1$, $B_2$, ..., $B_S$ каждая формула которой является либо аксиомой, либо формулой из Г, либо получена из двух предыдущих формулой этой последовательности по правилу МР, а последняя формула В совпадает с F."

[Maslov]

Overt в сообщении #399681 писал(а):

То есть, вместо пропозициональной переменной имею право поставить совершенно любую верную формулу, да же которой у меня не было до начала доказательства, но в результат должен получить посредством МР. Я правильно понял?

Правило подстановки формулируется следующим образом:
если выводима секвенция
$A_1, ..., A_n \vdash B$,
то выводима и секвенция
$A_1(P_1/C_1, ..., P_k/C_k), ..., A_n(P_1/C_1, ..., P_k/C_k) \vdash B(P_1/C_1, ..., P_k/C_k)$,
где $P_i$ -- пропозициональные переменные, $C_i$ -- произвольные формулы.

Overt в сообщении #399681 писал(а):

У меня возникала такая идея доказательства, просто записать
$B_1$= А $\lor$ В; и произвести А на В, В на А.
$B_1$= B $\lor$ A; сразу же приходим к нужному виду.

Формула $A \lor B$ не является выводимой из аксиом, поэтому после подстановки $A/B, B/A$ Вы получите просто еще одну формулу, а не последовательность формул, являющуюся выводом (доказательством).

Напротив, доказав выводимость
$A \lor B \vdash B \lor A$,
мы можем затем подставить вместо $A$ и $B$ произвольные формулы (не обязательно выводимые), и в результате получим выводимую секвенцию.

[Overt]

Спасибо за ответ.
Извиняюсь что долго не отвечал.
С вопросом разобрался, на экзамене заработал ХОР.
Еще раз спасибо!