Построить вывод в исчислении высказываний

[itzsaqr]

Требуется построить вывод:
$A\vee\urcorner B \vdash\urcorner (\urcorner A \wedge B)$
Аксиоматика стандартная (10 аксиом и modus ponens)
Препод дал пару подсказок, которые помогли мне в решении, но я все равно застрял:
1. $\urcorner A \wedge B\Rightarrow\urcorner A$ (некоторое кол-во шагов) $A \Rightarrow\urcorner(\urcorner A \wedge B)$
2. $\urcorner A \wedge B \Rightarrow B$ (так же некоторое кол-во шагов) $\urcorner B \Rightarrow\urcorner(\urcorner A \wedge B)$
(1.), по подсказке, получается следующим образом:
1) $A \Rightarrow(B \Rightarrow\urcorner C)$
2) $A \Rightarrow(B \Rightarrow C)$
3) Аксиома 9 и 2 раза случай 4 из теоремы о дедукции.
4) $A \Rightarrow\urcorner B$

Собственно, по 4 и 5 аксиомам я получил
$\urcorner A \wedge B \Rightarrow \urcorner A$ и $\urcorner A \wedge B \Rightarrow B$
Потом по 9 аксиоме получил
$(\urcorner A \wedge B \Rightarrow B) \Rightarrow (((\urcorner A \wedge B) \Rightarrow \urcorner B) \Rightarrow \urcorner (\urcorner A \wedge B))$

Потом после применения случая 4 т. о дедукции
$A \Rightarrow (((\urcorner A \wedge B) \Rightarrow \urcorner B) \Rightarrow \urcorner (\urcorner A \wedge B))$
Очень хочется получить формулу $((\urcorner A \wedge B) \Rightarrow \urcorner B)$, но она не тиф и, следовательно, не выводима(вроде бы).

[dgwuqtj]

Зато формула $A \Rightarrow ((\neg A \wedge B) \Rightarrow C)$ является общезначимой, можете её вывести и подставить $C := \neg B$.

[gefest_md]

Как бы я доказал?

$A\vee\neg B$ - допущение.

$A\to(\neg A\wedge B\to A)$ - аксиома 1.

$\neg B\to(\neg A\wedge B\to A)$ - доказать и вставить доказательство сюда. Доказательство теоремы о дедукции даёт метод (Клини, Математическая логика, теорема о дедукции).

$$(A\to(\neg A\wedge B\to A))\to((\neg B\to(\neg A\wedge B\to A))\to(A\vee\neg B\to(\neg A\wedge B\to A)))$$

- аксиома «разбор случаев».

$A\vee\neg B\to(\neg A\wedge B\to A)$ - MP.

$\neg A\wedge B\to A$ - MP.

$\neg A\wedge B\to \neg A$ - аксиома.

$(\neg A\wedge B\to A)\to((\neg A\wedge B\to\neg A)\to\neg (\neg A\wedge B))$ - аксиома «от противного».

$\neg (\neg A\wedge B)$ - MP.

[itzsaqr]

gefest_md в сообщении #1621720 писал(а):

Как бы я доказал?

$A\vee\neg B$ - допущение.

$A\to(\neg A\wedge B\to A)$ - аксиома 1.

$\neg B\to(\neg A\wedge B\to A)$ - доказать и вставить доказательство сюда. Доказательство теоремы о дедукции даёт метод (Клини, Математическая логика, теорема о дедукции).

$$(A\to(\neg A\wedge B\to A))\to((\neg B\to(\neg A\wedge B\to A))\to(A\vee\neg B\to(\neg A\wedge B\to A)))$$

- аксиома «разбор случаев».

$A\vee\neg B\to(\neg A\wedge B\to A)$ - MP.

$\neg A\wedge B\to A$ - MP.

$\neg A\wedge B\to \neg A$ - аксиома.

$(\neg A\wedge B\to A)\to((\neg A\wedge B\to\neg A)\to\neg (\neg A\wedge B))$ - аксиома «от противного».

$\neg (\neg A\wedge B)$ - MP.

Очень понравилась ваша идея. То есть все сводится к решению одной задачи, а не двух: $\neg B\to(\neg A\wedge B\to A)$
Решил использовать теорему о дедукции 1 раз
$\urcorner B \vdash \urcorner A \wedge B \rightarrow A$

$(\urcorner A \wedge B \rightarrow \urcorner B)\rightarrow(((\urcorner A \wedge B) \rightarrow ( \urcorner B \rightarrow A))\rightarrow ( \urcorner A \wedge B \rightarrow A))$

$(\urcorner A \wedge B \rightarrow \urcorner B)$ - акс 1 и МР.

$((\urcorner A \wedge B) \rightarrow ( \urcorner B \rightarrow A))\rightarrow ( \urcorner A \wedge B \rightarrow A)$ - MP и всё, дальше опять формула, которую вывести не получается.

Так же рассмотрел идею с двойной теоремой о дедукции: $\urcorner B, (\urcorner A \wedge B) \vdash A$. Но тут у меня даже идеи нет, какая аксиома может мне помочь.

