Доказать истинность заключения

[tupoidodik]

Необходимо доказать истинность заключения, построив дерево доказательства.

$$( \neg A \vee \neg B) \vdash ( \neg B \to A) \vee (A \to C)$$

Аксиома: $A \vdash A$
Правила вывода:

1. $\frac{\Gamma \vdash A \quad \Gamma \vdash B}{\Gamma \vdash A \wedge B}$

2. $\frac{\Gamma \vdash A \wedge B}{\Gamma \vdash A}$

3. $\tfrac{\Gamma \vdash A \wedge B}{\Gamma \vdash B}$

4. $\frac{\Gamma \vdash A}{\Gamma \vdash A \vee B}$

5. $\frac{\Gamma \vdash B}{\Gamma \vdash A \vee B}$

6. $\frac{\Gamma \vdash A \vee B \quad \Gamma, A \vdash C, \quad \Gamma, B \vdash C}{\Gamma \vdash C}$

7. $\frac{\Gamma, A \vdash B}{\Gamma \vdash A \to B}$

8. $\frac{\Gamma \vdash A \quad \Gamma \vdash A \to B}{\Gamma \vdash B}$

9. $\frac{\Gamma, \neg A \vdash}{\Gamma \vdash A}$

10. $\frac{\Gamma \vdash A \quad \Gamma \vdash \neg A}{\Gamma \vdash}$

11. $\frac{\Gamma \vdash B}{\Gamma, A \vdash B}$

Второй день уже бьюсь над заданием, не получается. Что делаю я (иду от корня к аксиоме):

1.1. Применяю правило 4 (думал использовать 5, но там С в скобках, не думаю, что она влиять будет). Получаем: $( \neg A \vee\neg B) \vdash ( \neg B \to A)$
1.2. Использую правило 7, больше я идей не вижу. Получаем: $( \neg A \vee\neg B), \neg B \vdash A$
1.3. Сначала подумал о правиле 8, но тогда у нас будет ветка с $(\neg B \to A)$, а мы от нее только избавились. Потом подумал ввести дизъюнкцию (6), но там в двух ветках у меня тупик. Остановился на правиле (9). Получаем: $( \neg A \vee\neg B), \neg B, \neg A \vdash$
1.4 Дальше только один вариант, это 10. Но тут стоит подумать, что выбрать для заключения. Сначала думал выбрать А/неА или B/неВ, но дальше в одной из веток я не знаю, что делать. Я выбрал $( \neg A \vee \neg B)$, получил две ветки:

• $( \neg A \vee \neg B), \neg B, \neg A \vdash ( \neg A \vee \neg B)$
• $( \neg A \vee \neg B), \neg B, \neg A \vdash \neg ( \neg A \vee \neg B)$

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

Я предполагаю, что ошибка в первом пункте, но там кроме удаления дизъюнкции я даже не знаю, что можно применить. Да еще и "С" там что-то делает, хотя в посылках ее вообще нет, а в интернете аналогичные задания не могу найти. Буду рад любой помощи.

[Pphantom]

Тема перемещена из форума «Помогите решить / разобраться (М)» в форум «Карантин»
по следующим причинам:

- неправильно набраны формулы (краткие инструкции: «Краткий FAQ по тегу [math]» и видеоролик Как записывать формулы).

Исправьте все Ваши ошибки и сообщите об этом в теме Сообщение в карантине исправлено.
Настоятельно рекомендуется ознакомиться с темами Что такое карантин и что нужно делать, чтобы там оказаться и Правила научного форума.

[Pphantom]

Тема перемещена из форума «Карантин» в форум «Помогите решить / разобраться (М)»

[arseniiv]

tupoidodik в сообщении #1267274 писал(а):

1.1. Применяю правило 4 (думал использовать 5, но там С в скобках, не думаю, что она влиять будет). Получаем: $( \neg A \vee\neg B) \vdash ( \neg B \to A)$

Это плохой шаг, потому что $\neg A\vee\neg B \not\vDash \neg B\to A$ (при $(A,B) = (0,0)$ левая имеет значение 1, а правая — 0), так что привести эту секвенцию к аксиомам не получится.

-- Вт ноя 21, 2017 00:32:27 --

Кстати, в правиле 9 что понимается под правой частью $\Gamma\vdash$? Подозрительно.

-- Вт ноя 21, 2017 00:33:52 --

А, ну, в принципе, понял. Можно понимать это как особый тип секвенций, вводимый правилом 10.

-- Вт ноя 21, 2017 00:45:48 --

В общем, можно дать такой совет: с «обратного применения» правил 4 и 5 начинать не нужно. Это даёт тупик. Есть вот правила 6 или 8, которые здесь тоже можно использовать — только придётся угадывать, что взять за $A, B$ в 6 и $A$ в 8.

tupoidodik в сообщении #1267274 писал(а):

Да еще и "С" там что-то делает, хотя в посылках ее вообще нет

Она позволяет более хитрым образом сказать $\neg A$.