Как доказать выводимость формулы в Исчислении высказываний

[kola1357]

Подскажите, пожалуйста, как доказать выводимость формулы в ИВ в таком примере:
$\vdash (( A \to \bar B) \to (B \to \bar A))$
Я попробовал это выражение упростить, у меня получилось, что оно всегда верно, то есть $\vdash 1$
И вроде все доказано, можно ли так решать эту задачу ?
Пробовал применять аксиомы, их у нас 10 штук дано, а также правило вывода modus pones.
Но пример такой, не получается увидить в аксиомах.
Подскажите, пожалуйста, как решить его правильно.

Аксиомы такие у нас на лекции давали.

$$\begin{array}{l} A \to (B\to A), \\ (A \to (B \to C)) \to ((A \to B) \to (A \to C)), \\ A \wedge B \to A, \\ A \wedge B \to B, \\ A \to (B \to (A \wedge B)), \\ A \to A \vee B, \\ B \to A \vee B, \\ (A \to C) \to ((B \to C) \to (A \vee B \to C)), \\ (A \to B) \to ((A \to \neg B) \to \neg A), \\ \neg\neg A \to A. \end{array}$$

[kola1357]

Я тут по этому примеру обнаружил, что $A \to \bar B $ и $B \to \bar A$ это одно и тоже. Тогда пример можно переписать в таком виде $\vdash X \to X$. А этого доказать выводимость уже знаю как, а выводимость этого говорит, что и исходное выводится.

Вот если я так решу задачу, это будет правильно ? Можно так делать при выводе в исчислении высказываний ?

[Sonic86]

kola1357 в сообщении #730017 писал(а):

Подскажите, пожалуйста, как доказать выводимость формулы в ИВ в таком примере:
$\vdash (( A \to \bar B) \to (B \to \bar A))$
Я попробовал это выражение упростить, у меня получилось, что оно всегда верно, то есть $\vdash 1$
И вроде все доказано, можно ли так решать эту задачу ?

Нет, нельзя. В ИВ есть только схемы аксиом (у Вас их 9) и правило вывода modus ponens. Вы же здесь воспользовались логическими значениями, в ИВ их нет.
Вы, конечно, можете в голове пользоваться таблицами истинности из АВ и тем фактом, что множество истинных формул в АВ совпадает со множеством доказуемых формул в ИВ (хотя технически это непростой факт). Например, с помощью таблиц истинности можно в голове пытаться определять, является ли такая-то формула выводимой или нет. Но все эти рассуждения не будут выводом в ИВ.

(Оффтоп)

Здесь можно спросить, а зачем такие сложности в ИВ, если есть простой алгоритм в АВ а "суть" от этого не меняется. Есть разные ответы с разных точек зрения. Если Вам нужны эти ответы для мотивации - могу кое-что написать, но сам написать их без просто так мотивации не могу.

kola1357 в сообщении #730078 писал(а):

Я тут по этому примеру обнаружил, что $A \to \bar B $ и $B \to \bar A$ это одно и тоже.

Правильно говорить, что эти формулы эквивалентны в ИВ.

kola1357 в сообщении #730078 писал(а):

Тогда пример можно переписать в таком виде $\vdash X \to X$. А этого доказать выводимость уже знаю как, а выводимость этого говорит, что и исходное выводится.

Вот если я так решу задачу, это будет правильно ? Можно так делать при выводе в исчислении высказываний ?

Опять же - нельзя, по вышеупомянутой причине.

Вообще, Вам можно пользоваться теоремой дедукции или нет? Если да - сразу пытайтесь использовать ее. Если нет, то скажите - будем думать.

[kola1357]

Sonic86, теоремой дедукции пользоваться можно, она была на лекции. С этим примером разобрался.
А вы не подскажите как быть вот в таком примере: $\vdash (A \bigvee A) \to A$
У меня идея использовать 8 аксиому.

[Sonic86]

kola1357 в сообщении #730110 писал(а):

Sonic86, теоремой дедукции пользоваться можно, она была на лекции.

Значит пользуйтесь, она сильно упрощает дело.

kola1357 в сообщении #730110 писал(а):

А вы не подскажите как быть вот в таком примере: $\vdash (A \bigvee A) \to A$
У меня идея использовать 8 аксиому.

Да, именно так. Пробуйте. Если не получается полностью, напишите, что получается, а что - нет.