[gefest_md]

itzsaqr в сообщении #1621734 писал(а):

Так же рассмотрел идею с двойной теоремой о дедукции: $\urcorner B, (\urcorner A \wedge B) \vdash A$.

Это имел в виду. Сначала записать вывод $\neg B,\ \neg A\wedge B\vdash A.$ Вот он.

$\neg B$ - допущение.
$\neg A \wedge B$ - допущение.
$\neg A\wedge B \to B$ - аксиома.
$B$ - MP.
$\neg B\to( B \to A)$ - аксиома.
$B\to A$ - MP.
$A$ - MP.

Затем согласно доказательству теоремы о дедукции из учебника Клини, приписываем слева от каждой строчки выражение $\neg A\wedge B\to,$ добавляя скобки если нужно. То есть.

$\neg A\wedge B\to\neg B$ - MP
$\neg A\wedge B\to\neg A \wedge B$
$\neg A\wedge B\to(\neg A\wedge B \to B)$
$\neg A\wedge B\to B$
$\neg A\wedge B\to(\neg B\to( B \to A))$
$\neg A\wedge B\to (B\to A)$
$\neg A\wedge B\to A$

Этот список строк не вывод $\neg B\vdash\neg A\wedge B\to A,$ но его можно превратить в такой вывод, добавляя перед каждой строчкой нужные формулы. Получится вывод. Какие строчки нужно добавить разбирается в доказательстве теоремы о дедукции. Например перед первой строчкой добавляется допущение $\neg B$ и аксиома 1, и тогда она получается по MP из них.

Аналогично этот второй вывод можно использовать, чтобы получить окончательно вывод $\vdash\neg B\to(\neg A\wedge B\to A).$

Ещё раз. Здесь используется не утверждение теоремы о дедукции (Если $A\vdash B,$ то $\vdash A\to B$), это было бы другим решением, а идея доказательства теоремы (из учебника Клини).

-- Вс дек 10, 2023 13:50:13 --

Строгое применение этого метода даст длинные выводы, но в процессе поиска вывод можно укоротить. Вообще стоит ожидать, что поиск вывода облегчается. Обратите внимание во втором выводе на последние три строчки (5,6,7). Там применима аксиома по-моему вторая (длинная аксиома для импликации).

[itzsaqr]

gefest_md в сообщении #1621740 писал(а):

Обратите внимание во втором выводе на последние три строчки (5,6,7). Там применима аксиома по-моему вторая (длинная аксиома для импликации).

А у меня, кажется, ее нет(используется система Клини). Т.е. теперь мне нужно вывести эту аксиому или ход решения кардинально поменяется?

[gefest_md]

itzsaqr в сообщении #1621755 писал(а):

А у меня, кажется, ее нет(используется система Клини). Т.е. теперь мне нужно вывести эту аксиому или ход решения кардинально поменяется?

В учебнике Клини она имеет номер 1b: $(A\to B)\to((A\to(B\to C))\to(A\to C)).$

-- Вс дек 10, 2023 15:06:10 --

Применительно к последним двум строкам второго списка эта аксиома будет такой:
$(\neg A\wedge B\to B)\to((\neg A\wedge B\to(B\to A))\to (\neg A\wedge B\to A)).$

[itzsaqr]

А, вот увидел. А еще у вас есть аксиома $\neg B\to( B \to A)$. Она же не из аксиоматики Клини? В целом алгоритм понятен.

[gefest_md]

itzsaqr в сообщении #1621773 писал(а):

А еще у вас есть аксиома $\neg B\to( B \to A)$.

Она из интуиционистской системы аксиом. Перепутал системы аксиом. Неформально вместо $A$ доказывается $\neg\neg A$, от противного, и в конце применяется классическая аксиома $\neg\neg A\to A.$ То есть доказывается $\neg B, \ B\vdash\neg\neg A.$

[itzsaqr]

gefest_md в сообщении #1621778 писал(а):

То есть доказывается $\neg B, \ B\vdash\neg\neg A.$

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

[gefest_md]

itzsaqr в сообщении #1621780 писал(а):

Потом мы дважды применяем док-во теоремы о дедукции и получаем указанную аксиому, которую можем спокойной использовать в главном выводе, я правильно понимаю?

Нет, если просят построить формальный вывод (из допущений - когда слева от $\vdash$ есть одна или несколько формул, это допущения). В случае формального вывода из допущений, в анализе доказательства, справа от каждой строчки объясняется её присутствие там и это может быть только одно из трёх возможностей: или допущение, или аксиома, или MP. Но не теорема о дедукции. Теорема о дедукции применяется в неформальном доказательстве в рамках более общей теоремы о введении и удалении логических связок (у Клини теорема 13).

То есть для формулы $\neg B\to(B\to A)$ надо получить список формул, являющийся её доказательством; формальный вывод; но уже без допущений, в анализе справа может быть только: или аксиома, или MP. Этот список будет готовым блоком, который можно вставить в другом выводе, который «запросил» этот вывод.