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

[Sinoid]

Здравствуйте! Пытаюсь по заданию в книге Верещагина, Шена довести рассуждение до конца (по заданию авторов) Отрывок вот:


Не совсем пока ясно, к чему это приведет, так что, пожалуйста, проконтролируйте меня. Это получается, вначале нужно доказать выводимость формул $\Gamma,\,((A\wedge B)\wedge C)\vdash\Delta$ и $\Gamma,\,(A\wedge (B\wedge C))\vdash\Delta$ одновременно?

[arseniiv]

Не для формул в секвенциях, а для формул—переводов секвенций: то, что $\vdash (A\wedge B)\wedge C\to\Delta'$ и $\vdash A\wedge (B\wedge C)\to\Delta'$ одновременно ($\Delta'$ — перевод $\Delta$, но проще доказать, не думая о том, что это дизъюнкция чего-то или тождественно ложная формула, а считая её любой формулой). Хотя раз уж тут части секвенций являются множествами, неплохо было бы также показать и коммутативность. Вот $3!\times C_{3-1} = 12$ всевозможных результатов

$$\begin{array}{cc} (A\wedge B)\wedge C, & A\wedge(B\wedge C), \\ (A\wedge C)\wedge B, & A\wedge(C\wedge B), \\ \vdots & \vdots \\ (C\wedge B)\wedge A, & C\wedge(B\wedge A), \end{array}$$

которые мы можем получить, вычисляя конъюнкцию множества как конъюнкцию каких-то двух его подмножеств, образующих разбиение, и считая конъюнкцией одноэлементного множества сам элемент, для трёхэлементного множества $\{A,B,C\}$. Все их можно получить из любого, применяя ассоциативность и коммутативность, но не одну только ассоциативность.

[Sinoid]

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

$\vdash (A\wedge B)\wedge C\to\Delta'$ и $\vdash A\wedge (B\wedge C)\to\Delta'$ одновременно

Это построить из формулы $\vdash (A\wedge B)\wedge C\to\Delta'$ вывод формулы $\vdash A\wedge (B\wedge C)\to\Delta'$ в ИВ и обратно?

[arseniiv]

Ну да, можно ожидать построение одного вывода по другому. Можно, однако, построить выводы (из гипотез в ИВ) $\textit{первая}\vdash\textit{вторая}$ и $\textit{вторая}\vdash\textit{первая}$ (∗), тогда это получится проще, потому что вывод одной получится из вывода другой банальным приклеиванием к нему в начале соответствующего гипотетического вывода. Притом ясно видно, как должны выглядеть сами выводы (∗), они сводятся к $(A\wedge B)\wedge C\vdash A\wedge(B\wedge C)$ и наоборот.

Но не забудьте потом и про коммутативность.

-- Ср май 03, 2017 18:03:34 --

Кстати, предлагаю ниже в теме писать для спорных случаев вместо $\vdash$ для выводимости в ИВ $\vdash_H$ (Hilbert) и для выводимости в ИС $\vdash_G$ (Gentzen).

[Sinoid]

Так. Начинаю рассуждать. Сначала докажу, что $(P \rightarrow Q)\vdash_H((Q \rightarrow R)\rightarrow(P \rightarrow R))$ (1). Применяя несколько раз лемму о дедукции, получу, что для этого достаточно доказать, что $P,\,(P \rightarrow Q),\,(Q \rightarrow R) \vdash_{H}R$. Это утверждение очевидно, поэтому я на нем не буду останавливаться. Теперь мне нужно доказать, что, с учетом принятых обозначений,

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

$(A \wedge B) \wedge C \vdash_H A \wedge(B \wedge C)$ и наоборот.

Я буду ссылаться на аксиоматику ИВ, приведенную в задачнике Лавровой, Максимова. Итак,
1. $((A \wedge B) \wedge C)$ (по условию);
2.$(((A \wedge B) \wedge C) \rightarrow (A \wedge B))$ (акс. 3);
3. $(((A \wedge B) \wedge C) \rightarrow C)$ (акс. 4);
4. $(A \wedge B)$ (МР, п. 1, п. 2);
5. $C$ (МР, п. 1, п. 3);
6. $((A \wedge B) \rightarrow A)$ (акс. 3);
7. $((A \wedge B) \rightarrow B)$ акс. 4);
8. $A$ (МР, п. 4, п. 6);
9. $B$ (МР, п. 4, п. 7);
10. $(B \rightarrow (A \rightarrow B))$ (акс. 1);
11. $(C \rightarrow (A \rightarrow C))$ (акс. 1);
12. $(A \rightarrow B)$ (МР, п. 9, п. 10);
13 $(A \rightarrow C)$ (МР, п. 5, п. 11);
14. $((A \rightarrow B) \rightarrow ((A \rightarrow C) \rightarrow (A \rightarrow (B \wedge C))))$ (акс. 5);
15. $((A \rightarrow C) \rightarrow (A \rightarrow (B \wedge C)))$ (МР, п. 12, п. 14);
16. $(A \rightarrow (B \wedge C))$ (МР, п. 13, п. 15);
17. $(B \wedge C)$ (МР, п. 8, п. 16);
18. $A \rightarrow A$ (вывод есть во многих книгах);
19. $((B \wedge C) \rightarrow (A \rightarrow (B \wedge C)))$ (акс. 1);
20. $(A \rightarrow (B \wedge C))$ (МР, п. 17, п. 19);
21. $((A \rightarrow A) \rightarrow((A \rightarrow (B \wedge C)) \rightarrow (A \rightarrow (A \wedge (B \wedge C)))))$ (акс. 5).
Из последней формулы с учетом выведенных выше формул, являющихся частями последней формулы, я, применяя несколько раз МР, получу $(A \wedge (B \wedge C))$. Итак, я доказал, что $((A\wedge B)\wedge C)\vdash_H(A\wedge(B\wedge C))$. В силу леммы о индукции это означает, что $\vdash_H(((A\wedge B)\wedge C)\rightarrow(A\wedge(B\wedge C)))$. В силу же (1) $(((A\wedge B)\wedge C)\rightarrow(A\wedge(B\wedge C)))\vdash_H(((A\wedge(B\wedge C))\rightarrow\Delta')\rightarrow(((A\wedge B)\wedge C)\rightarrow\Delta'))$, откуда, учитывая последнюю формулу, получаю, что $\vdash_H(((A\wedge(B\wedge C))\rightarrow\Delta')\rightarrow(((A\wedge B)\wedge C)\rightarrow\Delta'))$. Верно? Только не совсем ясно, почему

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

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

