Построение вывода в аксиоматической теории

[AliceUchiha]

$$\overline{Y\rightarrow{(X \rightarrow Z)}}\vdash\overline{X \rightarrow{(Y \rightarrow Z)}} $$

Помогите разобраться, как вывести данную формулу? Вводит в ступор отрицание. Думаю, быть может по "Сл.3" нарастить двойное отрицание: $\overline{\overline{X\rightarrow{(Y \rightarrow Z)}}}\vdash\overline{\overline{Y \rightarrow{(X \rightarrow Z)}}} $, далее по "Т5" снять отрицание: $\overline{Y\rightarrow{(X \rightarrow Z)}}\rightarrow {Y\rightarrow{(X \rightarrow Z)}$ и привести к "А3". Но я не уверен, что рассуждаю правильно.
Список всех доступных аксиом, теорем, следствий и т.д.

[Pphantom]

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

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

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

[Pphantom]

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

[george66]

Используйте "правило перевёртывания" (и пустое $\Gamma$). Аксиоматика убийственная, где такую взяли?

-- 30.05.2018, 00:48 --

Думаю над правилом T4. Однако. Что это за книга?

[AliceUchiha]

местные вузовские пособия, по теории Чёрча. Так я его и использую получается двойное отрицание или оно и в обратную сторону тоже действует?
Забыл добавить еще пару правил:

[george66]

Вам надо доказать секвенцию вида $\neg B\vdash\neg A$
По "правилу перевёртывания" для этого достаточно доказать $A\vdash B$, вот его и докажите. Двойного отрицания не надо.
Прочитайте лучше начало главы "Исчисление высказываний" из моего учебника (можно читать независимо от предыдущей части)
https://github.com/George66/Textbook/bl ... 8F%209.pdf

[AliceUchiha]

Посмотрите пожалуйста, правильно ли я ее вывел теперь:
1.$\vdash X\rightarrow{(Y\rightarrow{Z})}\rightarrow{((X\rightarrow{Y})\rightarrow(X\rightarrow{Z}))}$(A3)
2.$X\rightarrow{(Y\rightarrow{Z})}\vdash ((X\rightarrow{Y})\rightarrow(X\rightarrow{Z}))$ (T.o.d. k 1)
3.$\vdash (X\rightarrow{Y})\rightarrow(X\rightarrow{Z}) $(MP k 1,2)
4.$(X\rightarrow{Y}) \vdash (X\rightarrow{Z}) $(T.o.d. k 3)
5.$\vdash X\rightarrow{Y}$ (CB. 8 k 3,4)
6.$\vdash Y$ (T2 k 5)
7.$Y\vdash (X\rightarrow{Z})$ (CB.7 k 5,6)
8.$\vdash Y\rightarrow{(X\rightarrow{Z})} $(T.o.d. k 7)
9.$ X\rightarrow{(Y\rightarrow{Z})} \vdash Y\rightarrow{ (X\rightarrow{Z})} $(CB.2 k 2,8)
10.$\overline{ X\rightarrow{(Y\rightarrow{Z})}} \vdash \overline{Y\rightarrow{ (X\rightarrow{Z})}} $ (СЛ. 3 к 9)

[george66]

Вы читаете правила справа налево, а надо слева направо. Теорема о дедукции позволяет из $A\vdash B$ получить $\vdash A\to B$
Из второй строчки Вашего вывода можно получить первую, используя теорему о дедукции. А из первой вторую нельзя. (Также в первой строчке замените A3 на A2)

-- 30.05.2018, 04:09 --

И в последней поменяйте местами левую и правую часть.

[AliceUchiha]

Допустим я поменяю местами 1. и 2., Далее 1. же можно будет оперировать, ввиду того, что по Т.о.д. она является А2? И еще, как можно избавиться от $ A\to B$ в 3.? чтобы осталось только $\vdash A\rightarrow{C}$

[george66]

Правила делаются только слева направо. "Если $A$, то $B$" означает: если мы уже доказали $A$, мы можем считать доказанным $B$. Чтобы использовать теорему о дедукции, надо доказать $A\vdash B$, только тогда мы можем считать доказанным $\vdash A\to B$
Я не могу просто выписать вывод, потому что здесь это запрещено (просто решать чужие задачи). Но общее правило такое: если хотите из $A$ вывести $B$ (например, из $X\to(Y\to Z)$ вывести $Y\to(X\to Z)$), начните с секвенции $A\vdash A$
Аксиоматика крайне неудобная. Очень советую почитать начало главы "Исчисление высказываний", там описано, как доказывать удобно. Поймёте принцип.

[AliceUchiha]

А так:
1.$ Z\vdash Z$ (Cв.3)
2.$\vdash Y\to Z$(Т2 к 1)
3.$\vdash X\to Z$(Т2 к 1)
4.$\vdash X\to {(Y\to Z)}$ (T2 k 2)
5.$\vdash Y\to {(X\to Z)}$(T2 k 3)
6.$X\to{(Y\to Z)}\vdash Y\to {(X\to Z)}$(Св.2)

[george66]

Начните вывод с секвенций

$X\to(Y\to Z)\vdash X\to(Y\to Z)$

$X\vdash X$

$Y\vdash Y$

Из них получите секвенцию

$X\to(Y\to Z),Y,X\vdash Z$

с помощью свойств 1 и 8. Если не сможете, я больше ничего не скажу:)

[AliceUchiha]

Кажется я вывел, но остался вопрос, как из $X\to(Y\to Z)\vdash X\to(Y\to Z)$ мы получаем $X\vdash X$ и $Y\vdash Y$ или это получается отдельные гипотезы? и можно ли их использовать в дальнейшем как А,В,С и т.д.
И чуть не забыл, спасибо вам за помощь в понимании и решении поставленной задачи.

[george66]

Это три аксиомы или теоремы (свойство 3), их можно использовать в дальнейшем как $A,B,C$. По этой книге не учитесь, почитайте лучше самого Чёрча (или меня).

[AliceUchiha]

разобрался, еще раз спасибо