д-во с помощью теоремы о дедукции

[tgg]

Спасибо!

[tgg]

У меня еще один пример, тоже дедукцией:
$\[A\rightarrow (B\rightarrow C)$; $\[\bar D \vee A$;$\[B \vdash D\rightarrow C$
по теореме о дедукции:
$\[A\rightarrow (B\rightarrow C)$; $\[\bar D \vee A$;$\[B$; $\[D$ $\[\vdash C$
1. $\[A\rightarrow (B\rightarrow C) \rightarrow ((A\rightarrow B)\rightarrow(A\rightarrow C))$ по аксиоме 2
2.$\[A\rightarrow (B\rightarrow C)$ гипотеза
3. $\[((A\rightarrow B)\rightarrow(A\rightarrow C))$ по МР
4. $\[B$ гипотеза
5. из 4 и 5 можно сказать, что $\[A\rightarrow C$ ?

как можно вывести А?

[Maslov]

Да тут проще:
$\overline D \lor A, D \vdash A$ с помощью эквивалентности из первого поста этой темы
Ну а дальше все вроде очевидно.

[tgg]

также выводила из эквивалентности, но препод сказал не использовать вообще эквивалентность почему-то.
Без этого не получится?

[Maslov]

Да получиться-то должно по-всякому, только я опять не понимаю, каким набором аксиом Вы пользуетесь: в том наборе, который я писал, аксиома 2 -- это
$(A \to B) \to ((A \to (B \to C)) \to (A \to C)$
а не
$(A \to (B \to C)) \to ((A \to B) \to (A \to C))$

[tgg]

просто в Мендельсоне так написано, в Клини вроде как вы написали, я взяла то что мне подходит :)

[Maslov]

Лихо Вы.
В Мендельсоне всего 3 аксиомы, а связка $A \lor B$ по определению вводится как $\overline A \to B$, поэтому и доказывать почти ничего не надо.
Преподаватель-то на какую систему аксиом рассчитывает?

[tgg]

он писал аксиомы такие как вы написали. А вообще допустимо применять в доказательствах эквивалентные формулы? Ведь все остальные связки можно выражать через отрицание и импликацию. Я не понимаю, почему эта аксиома в разных источниках по разному формулируется, еще в интернете видела что пишут по разному. В обеих случаях тождественна истинна все равно

[Maslov]

Тут ведь дело такое: пользоваться можно всем, что является аксиомами или из них выведено.
Поэтому если Вы исходите из системы аксиом Мендельсона (3 аксиомы + связки $\lor, \land, \sim$, введенные по определению), то все свойства этих связок (которые у Клини яляются аксиомами) надо доказывать. И наоборот. Ну а доказавши, пользуйтесь сколько угодно.

Ну это лирика. Останавливаемся на аксиомах Клини.
А чем еще можно пользоваться, кроме теоремы о дедукции? Правилами псевдовывода можно?
Таким, например: если $A \vdash C, B \vdash C$, то $A \lor B \vdash C$?

[tgg]

да, вспомогательные правила вывода

[Maslov]

Ну тогда $(\overline D \lor A) \to (D \to A)$ можно в пару шагов вывести:

I. Выводим правило $ \neg A \vdash A \to B$:
1. $A, \neg A, \neg B \vdash A$
2. $A, \neg A, \neg B \vdash \neg A$
3. $A, \neg A \vdash \neg \neg B$ (по вспом. правилу "док-во от противного")
4. $\neg \neg B \vdash B$ (A10)
5. $A, \neg A \vdash B$ (3, 4)
6. $\neg A \vdash A \to B$ (5, теорема о дедукции)

II. Выводим $\overline D \lor A \vdash D \to A$:
1. $A \vdash D \to A$ (A1, теорема о дедукции)
2. $\neg D \vdash D \to A$ (правило I)
3. $\neg D \lor A \vdash D \to A$ (вспом. правил "исключение дизъюнкции")

[tgg]

и просто в условии вместо дизъюнкции вставить то что вывела? А как объяснить откуда взялось
$\[D\rightarrow A$? Я точно так же делала, в первой задаче тоже такое же надо было доказать.
Получается применяется эквивалентность с доказательством?

[Maslov]

Я бы просто взял и начал с этого Ваш вывод для $C$:
1. $~A \vdash D \to A$ (A1, теорема о дедукции)
$ 2. ~\neg D \vdash D \to A$ (правило I)
$ 3. ~\neg D \lor A \vdash D \to A$ (вспом. правил "исключение дизъюнкции")
$ 4. ~\neg D \lor A $ (гипотеза)
$ 5. ~D \to A $ (3, 4, MP)
$ 6. ~D$ (гипотеза)
$ 7. ~A$ (5, 6, MP)
$ 8. ~A \to (B \to C)$ (гипотеза)
$ 9. ~B \to C$ (7, 8, MP)
и т.д.

Или объясните подробнее, что Вам нужно.

[tgg]

просто не знала что можно использовать $\[A$ и $\[\bar D$ в 1 и 2 действии, они не даны как гипотезы.

[Maslov]

Ну и что из того, что не даны. Аксиомы тоже не даны как гипотезы, Вы же их используете.