? Ведь я $\Delta'$ приклеивал не в начале, а в окончании полученных ранее утверждений о выводимости. Теперь про коммутативность. Мне кажется, начинать нужно с вывода $(B\wedge A)\vdash_H(A\wedge B)$ и дальше применить формулу (1). Верно?

[arseniiv]

А, та моя цитата немного о другом. Вот вы фактически получили $(A\wedge B)\wedge C\to\Delta' \vdash_H A\wedge (B\wedge C)\to\Delta'$. Я говорил о том, что теперь если у нас есть вывод $\vdash_H (A\wedge B)\wedge C\to\Delta'$, мы показываем $\vdash_H A\wedge (B\wedge C)\to\Delta'$, приклеивая к первому выводу второй сразу после (ну, почти приклеивая). Ведь исходно нужно доказать, что одно выводится ттт, когда выводится второе, а не то, что оба выводятся из друг друга. Ну, это формальные заморочки.

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

Теперь про коммутативность. Мне кажется, начинать нужно с вывода $(B\wedge A)\vdash_H(A\wedge B)$ и дальше применить формулу (1). Верно?

Да. Вообще я надеялся на то, что вы будете использовать высокоуровневые теоремы о выводимости $\vdash_H$ типа дедукции. Смотрите, как можно управиться с коммутативностью:
$A\wedge B\vdash_H A$, потому что $\vdash_H A\wedge B\to A$ (акс.) и по теореме дедукции;
$A\wedge B\vdash_H B$, потому что $\vdash_H A\wedge B\to B$ (акс.) и по теореме дедукции;
$B, A\vdash_H B\wedge A$, потому что $\vdash_H B\to(A\to B\wedge A)$ и теорема дедукции два раза;
осталось поприменять теорему о транзитивности выводимости, и получим $A\wedge B\vdash_H B\wedge A$ (а потом сделаем замену $A\leftrightarrow B$ — фокус, с ассоциативностью, увы, не проходящий).

Вывод, существование которого будет доказываться всеми этими теоремами, будет практически такой, как у вас получился — длинный и правильный, но не выписывать его явно, по-моему, приятно. Так же можно будет разделаться с ожидаемым $A\wedge B\to\Delta'\vdash_H B\wedge A\to\Delta'$. Так как у вас дальше аналогичные штучки с дизъюнкцией, я бы посоветовал этот путь.

-- Чт май 04, 2017 17:50:45 --

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

такой, как у вас получился — длинный и правильный

Правильность, правда, лучше бы поручать проверять не мне, а какой-нибудь программе…

[Sinoid]

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

Ведь исходно нужно доказать, что одно выводится ттт, когда выводится второе

Так с этой я и показывал, что

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

$(A\wedge B)\wedge C\to\Delta' \vdash_H A\wedge (B\wedge C)\to \Delta'$.

