Помогите доказать в исчислении высказываний

[dirkul]

Помогите доказать в исчислении высказываний (буквы обозначают произвольные формулы): $$A \lor (B \lor C) \to A \lor (B \lor (A \lor C))
Примерное решение такое.
1. $$A \lor (B \lor C) \to A \lor (B \lor (A \lor C)
2. Если В $\vdash$ А, то $C \lor B $ $\vdash$ $C \lor A $ следствие 4
3. $C \lor A $ $\vdash$ $A \lor C $ следствие 5
4. С $\vdash$ $A \lor C $
5. $A \lor (B \lor C) \to A \lor (B \lor C)$

6. $A \lor (B \lor C) \to A \lor (B \lor (A \lor C)$


Заранее спасибо.

Используется 3 схемы аксиом.
$A \to (B \to A)
$(A \to (B \to C)) \to ((A \to B) \to (A \to C))
$ (\overline {B} \to \overline{A}) \to ((\overline{B} \to A) \to B)

[Toucan]

Тема перемещена в Карантин.

Чтобы оттуда выбраться, запишите формулы в соответствии с требованиями Правил форума, т.е. в $\TeX$. Краткие инструкции можно найти здесь: topic8355.html и topic183.html.

В частности: $A \to B, A \lor B$ набирается так:

$A \to B, A \lor B$

Кроме этого, укажите, пожалуйста, какая система аксиом исчисления высказываний используется.

После того как исправите сообщение, сообщите об этом в теме Сообщение в карантине исправлено.

[Maslov]

dirkul в сообщении #371378 писал(а):

2. Если В $\vdash$ А, то $C \lor B $ $\vdash$ $C \lor A $ следствие 4

А о каких следствиях идёт речь?

[dirkul]

На лекциях давали 5 следствий:
1. Если В $\vdash$ А, то $C \lor B $ $\vdash$ $C \lor A $ следствие 4
2. $A \lor B $ $\vdash$ $B \lor A $
3. $A \to (A \lor B) $ и $B \to (A \lor B) $
4. A,B - гипотеза $\vdash$ А$\Lambda B$
5. (А$\Lambda B$)\to A и (А$\Lambda B$)\to B

[BapuK]

чтобы Вам помогли, Вам нужно написать систему аксиом, что вам давали, и все правила вывода, которые опять же Вам давали на лекциях

[dirkul]

На лекциях давали 3 схемы аксиомы, которые указаны в первом посте, следствия, указанные во 2 посте и еще 9 секвенций.
Подсказка была, что доказательство строится на следствии.

[Maslov]

Что-то мне Ваша логика не очень понятна.

Я бы начал с доказательства $\vdash (A \lor (B \lor C)) \to (B \lor (A \lor C))$

Например, по такой схеме:

$1.~ \vdash (A \lor (B \lor C)) \to ((A \lor B) \lor C)$
$2.~ \vdash ((A \lor B) \lor C) \to ((B \lor A) \lor C)$
$3.~ \vdash ((B \lor A) \lor C) \to (B \lor (A \lor C))$

При этом коммутативностью связки $\lor$ можно пользоваться (следствие 2), а вот ассоциативность придётся доказывать самостоятельно.

[dirkul]

Спасибо за подсказку.
А как дальше, когда я докажу , что $ \vdash ((B \lor A) \lor C) \to (B \lor (A \lor C))$
получить из $B \lor (A \lor C) \to A \lor (B \lor (A \lor C))$, откуда взять А?
Заранее спасибо.

[Maslov]

У Вас же есть следствие 3 (вторая часть).

[dirkul]

Как в следствие 3 ($B \to (A \lor B)$) поставить $B \lor (A \lor C))$ вместо $B$?
как мы пришли к тому, что В равно $B \lor (A \lor C))$ ?

[Maslov]

dirkul в сообщении #372696 писал(а):

Как в следствие 3 ($B \to (A \lor B)$) поставить $B \lor (A \lor C))$ вместо $B$?

Я имел в виду Ваше следствие 3: $B \to (A \lor B)$.
Если в него подставить $B \lor (A \lor C)$ вместо $B$, получим формулу, которую надо вывести.

[dirkul]

А как доказать, что B = $B \lor (A \lor C)$? Почему мы решили, что B = $B \lor (A \lor C)$

[Joker_vD]

dirkul
Странно видеть человека, не различающего свободных и связанных переменных.

$B \to (A \lor B)$, заменяем $B$ на $B \lor (A \lor C)$, получаем $B \lor (A \lor C) \to (A \lor B \lor (A \lor C))$.

[Maslov]

dirkul, что импликация $B \to (A \lor B)$ справедлива при подстановке вместо $A$ и $B$ любых формул. В том числе, при подстановке $A$ вместо $A$ и $B \lor (A \lor C)$ вместо $B$

[dirkul]

Максим, спасибо большое.