Еще одно правило вывода

[Sinoid]

Здравствуйте! Пытаюсь в ИВ обосновать такое правило вывода: $\begin{matrix}\Gamma,\, A\vdash B;\,\Gamma,\, A\vdash\neg B\\ \hline\Gamma\vdash\neg A \end{matrix}$. Вот что я думаю. У меня есть формула $((A\supset B)\equiv(\neg B\supset\neg A))$. Значит, я данное правило могу заменить таким: $\begin{matrix}\Gamma,\,\neg B\vdash\neg A;\,\Gamma,\, B\vdash\neg A\\ \hline \Gamma\vdash\neg A \end{matrix}$. Тогда, если выводимо $B$, то выводимо и $\neg A$. Если же $B$ невыводимо, то выводимо $\neg B$, а это означает выводимость $\neg A$. Скажите, пожалуйста, я правильно рассуждаю?

[arseniiv]

А вы уже доказали полноту исчисления высказываний? Если нет, проще пойти более прямым путём, взяв аксиому, определяющую отрицание.

-- Пн мар 06, 2017 23:36:14 --

Среди аксиом

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

интересующая должна быть 9.

[mihaild]

Теорема о дедукции уже есть? Если да, то сверху получаем $\Gamma \vdash A \rightarrow B, A \rightarrow \neg B$, и это уже почти всё.

[Sinoid]

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

А вы уже доказали полноту исчисления высказываний?

Нет.

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

Если нет, проще пойти более прямым путём, взяв аксиому, определяющую отрицание.

Так по существу-то я ее и использовал.

mihaild в сообщении #1197735 писал(а):

Теорема о дедукции уже есть? Если да, то сверху получаем $\Gamma \vdash A \rightarrow B, A \rightarrow \neg B$, и это уже почти всё.

Да, эта теорема уже есть. Я формулу $((A\supset B)\supset((A\supset\neg B)\supset\neg A))$ не могу вывести.

[arseniiv]

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

Так по существу-то я ее и использовал.

Ну, по существу сказать, что если не выполняется $\Delta\vdash A$, то выполняется $\Delta\vdash\neg A$ — это всё-таки полнота как она есть. Отсюда ещё спускаться до аксиомы.

[Sinoid]

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

Ну, по существу сказать, что если не выполняется $\Delta\vdash A$, то выполняется $\Delta\vdash\neg A$ — это всё-таки полнота как она есть. Отсюда ещё спускаться до аксиомы.

Полноты у меня еще нет, да я про нее и не думал. Так, хорошо, напишу по порядку. Пусть $\Gamma,\, A\vdash B$. Тогда, в силу теоремы о дедукции $\Gamma\vdash (A\supset B)$. Аксиому 9 я могу записать так: $((A\supset B)\supset(\neg B\supset\neg A))$. Эту формулку я в силу теоремы о дедукции могу представить так: $((A\supset B)\vdash(\neg B\supset\neg A))$, значит, $\Gamma\vdash(\neg B\supset\neg A)$, откуда по многострадальной теореме о дедукции $\Gamma,\,{\neg B}\vdash\neg A$. Так же и со второй посылкой. Это пока все мысли относительно аксиомы 9. Как рассуждать дальше ума не приложу.

[arseniiv]

Вот $\Gamma,\neg B\vdash\neg A$. С другой стороны, $\Gamma,A\vdash\neg B$. Так что $\Gamma,A\vdash\neg A$. Правда, я почему-то забыл, как убрать из посылок $A$.

[Sinoid]

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

Так что $\Gamma,A\vdash\neg A$. Правда, я почему-то забыл, как убрать из посылок $A$.

Мне до этого казался бы это путь в никуда и я бы по нему не пошел, но раз вы сказали... Честно говоря, я удивлен таким поворотом дела. Интересно, а что дальше ?

[arseniiv]

Ну, я совершенно серьёзно написал, что не знаю, как убрать лишнюю посылку. Пусть mihaild лучше подтвердит или опровергнет, что это куда-то приведёт. Хотя попробовать это не мешает.

[mihaild]

А какие есть аксиомы? Приведенные arseniiv? $((A\supset B)\supset((A\supset\neg B)\supset\neg A))$ часто включается в аксиомы.
(скорее всего, важны те, которые включают только импликацию и отрицание - почти всегда аксиомы стараются записать так, чтобы конъюнкция и дизъюнкция сами по себе были не нужны)

[Sinoid]

mihaild в сообщении #1197896 писал(а):

А какие есть аксиомы? Приведенные arseniiv?

Да.

mihaild в сообщении #1197896 писал(а):

$((A\supset B)\supset((A\supset\neg B)\supset\neg A))$ часто включается в аксиомы.

Я же писал

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

Я формулу $((A\supset B)\supset((A\supset\neg B)\supset\neg A))$ не могу вывести.

так что это не аксиома.

[mihaild]

Так, нам надо $\vdash (A \to \neg A) \to \neg A$?
$A \vdash ((A \to \neg A) \to \neg A) \to (A \to \neg(A \to \neg A))$
$A \vdash (A \to \neg A) \to \neg A$ (тут опять нужна теорема о дедукции)
$A \vdash A \to \neg(A \to \neg A)$
$A \vdash \neg (A \to \neg A)$
$\vdash A \to \neg(A \to \neg A)$
$\vdash (A \to \neg(A \to \neg A)) \to ((A \to \neg A) \to \neg A)$
$\vdash (A \to \neg A) \to \neg A$

[Sinoid]

Вот спасибо-то большое за помощь.