Тогда, если $\vdash_H (A \wedge B)\wedge C \to \Delta'$, то и $\vdash_H A\wedge (B \wedge C) \to \Delta'$.

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

осталось поприменять теорему о транзитивности выводимости

Эта теорема у упомянутых мной авторов в явном виде не формулируется, а я хотел остаться в рамках книги.

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

осталось поприменять теорему о транзитивности выводимости

Не совсем понятно: формула $A\wedge B\vdash A,\, B$ не принадлежит ИВ. Соответственно рекомендация

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

я бы посоветовал этот путь.

пока не совсем ясна.

[arseniiv]

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

Так с этой я и показывал, что

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

$(A\wedge B)\wedge C\to\Delta' \vdash_H A\wedge (B\wedge C)\to \Delta'$.

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

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

Эта теорема у упомянутых мной авторов в явном виде не формулируется, а я хотел остаться в рамках книги.

Но ведь ничто не мешает вам изобрести и доказать её с нуля. Ну ладно, это уж как хотите.

(Если вам мешает отсутствие формулировки, совместимой с учебником, то, думаю, такая:

Если $\Gamma\vdash A$ и $\Delta,A\vdash B$, то $\Gamma,\Delta\vdash B$.

будет прекрасно подходить. Ну и в доказательстве теоремы как обычно (вроде вы её уже как-то доказывали в другом контексте?) используется то же почти-склеивание выводов, т. е. вообще-то я её уже и так неявно имел в виду.)

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

Не совсем понятно: формула $A\wedge B\vdash A,\, B$ не принадлежит ИВ.

Только секвенция, а не формула. Но я и не говорю о секвенции, я имел в виду только обычные выводимости $\vdash_H$ из гипотез в ИВ, где это, конечно, тоже не формула, а просто запись, обозначающая выводимость.

[Sinoid]

Что-то я подзапутался.

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

(Если вам мешает отсутствие формулировки, совместимой с учебником, то, думаю, такая:

Если $\Gamma\vdash A$ и $\Delta,A\vdash B$, то $\Gamma,\Delta\vdash B$.

Это подсказка для доказательства ассоциативности или коммутативности конъюнкции? Я понял вот что.

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

$A\wedge B\vdash_H A$, потому что $\vdash_H A\wedge B\to A$ (акс.) и по теореме дедукции;
$A\wedge B\vdash_H B$, потому что $\vdash_H A\wedge B\to B$ (акс.) и по теореме дедукции;
$B, A\vdash_H B\wedge A$, потому что $\vdash_H B\to(A\to B\wedge A)$ и теорема дедукции два раза;
осталось поприменять теорему о транзитивности выводимости, и получим $A \wedge B \vdash_H B \wedge A$ (а потом сделаем замену $A \leftrightarrow B$

Это сокращенная запись такого вывода (в ИВ) из $A \wedge B$ $B \wedge A$: из $A \wedge B$ на каких-то этапах вывода получаем $A$, затем $B$ и из только что полученных $A$ и $B$ с помощью пятой аксиомы из книги Верещагина, Шена выведу $B \wedge A$, что и будет означать, что $A \wedge B \vdash_{H}B \wedge A$. Верно?

[arseniiv]

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

Это подсказка для доказательства ассоциативности или коммутативности конъюнкции?

Не, это для метатеоремы о транзитивности выводимости, если вы всё же захотите ею пользоваться для сокращения выкладок.

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

Это сокращенная запись такого вывода (в ИВ) из $A \wedge B$ $B \wedge A$: из $A \wedge B$ на каких-то этапах вывода получаем $A$, затем $B$ и из только что полученных $A$ и $B$ с помощью пятой аксиомы из книги Верещагина, Шена выведу $B \wedge A$, что и будет означать, что $A \wedge B \vdash_{H}B \wedge A$. Верно?

Ага.

Кстати, почему Шена? Он же Шень.

[Sinoid]

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

Кстати, почему Шена? Он же Шень.

Ето у меня уже закипает.

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

Не, это для метатеоремы о транзитивности выводимости

Если вас не затруднит, давайте пока без метатеории. У Верещагина, Шеня пока никакой метатеории и в помине нет. Ну нет да и нет и бог с ней. Мне бы сейчас без нее осилить. Так, сейчас, пока копался, пришла мысль про коммутативность дизъюнкции. Надо показать, что $A\vee B\vdash_{H}\, B\vee A$. Но ведь это элементарно. (Аксиоматика Верещагина, Шеня)
1. $A \rightarrow B \vee A$ (акс. 7);
2. $B \rightarrow B \vee A$ (акс. 6);
3. $(A\rightarrow B\vee A)\rightarrow((B\rightarrow B\vee A)\rightarrow(A\vee B\rightarrow B\vee A))$ (акс. 8);
применяя 2 раза МР, получу $\vdash_{H}(A\vee B\rightarrow B\vee A))$, Откуда и последует, что нужно. Не думаю, что применение леммы о дедукции в данном случае сильно бы сократило выкладки. Сейчас буду думать, как сократить вывод ассоциативности дизъюнкции.

[arseniiv]

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

Если вас не затруднит, давайте пока без метатеории.

Но теорема о дедукции тоже метатеорема. Вообще любые теоремы, которые вы докажете про вывод — это ведь не теоремы рассматриваемой теории, а именно метатеоремы, просто обычно тут не пишут «мета», чтобы, видимо, читателей не пугать.

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

Надо показать, что $A\vee B\vdash_{H}\, B\vee A$. Но ведь это элементарно. (Аксиоматика Верещагина, Шеня)
1. $A \rightarrow B \vee A$ (акс. 7);
2. $B \rightarrow B \vee A$ (акс. 6);
3. $(A\rightarrow B\vee A)\rightarrow((B\rightarrow B\vee A)\rightarrow(A\vee B\rightarrow B\vee A))$ (акс. 8);
применяя 2 раза МР, получу $\vdash_{H}(A\vee B\rightarrow B\vee A))$, Откуда и последует, что нужно.

