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

[StopCry]

Помогите построить вывод
$A \supset B \vdash \neg A \vee B$

вроде как то так делать надо:
$\neg A \supset \neg (A \vee B)$
потом контрапозиция...
$\neg(\neg A \vee B)\supset \neg \neg A $
$\neg \neg A \supset A$

потом хз что, но по моей логике что то примерно на подобии этого получится должно
$\neg(\neg A \supset B) \supset A$
$A \supset B$
а дальше я в полном ступоре...

[Maslov]

StopCry, какая система аксиом исчисления высказываний используется?
Какими производными правилами вывода можно пользоваться?

[StopCry]

Maslov
Система Клини.
Правило заключения, Правило контрапозиции.

[Maslov]

Можно действовать так:
1. Доказываем $A \vdash (A \supset B) \supset (\neg A \lor B)$
2. Доказываем $\neg A \vdash (A \supset B) \supset (\neg A \lor B)$
3. Объединяем их по правилу удаления $\lor$
4. Доказываем $\vdash A \lor \neg A$
5. Применяем modus ponens и обратную теорему о дедукции.

Посмотрите пример 13.4 на стр. 75 в "Клини. Математическая логика."

[StopCry]

Я вот так построил, проверьте пожалуйста на правильность
$A \supset B \vdash \neg A \lor B$
От противного
1)$\neg A \supset \neg A \lor B$ акс. 6 $A \rightarrow \neg A$
2)$\neg(\neg A \lor B) \supset \neg \neg A$ контрапозиция 1
3)$\neg \neg A \supset A$ акс. 10
4)$\neg(\neg A \lor B)\supset A$ объединение 2 и 3
5)$A \supset B$ посылка
6)$\neg (\neg A \lor B) \supset B$ объединение 4 и 5
7)$B \supset \neg A \lor B$ акс. 7 $A \rightarrow \neg A$
8)$\neg (\neg A \lor B) \supset \neg B$ контрапозиция 7
Получили противоречие 6 и 8

[StopCry]

Я нашел у себя ошибку...
между 1 и 2 шагами должно быть еще что-то, контрапозицию нельзя сразу записать.между 7 и 8 тоже самое.
А перед шагами 4 и 6 должно быть доказательство транзитивности наверное...

И еще один вопрос, можно ли раскрыть отрицание?

[Maslov]

StopCry в сообщении #662262 писал(а):

между 1 и 2 шагами должно быть еще что-то, контрапозицию нельзя сразу записать.

Можно записать так:
1) $~\vdash \neg A \supset \neg A \lor B $ аксиома ??
2) $~\vdash (\neg A \supset \neg A \lor B) \supset (\neg (\neg A \lor B) \supset \neg \neg A) $ правило контрапозиции
3) $~\vdash \neg (\neg A \lor B) \supset \neg \neg A $ 1, 2, modus penens

StopCry в сообщении #662262 писал(а):

А перед шагами 4 и 6 должно быть доказательство транзитивности наверное...

Да, выводимость $\vdash (A \supset B) \supset ((B \supset C) \supset (A \supset C))$ надо доказывать.

Но то, что Вы построили, выводом не является: в исчислении высказываний понятия "противоречие" нет, есть только понятие выводимости. Воспользуйтесь аксиомой $ \vdash (X \supset Y) \supset ((X \supset \neg Y) \supset \neg X)$ (не знаю, под каким она у Вас номером).

StopCry в сообщении #662262 писал(а):

И еще один вопрос, можно ли раскрыть отрицание?

Не понял вопроса.

[StopCry]

Maslov
ну я имею ввиду что
$-(-3 + 5) = 3 - 5$
а с отрицанием есть что то подобное?
наподобии:
$\neg(\neg A \lor B)$тоже самое, что и $A \lor \neg B$?

[Maslov]

$\vdash \neg (A \lor B) \sim (\neg A) \land (\neg B)$
Но это тоже надо доказывать.