Матлогика - доказывание теорем - гипотезы и теорема дедукции

[davidgale]

Никак нимогу понять - если дана теорема и нужно eё доказать то что можно взять за гипотезы? Какие правила существует? Например $\[\vdash (A \to B) \to ((B \to C) \to (A \to C))\]$. Можно ли взять A или B по отдельности? Или только тогда, когда как гипотез принят$\[(A \to B)$? Можно ли взять $\[((B \to C) \to (A \to C))\]$ или $\[(B \to C)\]$ или $\[(A \to C)\]$ как гипотезы?
Также проблема с пониманием теоремы дедукции. Мне кто-то обяснял что суть заключается в том что если мы принили за гипотезу A и потом получили B и в начальней формуле $\[(A \to B)\]$ то можем принять $\[(A \to B)\]$ доказанным. Это так? Небыло бы плохо увидеть доказательство какой небудь теоремы с использованием ТД.

[davidgale]

кто нибудь? завтра контрольная...

[arseniiv]

Вот теорема о дедукции и покажет вам, как можно доказательство формулы преобразить в доказательство какой-то формулы попроще из гипотез. Например, вывод $\vdash (A \to B) \to ((B \to C) \to (A \to C))$ эквивалентен выводу $A\to B\vdash(B\to C)\to(A\to C)$, а этот вывод эквивалентен выводу $A\to B,B\to C\vdash A\to C$.

davidgale в сообщении #802903 писал(а):

Также проблема с пониманием теоремы дедукции. Мне кто-то обяснял что суть заключается в том что если мы принили за гипотезу A и потом получили B и в начальней формуле $(A \to B)$ то можем принять $(A \to B)$ доказанным. Это так?

Не совсем ясно, понимаете ли вы написанное как нужно, так что я напишу точнее: теорема дедукции утверждает, что $\mathcal A\vdash\mathcal B$ эквивалентно $\vdash \mathcal A\to\mathcal B$ для любых формул $\mathcal A, \mathcal B$. Если $\mathcal B$ выводится из $\mathcal A$ — значит, выводится $\mathcal A\to\mathcal B$, и в обратную сторону. (Ну и если какой-то выводимости нет, то и второй тоже нет. Например, не существует вывода $C$ из $\neg C$ — значит, вывести формулу $\neg C\to C$ тоже нельзя.)

P. S. Внутри формул не нужно писать \[...\], достаточно одних долларов.

[davidgale]

теперь насчёт гипотез кто нибудь подскажет...
также хочу спросить есть ли программа которая может доказать простые теоремы?

[davidgale]

Есть формула:
$(F \wedge G) \vee H \to (F \vee H) \wedge (G \vee H)$

Разделаем на две (по L8):
a) $(F \wedge G) \to (F \vee H) \wedge (G \vee H)$
и
b) $H \to (F \vee H) \wedge (G \vee H)$

Работаем с a)
1) $F \vee H$ - гипотеза
2) $F \vee H$ \to F - L3
3) $F \vee H$ \to G - L4
4) $F - MP 1,2
5) $G - MP 1,3
6) $F \to (G \to (F \wedge G)$ - L5
7) $G \to F \wedge G$ - MP 4,6
8) $F \wedge G - MP 5,7

Теперь самое главное. Видим что получили первую часть формулы а). Вопрос следующий. Можно ли взять как гипотезу дополнительно всю а) и с помошю MP получить вторую часть формулы или я должен вывести вторую часть формулы а) тоже с помошю аксиом (L6, L7)?

-- 19.12.2013, 00:00 --

другая формула:
\vdash $(C \to D) \to ((\neg C \to D) \to D)$
1) $C$ - hip.
2) $D \to (C \to D)$ - L1
3) $(C \to D)$ MP 1,2
4) $D$ MP 1,3
Как достать $\neg C$? Можно взять как hip.?