Перестановка посылок

[Sinoid]

Здравствуйте! Проверьте, пожалуйста, решение задачи. Пусть запись $(A\equiv B)$ обозначает $((A\supset B)\wedge(B\supset A))$. Хочу доказать, что $((A\supset(B\supset C))\equiv(B\supset(A\supset C)))$.
Доказательство. Пусть теорема дедукции уже доказана. $(A\supset(B\supset C))$ тогда и только тогда, когда ${A}\vdash(B\supset C)$, которая тогда и только тогда, когда ${A},{B}\vdash C$, которая тогда и только тогда, когда ${B},{A}\vdash C$, которая тогда и только тогда, когда ${B}\vdash(A\supset C)$, которая тогда и только тогда, когда $(B\supset(A\supset C))$. Итак, я доказал, что с помощью теоремы о дедукции можно доказать, что $(A\supset(B\supset C))\vdash(B\supset(A\supset C))$. Но по той же теореме о дедукции это означает, что $((A\supset(B\supset C))\supset(B\supset(A\supset C)))$. Т.к. в приведенном выше доказательстве использовалось "тогда и только тогда", то рассуждение обратимо, и, значит, выводимо $((B\supset(A\supset C))\supset(A\supset(B\supset C)))$. А тогда, в силу аксиомы $((P\supset Q)\supset((P\supset R)\supset(P\supset(Q\wedge R))))$ выводимо и $(((A\supset(B\supset C))\supset(B\supset(A\supset C))) \wedge ((B\supset(A\supset C))\supset(A\supset(B\supset C))))$. Что вы думаете по поводу такого доказательства?

[arseniiv]

Хорошее доказательство, если ещё до этого ввести на основании теоремы о дедукции и указанной аксиомы производное правило вывода $\dfrac{A,\quad B}{A\wedge B}$. Тогда всё будет примерно на одном уровне абстракции, как-то приятнее будет смотреться.

Sinoid в сообщении #1197661 писал(а):

Т.к. в приведенном выше доказательстве использовалось "тогда и только тогда", то рассуждение обратимо, и, значит, выводимо $((B\supset(A\supset C))\supset(A\supset(B\supset C)))$.

Кстати, можно добиться того же, не используя обратимость, просто сделав замену $[A/B, B/A]$ (одновременно) и использовав теорему $(\Gamma\vdash A)\Rightarrow(\Gamma[\ldots]\vdash A[\ldots])$, где $[\ldots]$ — корректная для любой формулы из $\Gamma\cup\{A\}$ замена.

-- Пн мар 06, 2017 19:49:20 --

(В логике высказываний все замены корректны.)

[Sinoid]

arseniiv в сообщении #1197665 писал(а):

если ещё до этого ввести на основании теоремы о дедукции и указанной аксиомы производное правило вывода $\dfrac{A,\quad B}{A\wedge B}$.

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

arseniiv в сообщении #1197665 писал(а):

Кстати, можно добиться того же, не используя обратимость, просто сделав замену $[A/B, B/A]$ (одновременно) и использовав теорему $(\Gamma\vdash A)\Rightarrow(\Gamma[\ldots]\vdash A[\ldots])$, где $[\ldots]$ — корректная для любой формулы из $\Gamma\cup\{A\}$ замена.

я это свойство еще не доказал.

-- 06.03.2017, 19:53 --

Так это получается, вывод формул не всегда состоит из последовательных записей аксиом и выводов из них. Скажите, пожалуйста, вот запись $\neg A$ означает выводимость этой формулы и невыводимость формулы $A$?