Незаконченное рассуждение Верещагина, Шеня

[Sinoid]

Замечаний нет. Поэтому рискну предположить, что рассуждение не содержит ошибок. Докажу что, наоборот, из $(\Gamma\wedge\neg A)\rightarrow\Delta$ выводимо $\Gamma\rightarrow(\Delta\vee A)$. Пусть $(\Gamma\wedge\neg A)\rightarrow\Delta$. Тогда $\Gamma\wedge(\neg A)\vdash_{H}\,\Delta$ (теорема о дедукции), а т.к. $\Gamma,\,\neg A\vdash_{H}\,(\Gamma\wedge(\neg A))$, то $\Gamma,\,\neg A\vdash_{H}\,\Delta$, откуда по теореме о дедукции $\Gamma\vdash_{H}\,(\neg A\rightarrow\Delta)$. Осталось показать, что $(\neg A\rightarrow\Delta)\vdash_{H}\,(A\vee\Delta)$, для чего достаточно из списка формул $\{(\neg A\rightarrow\Delta),\,\neg(A\vee\Delta)\}$ вывести какую-нибудь формулу и ее отрицание. В той книге перед этим было задание доказать, что $(P\rightarrow Q)\vdash_{H}(\neg Q\rightarrow\neg P)$. Вот я этой выводимостью и воспользуюсь. Имею $A\rightarrow(A\vee\Delta)$ и $\Delta \rightarrow (A\vee\Delta)$ (акс. 6 и 7). Откуда в силу упомянутой мной выводимости с последующей доработкой с помощью теоремы о дедукции $\neg(A\vee\Delta)\vdash_{H}\,\neg A$ и $\neg(A\vee\Delta)\vdash_{H}\,\neg\Delta$. В итоге получаем, что из списка формул $\{(\neg A\rightarrow\Delta),\,\neg(A\vee\Delta)\}$ выводима (в ИВ) формула $\Delta$ и ее отрицание. Есть какие-нибудь замечания?

[arseniiv]

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

Замечаний нет. Поэтому рискну предположить, что рассуждение не содержит ошибок.

Да, я решил, что нет смысла писать это.

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

Есть какие-нибудь замечания?

Нет.

[Sinoid]

Давайте пока доказательство про дизъюнкцию опустим. Меня интересует общее направление мысли. Это мне нужно на индукционном шаге доказать, что если из $g_{1},\, g_{2},\,\ldots\,,g_{m}\vdash_{G}\, d_{1},\, d_{2},\,\ldots\,,\, d_{n}$ будет следовать $g_{1}\wedge g_{2}\wedge\ldots g_{m}\vdash_{H}\, d_{1}\vee d_{2}\vee\ldots d_{n}$, то из $g,\, g_{1},\, g_{2},\,\ldots\,,g_{m}\vdash_{G}\, d_{1},\, d_{2},\,\ldots\,,\, d_{n}$ будет следовать $g\wedge g_{1}\wedge g_{2}\wedge\ldots g_{m}\vdash_{H}\, d_{1}\vee d_{2}\vee\ldots d_{n}$?

[arseniiv]

Не совсем. Вывод представляет собой дерево, и индукция по структуре вывода имеет вид

Пусть (база) утверждение $A(\sigma)$ верно для секвенции $\sigma$, являющейся аксиомой.
Пусть (переход) для каждого правила вывода $\dfrac{\sigma_1\quad\ldots\quad\sigma_n}{\sigma}$ если верны $A(\sigma_1),\ldots,A(\sigma_n)$, то $A(\sigma)$.
Тогда для каждой выводимой секвенции $\sigma$ верно $A(\sigma)$.

В данном случае $A(\sigma) = {}$ «представляющая $\sigma$ формула ИВ выводима (в ИВ)».

Скажем, кусок индукционного перехода для правила $\dfrac{\Gamma\vdash_G A,\Delta\quad \Gamma\vdash_G B,\Delta}{\Gamma\vdash_G A\wedge B,\Delta}$ выглядит как «если $\vdash_H (\wedge\Gamma)\to A\vee(\vee\Delta)$ и $\vdash_H (\wedge\Gamma)\to B\vee(\vee\Delta)$, то $\vdash_H (\wedge\Gamma)\to(A\wedge B)\vee(\vee\Delta)$».

Или для правила $\dfrac{A,B,\Gamma\vdash_G\Delta}{A\wedge B,\Gamma\vdash_G\Delta}$ это будет «если $\vdash_H A\wedge B\wedge(\wedge\Gamma)\to(\vee\Delta)$ [тут скобки вокруг конъюнкции можно ставить как угодно, т. к. мы показали нужное], то $\vdash_H (A\wedge B)\wedge(\wedge\Gamma)\to(\vee\Delta)$».

[Sinoid]

А база доказывается так: если $p,\, q_{1},\ldots,q_{m}\vdash_{G}p,\, r_{1},\ldots,\, r_{n}$ - аксиома ИС, то, по причинам, совершенно независимым от аксиоматики ИС, $p\wedge q_{1}\wedge\ldots\wedge q_{m}\vdash_{H}p$ и $p\vdash_{H}p\vee r_{1}\ldots \vee r_{n}$, откуда $p\wedge q_{1}\wedge\ldots\wedge q_{m}\vdash_{H}p\vee r_{1}\ldots \vee r_{n}$.

[Sinoid]

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

Пусть (переход) для каждого правила вывода $\dfrac{\sigma_1\quad\ldots\quad\sigma_n}{\sigma}$ если верны $A(\sigma_1),\ldots,A(\sigma_n)$, то $A(\sigma)$.

Я просто думал, в ИС, как и в ИВ, рассуждение допустимо только в одну сторону. С другой стороны, я не мог понять, почему в книге Верещагина, Шена и задачнике Лаврова, Максимовой изложение, казалось бы, одного и того же ИС происходит в противоположных направлениях, даже тему хотел начать по этому поводу. Но до меня дошло, что в ИС формулу можно как строить, так и разбирать по частям.

[arseniiv]

Ну, вообще нет. Если мы рассматриваем ИС именно как систему вывода, у нас правила вывода идут только в одну сторону, сверху вниз, как и в любых системах вывода (когда есть двунаправленные правила, их просто добавляют отдельно).

В обратную же сторону мы «применяем» правила, если получаем (заранее неизвестный) вывод нужной формулы, и механически доходим до аксиом и «не-аксиом» вида $v_1,\ldots,v_m\vdash_G v_{m+1},\ldots,v_n$, где все $v_i$ разные, и когда в ветвях одни аксиомы, мы знаем, что вывод есть, и мы его построили, а когда есть не-аксиомы, мы знаем, что вывода не существует.