2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




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

 
 
 
 Re: Построить вывод в ИВ
Сообщение10.12.2009, 19:11 
Аватара пользователя
Конкретный вывод тут вроде довольно муторный.

Я знаю лишь следующий способ. Сначала доказать, что $\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$ и по теореме о дедукции свести всё к девятой аксиоме. Квазивывод получается довольно несложный, но когда всё начинаешь разворачивать в конкретный вывод... Или Вам разрешено пользоваться теоремой о дедукции и прочими правилами квазивывода, не расписывая их в линейный вывод вплоть до аксиом?

 
 
 
 Re: Построить вывод в ИВ
Сообщение10.12.2009, 19:34 
Можно по теореме о дедукции(основной+вспомогательный вывод) а потом сократить.

 
 
 
 Re: Построить вывод в ИВ
Сообщение10.12.2009, 19:35 
Аватара пользователя
AloneIn в сообщении #269977 писал(а):
Можно по теореме о дедукции(основной+вспомогательный вывод) а потом сократить.

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

 
 
 
 Re: Построить вывод в ИВ
Сообщение10.12.2009, 20:06 
У меня была идея :
вывести
5) $B$
затем :
10) $B \supset \neg A \vee B$ , акс.7 , $A \rightarrow \neg A$
и тогда можно бы было :
11) $\neg A \vee B$ , m.p 5) и 10).

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

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

 
 
 
 Re: Построить вывод в ИВ
Сообщение10.12.2009, 20:17 
Аватара пользователя
AloneIn в сообщении #270001 писал(а):
Это был бы верный способ вывода ?

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

 
 
 
 Re: Построить вывод в ИВ
Сообщение11.12.2009, 19:31 
Я что-то не смог приспособить $A\rightarrow B, \neg(\neg A \vee B) \vdash A$ и $A\rightarrow B, \neg(\neg A \vee B) \vdash \neg A$
Подскажите чем это поможет ,а желательно - как)

 
 
 
 Re: Построить вывод в ИВ
Сообщение11.12.2009, 19:40 
Аватара пользователя
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$.

 
 
 
 Re: Построить вывод в ИВ
Сообщение11.12.2009, 19:49 
А потом наверное 6-тая аксиома?

 
 
 
 Re: Построить вывод в ИВ
Сообщение12.12.2009, 07:28 
Аватара пользователя
Я уже забыл, в каком они там порядке нумеруются. Напишите решение, а мы проверим.

 
 
 
 Re: Построить вывод в ИВ
Сообщение13.12.2009, 20:41 
Решение никак не получается - одни догадки :?

 
 
 
 Re: Построить вывод в ИВ
Сообщение14.12.2009, 18:31 
Я пытаюсь решить "с конца"
нужно получить $\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)$
а дальше не могу

 
 
 
 Re: Построить вывод в ИВ
Сообщение14.12.2009, 19:42 
Доказательство есть в Клини С. — Математическая логика (стр. 75, упр. 13.4).
Но там вывод строится не непосредственно из аксиом, а с использованием ранее полученных результатов.

 
 
 
 Re: Построить вывод в ИВ
Сообщение14.12.2009, 21:10 
Аватара пользователя
Короче, напишу (форум, блин, отвлекает от работы, зараза такая).

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$ :)

 
 
 
 Re: Построить вывод в ИВ
Сообщение14.12.2009, 23:47 
Ну а другое решение такое:
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))$

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

 
 
 [ Сообщений: 18 ]  На страницу 1, 2  След.


Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group