Доказать теорему в теории L4

[YgolovnicK]

Доброго времени суток. Помогите, пожалуйста, доказать следующую теорему в теории $L_4$:

$\vdash _L_4 \neg B \rightarrow (B \rightarrow C)$

Собственно, с решением совсем глухо, ибо формализованного четкого подхода к решениям такого типа задач нет, а опыт - пара с грехом пополам доказанных теорем в теории $L$. Для $L_4$ имею перед собой только набор аксиом, попытки применить их ни к чему хорошему не привели, по этой причине и обращаюсь к более сведущим с просьбой о помощи.

[Sonic86]

YgolovnicK в сообщении #737068 писал(а):

в теории $L_4$

А что это за теория? Или эквивалентный вопрос: какие у нее аксиомы?

[YgolovnicK]

Теория $L_4$:
Примитивными связками служат $\rightarrow , \& , \vee, \neg $
Набор аксиом:
1)$ A \rightarrow (B \rightarrow A)$
2) $ (A \rightarrow (B \rightarrow C )) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$
3) $A \& B \rightarrow A$
4) $A \& B \rightarrow B$
5) $A \rightarrow (B \rightarrow (A \& B))$
6) $A \rightarrow (A \vee B)$
7) $B \rightarrow (A \vee B) $
8) $(A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow ((A \vee B) \rightarrow C))$
9) $(A \rightarrow B) \rightarrow (( A \rightarrow \neg B) \rightarrow \neg A)$
10) $\neg \neg A \rightarrow A$

$A \equiv B$ означает $(A \rightarrow B) \& (B \rightarrow A)$

[Sonic86]

(Если не ошибаюсь, то $L_4$ - исчисление высказываний с системой аксиом Гильберта.)

Теоремой дедукции пользоваться можно?

[YgolovnicK]

На счет того, что такое $L_4,$ ничего конкретного сказать не могу, не в курсе.
Полагаю, что теорема дедукции работает и здесь, т.к. для доказательства её работы в теории $L$ потребовались лишь первые 2 аксиомы, которые идентичны первым двум в теории $L_4$

[Sonic86]

YgolovnicK в сообщении #737090 писал(а):

Полагаю, что теорема дедукции работает и здесь, т.к. для доказательства её работы в теории $L$ потребовались лишь первые 2 аксиомы, которые идентичны первым двум в теории $L_4$

Значит пользуемся. Тогда так: Примените к искомой формуле теорему дедукции - получите вывод, который Вам надо найти. Теперь подсказка: достаточно пользоваться аксиомами 1,2,9. И еще подсказка: Вам надо вывести из одного утверждения совершенно другое. Посмотрите, какие аксиомы позволяют новое утверждение, хотя и в связи старым, а какие аксиомы позволяют эту разорвать связь одного утверждения с другим?

[YgolovnicK]

Вот меня как то смущает тот факт, что получается 2 гипотезы, $B, \neg B$, которые противоречивы. Или не надо так брать? взять только $\neg B$? До того, как увидел Ваш пост, получилось нечто такое:
1) $\neg B$ гипотеза
2) $B$ гипотеза
3) $B \rightarrow (B \vee C)$ 6 аксиома
4) 2 к 3 MP $B \vee C$
5) $B \vee C$ есть то же самое, что и $( \neg A) \rightarrow C$
6) 1 к 5 MP, $C$
Получили $C$. 2 раза теорему дедукции к $ \neg B, B \vdash C$, получаем искомое $\vdash \neg B \rightarrow (B \rightarrow C)$

[Sonic86]

YgolovnicK в сообщении #737193 писал(а):

Вот меня как то смущает тот факт, что получается 2 гипотезы, $B, \neg B$, которые противоречивы. Или не надо так брать? взять только $\neg B$?

Все правильно! Т.е. мы должны доказать, $B,\neg B\vdash C$, т.е., что из противоречивых гипотез следует, что угодно. Из одной гипотезы такого мы, естественно, не получим.

YgolovnicK в сообщении #737193 писал(а):

До того, как увидел Ваш пост, получилось нечто такое:
1) $\neg B$ гипотеза
2) $B$ гипотеза
3) $B \rightarrow (B \vee C)$ 6 аксиома
4) 2 к 3 MP $B \vee C$
5) $B \vee C$ есть то же самое, что и $( \neg A) \rightarrow C$

Ага, я тоже сначала так начал Это обычная ошибка - вносить в ИВ факты или инструменты из АВ. Дело в том, что мы не знаем того, что

YgolovnicK в сообщении #737193 писал(а):

5) $B \vee C$ есть то же самое, что и $( \neg A) \rightarrow C$

В аксиомах это не прописано. А доказать просто это не получается - у меня получилось, что требуется для этого сначала доказать $\vdash B\to(\neg B \to C)$ Сразу также скажу, что заменять одну подформулу на ей эквивалентную в ИВ тоже нельзя - нет соответствующих правил. Т.е. в ИВ технически сложнее работать, чем в АВ: у нас есть только схемы аксиом и MP и больше ничего.
Все-таки, попробуйте воспользоваться только 1,2 и 8.

[YgolovnicK]

Пока не придумал, как использовать только 1,2,9 (полагаю, в последнем сообщении у Вас, Sonic86, опечатка).
Рассуждения привели меня к следующему:
1)$\neg B$ гипотеза
2)$B$ гипотеза
3) $B \rightarrow ( \neg C \rightarrow B)$ 1 аксиома
4) 2 к 3 MP, $\neg C \rightarrow B$
5)$(\neg C \rightarrow B) \rightarrow (( \neg C \rightarrow \neg B) \rightarrow \neg \neg C)$ 9 аксиома
6) 4 к 5 MP, $( \neg C \rightarrow \neg B) \rightarrow \neg \neg C$
7) $\neg B \rightarrow (\neg C \rightarrow \neg B)$, 1 аксиома
8) 1 к 7 MP, $ \neg C \rightarrow \neg B$
9) 8 к 6 MP, $\neg \neg C$
10) $\neg \neg C \rightarrow C$ 10 аксиома
11) 9 к 10 MP, $C$

[Sonic86]

Ну вот, поздравляю, мучения были не напрасны

YgolovnicK в сообщении #737228 писал(а):

Пока не придумал, как использовать только 1,2,9 (полагаю, в последнем сообщении у Вас, Sonic86, опечатка).

Да, опечатка

[YgolovnicK]

т.е. мои суждения верны, и вывод построен верно?

[Sonic86]

YgolovnicK в сообщении #737232 писал(а):

т.е. мои суждения верны, и вывод построен верно?

Да. Еще надо указать, что пользовались теоремой дедукции (самой теоремой, или обратной к ней - я не помню)

[YgolovnicK]

Ура!
Благодарю за помощь