Ага.

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

Сейчас буду думать, как сократить вывод ассоциативности дизъюнкции.

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

[Sinoid]

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

а вот его исчерпывающее описание может быть короче его явного вида, если использовать в этом описании метатеоремы и не включать их доказательства

Попробую. $C \vdash_{H}\, B \vee C$ (МР из акс. 7), $B \vee C \vdash_{H}\, A \vee(B \vee C)$ (МР из акс. 7) (2), откуда $C \vdash_{H}\, (A \vee(B \vee C))$, а эту формулу опять-таки с прицелом на использование в дальнейшем в качестве выводимой левой части другой выводимости так и тянет переписать в виде $\vdash_{H}\,(C\rightarrow A\vee(B\vee C))$ (3) (может, запись в таком виде и не к чему, просто на большее пока мозгов не хватает). Далее $B \vdash_{H}\, B\vee C$ (МР из акс. 6), и, с учетом (2), $B \vdash_{H}\, A \vee(B \vee C)$ по тем же причинам тянет ее переписать в виде $ \vdash_{H}\,(B \rightarrow A \vee (B \vee C))$ (3). По акс. 6, $A\rightarrow A\vee(B\vee C)$ (4) Далее, в силу акс. 8, $(A\rightarrow A\vee(B\vee C))\rightarrow((B\rightarrow A\vee(B\vee C))\rightarrow(A\vee B\rightarrow A\vee(B\vee C)))$, откуда, в силу (3) и (4) получаю: $\vdash_H (A\vee B\rightarrow A\vee(B\vee C))$ (5). В силу акс. 8 могу написать: $(A\vee B\rightarrow A\vee(B\vee C))\rightarrow((C\rightarrow A\vee(B\vee C))\rightarrow((A\vee B)\vee C\rightarrow A\vee(B\vee C)))$, откуда, с учетом (5) и (3) могу написать: $\vdash_{H}((A\vee B)\vee C\rightarrow A\vee(B\vee C))$, что, в принципе и требовалось. В принципе, получается, что вывод подсократился только в самом начале. Видать, пока у меня с применением метатеории практики маловато, потому и получилось длинновато.

[arseniiv]

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

Видать, пока у меня с применением метатеории практики маловато, потому и получилось длинновато.

Да, тут не хватает метатеоремы «если $\Gamma, X\vdash_H Z$ и $\Gamma, Y\vdash_H Z$, то $\Gamma, X\vee Y\vdash_H Z$», получающейся как раз «обдедуктиванием» аксиомы 8, признаю (действительно, без обработки подобным образом почти всех аксиом толку будет не очень много). Возможно, мне не стоило так прям настаивать. В конце концов, когда заполнение пропусков закончится, проще будет пользоваться исчислением секвенций, раз уж мы в конечном счёте о нём.

[Sinoid]

Иду дальше. Покажу, что из $\Gamma\rightarrow(\Delta\vee A)$ выводимо $(\Gamma\wedge\neg A)\rightarrow\Delta$. Для этого достаточно показать, что $\Delta\vee A\vdash(\neg A\rightarrow\Delta)$. Сделать это не составит большого труда, ввиду того, что по аксиоме 8 $(\Delta\rightarrow(\neg A\rightarrow\Delta))\rightarrow((A\rightarrow(\neg A\rightarrow\Delta))\rightarrow(\Delta\vee A\rightarrow(\neg A\rightarrow\Delta)))$, а дальше через МР. Первая посылка - это чистая аксиома 1, а вторая - немного переделанная аксиома 9.