Контрапозиция в ИС

[Sinoid]

Здравствуйте! Пытаюсь решить в задачнике Лаврова Максимовой такую задачу:
Доказать, что следующие правила являются допустимыми в ИС:
д)$\dfrac{\Gamma,\, A\vdash B}{\Gamma,\,\neg B\vdash\neg A}$.
В указании сказано, что надо воспользоваться аксиомой $\neg B\vdash\neg B$ и правилами 9, 10, 14. Правило 9: $\dfrac{\Gamma,\, A\vdash}{\Gamma\vdash\neg A}$, правило 10: $\dfrac{\Gamma_{1}\vdash A;\,\Gamma_{2}\vdash\neg A}{\Gamma_{1},\,\Gamma_{2}\vdash}$ и правило 14: $\dfrac{\Gamma_{1},\, A,\, B,\,\Gamma_{2}\vdash C}{\Gamma_{1},\, B,\, A,\,\Gamma_{2}\vdash C}$. Хорошо, начинаю построение:
1. $\Gamma,\, A\vdash B$ (по условию);
2. $\neg B\vdash\neg B$ (аксиома);
3. $\Gamma,\, A,\,\neg B\vdash$ (10).
Но ведь, строго говоря, из этого, в силу 14 не следует $\Gamma,\,\neg B,\, A\vdash$ ? Правильно?

[arseniiv]

Следует. $\Gamma,\Gamma_1,\Gamma_2$ могут быть пустыми.

[Sinoid]

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

Следует. $\Gamma,\Gamma_1,\Gamma_2$ могут быть пустыми.

Дык, это-то я и сам знаю и дело совсем не в этом. В правиле 14 после знака $\vdash$ есть формула. В пункте же 3 моего построения после этого знака нет ничего.

[arseniiv]

Ой, простите. Тут я вообще не пойму, почему не сделали в этом правиле справа произвольную последовательность формул. Там есть ещё правила с перестановкой?

-- Сб апр 29, 2017 17:13:34 --

(Оффтоп)

Вообще, по моему нескромному мнению, все эти игры в упорядоченную последовательность не очень полезны, потому что когда формализация доходит до компьютера, довольно удобно работать и с неупорядоченными наборами формул. Математическое описание работы с ними не сильно сложнее описания работы с конечными последовательностями и в некоторой литературе используются именно неупорядоченные наборы.

Могу предложить разве что сверить набор аксиом исчисления секвенций с каким-то ещё источником. Видимо, это опечатка или недосмотр.

[Sinoid]

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

Там есть ещё правила с перестановкой?

Нет.

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

Могу предложить разве что сверить набор аксиом исчисления секвенций с каким-то ещё источником

С каким? Например, у Верещагина, Шена вообще несколько аксиом вместо одной. Надо точно восстановить имевшийся ими ввиду список правил вывода (чтобы внятно прорешать задачи). Вы не могли бы помочь это сделать? А то опять найду какую-нибудь ерунду. Вот список правил вывода:
1. $\dfrac{\Gamma_{1}\vdash A;\,\Gamma_{2}\vdash B}{\Gamma_{1},\,\Gamma_{2}\vdash(A\wedge B)}$
2. $\dfrac{\Gamma\vdash(A\wedge B)}{\Gamma\vdash A}$

(Оффтоп)

если нужно, я все формулы наберу в ТеХ

Где, по-вашему, здесь содержатся еще опечатки?

(Оффтоп)

Я не пойму, а в природе вообще существует внятный задачник по логике?

[arseniiv]

Странно как-то. Обычно sequent calculus предполагает, что справа может быть любое количество формул, а не только ноль или одна. Тут какой-то гибрид между натуральной дедукцией (ровно одна формула справа) и этим. В таких асимметричных правилах вывода теряется сама цель, с которой исчисление было задумано. В принципе, это можно считать изложением натуральной дедукции, где противоречивая формула обозначается пустой строкой вместо отдельного знака вроде $\bot$ (для путаницы?).

Вы можете, например, взять список из статьи англ. Википедии https://en.wikipedia.org/wiki/Sequent_calculus#Inference_rules. Для натуральной дедукции в таком исполнении (явные контексты, упорядоченные наборы формул и отсутствие переменных для доказательств) там, насколько копалса, нормального списка нет, а у вас, видимо, всё-таки она.

(Оффтоп)

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

Я не пойму, а в природе вообще существует внятный задачник по логике?

Не в курсе.

-- Вс апр 30, 2017 00:07:22 --

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

Где, по-вашему, здесь содержатся еще опечатки?

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

-- Вс апр 30, 2017 00:08:23 --

На всякий случай: теперь ясно, что это не опечатка, потому что произвольные последовательности формул справа здесь вообще не фигурируют.