Построить вывод в ИВ

[AloneIn]

Затрудняюсь в построении вывода, прошу подсказать\показать с чего и как начать, и указать мне примерный ход построения(что нужно получить и для чего).
Вывод : $A \supset B \vdash \neg A \vee B$ (эта формула является ТИФ, значит вывод существует).
Аксиомы ИВ(система Клини).

[Профессор Снэйп]

Конкретный вывод тут вроде довольно муторный.

Я знаю лишь следующий способ. Сначала доказать, что $\Gamma, \Phi \vdash \Psi \Leftrightarrow \Gamma, \neg\Psi \vdash \neg\Phi$ для любых формул $\Phi$, $\Psi$ и любой последовательности формул $\Gamma$. Затем, пользуясь этим, доказать, что $A \rightarrow B, \neg(\neg A \vee B) \vdash A$, $A \rightarrow B, \neg(\neg A \vee B) \vdash \neg A$ и по теореме о дедукции свести всё к девятой аксиоме. Квазивывод получается довольно несложный, но когда всё начинаешь разворачивать в конкретный вывод... Или Вам разрешено пользоваться теоремой о дедукции и прочими правилами квазивывода, не расписывая их в линейный вывод вплоть до аксиом?

[AloneIn]

Можно по теореме о дедукции(основной+вспомогательный вывод) а потом сократить.

[Профессор Снэйп]

AloneIn в сообщении #269977 писал(а):

Можно по теореме о дедукции(основной+вспомогательный вывод) а потом сократить.

Ну тогда всё, что надо, я Вам указал. Дело за малым

[AloneIn]

У меня была идея :
вывести
5) $B$
затем :
10) $B \supset \neg A \vee B$ , акс.7 , $A \rightarrow \neg A$
и тогда можно бы было :
11) $\neg A \vee B$ , m.p 5) и 10).

не могу получить $B$

Это был бы верный способ вывода ?

[Профессор Снэйп]

AloneIn в сообщении #270001 писал(а):

Это был бы верный способ вывода ?

НЕТ. Из $A \rightarrow B$ не выводимо $B$.

[AloneIn]

Я что-то не смог приспособить $A\rightarrow B, \neg(\neg A \vee B) \vdash A$ и $A\rightarrow B, \neg(\neg A \vee B) \vdash \neg A$
Подскажите чем это поможет ,а желательно - как)

[Профессор Снэйп]

AloneIn в сообщении #270362 писал(а):

Я что-то не смог приспособить $A\rightarrow B, \neg(\neg A \vee B) \vdash A$ и $A\rightarrow B, \neg(\neg A \vee B) \vdash \neg A$
Подскажите чем это поможет ,а желательно - как)

Теорема о дедукции и девятая аксиома: $(A \rightarrow B) \rightarrow ((A \rightarrow \neg B) \rightarrow \neg A)$. Потом десятая: $\neg\neg A \rightarrow A$.

[AloneIn]

А потом наверное 6-тая аксиома?

[Профессор Снэйп]

Я уже забыл, в каком они там порядке нумеруются. Напишите решение, а мы проверим.

[AloneIn]

Решение никак не получается - одни догадки

[AloneIn]

Я пытаюсь решить "с конца"
нужно получить $\neg A \vee B$
по акс.6 $\neg A \supset \neg A \vee B$
значит нужно $\neg A$
по акс.9 $(A \supset B) \supset ((A \supset \neg B) \supset \neg A)$
значит нужно $(A \supset \neg B)$
по акс.2 $(A \supset B) \supset ((A \supset (B \supset \neg B)) \supset (A \supset \neg B)$
а дальше не могу

[Maslov]

Доказательство есть в Клини С. — Математическая логика (стр. 75, упр. 13.4).
Но там вывод строится не непосредственно из аксиом, а с использованием ранее полученных результатов.

[Профессор Снэйп]

Короче, напишу (форум, блин, отвлекает от работы, зараза такая).

1) У нас есть теорема о дедукции и мы можем ею пользоваться.

2) Доказываем, что для любого множества формул $G$ и любых формул $A$, $B$ справедливо $G \cup \{ A \} \vdash B \Rightarrow G \cup \{ \neg B \} \vdash \neg A$.

3) Доказываем, что $\neg\neg A \vdash A$ (вроде это ваще аксиома)

4) Доказываем, что $\{ A \rightarrow B, A \} \vdash \neg A \vee B$ и $\{ A \rightarrow B, \neg A \} \vdash \neg A \vee B$.

5) Из 4 с помощью 2 и 3 получаем $\{ A \rightarrow B, \neg(\neg A \vee B) \} \vdash A$ и $\{ A \rightarrow B, \neg(\neg A \vee B) \} \vdash \neg A$.

6) Из 5 с помощью 1 получаем $\{ A \rightarrow B \} \vdash \neg(\neg A \vee B) \rightarrow A$ и
$\{ A \rightarrow B \} \vdash \neg(\neg A \vee B) \rightarrow \neg A$.

7) Записываем аксиому $(\neg(\neg A \vee B) \rightarrow A) \rightarrow ((\neg(\neg A \vee B) \rightarrow \neg A) \rightarrow \neg\neg(\neg A \vee B))$.

8) Из 6 и 7 получаем $\{ A \rightarrow B \} \vdash \neg\neg(\neg A \vee B)$.

9) Из 8 и 3 получаем то, что нужно.

-- Вт дек 15, 2009 00:15:11 --

AloneIn в сообщении #271411 писал(а):

Я по акс.6 $\neg A \supset \neg A \vee B$
значит нужно $\neg A$
...
а дальше не могу

И немудрено. Из $A \rightarrow B$ не выводимо $\neg A$

[Maslov]

Ну а другое решение такое:
1. Доказываем $\vdash A \lor \neg A$
2. Доказываем, что для любого множества формул $G$ и любых формул $A, B, C$ справедливо $G, A \vdash C; G, B \vdash C \Rightarrow G, A \lor B \vdash C$
3. Доказываем $A \to B, A \vdash \neg A \lor B $
4. Доказываем $A \to B, \neg A \vdash \neg A \lor B $
5. Ну и из 2, 3, 4 и по теореме о дедукции: $\vdash (A \to B) \to ((A \lor \neg A) \to (\neg A \lor B))$

(Если что, это не я , это Клини придумал )