Доказать существование вывода в аксиоматической теории L

[Ruprecht]

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

a) ${\vdash ¬(A \vee B) \equiv (¬B \& ¬A)}$
b) ${\vdash A \Rightarrow ((A \& B) \vee (A \& ¬B))}$

Под a формулу разделил на две подформулы:
I. ${¬(A \vee B) \Rightarrow (¬B \& ¬A)}$
II. ${(¬B \& ¬A) \Rightarrow ¬(A \vee B)}$
Попытался решить первую (I), но вышло все не особо удачно:
${¬(A \vee B) \vdash (¬B \& ¬A)}$
${¬(¬A \Rightarrow B) \vdash ¬(¬B \Rightarrow ¬¬A)}$
1. ${¬(¬A \Rightarrow B)}$ - посылка
2. Тут изначально пытался использовать теорему 4.2.2 (5), но все вышло громоздко и сразу зашло в тупик


Решил под b, но не уверен правильный ли был ход:
${A, ¬¬(A \Rightarrow ¬B) \vdash ¬(A \Rightarrow ¬¬B)}$
1. ${A}$ - посылка
2. ${¬¬(A \Rightarrow ¬B)}$ - посылка
3. ${¬¬(A \Rightarrow ¬B) \Rightarrow (A \Rightarrow ¬B)}$ - 4.2.2 (2)
4. ${A \Rightarrow ¬B}$ - MP к 2 и 3
5. ${¬B}$ - MP к 1 и 4
6. ${¬B \Rightarrow (B \Rightarrow ¬(A \Rightarrow ¬¬B))}$ - 4.2.2 (4)
7. ${¬B \Rightarrow ¬(A \Rightarrow ¬¬B)}$ - 4.2.2 (1) к 6
8. ${¬(A \Rightarrow ¬¬B)}$ - MP к 4 и 7
9. ${A \& ¬B}$ - D1 к 8

[Lia]

Тема перемещена из форума «Помогите решить / разобраться (М)» в форум «Карантин»
по следующим причинам:

- уберите первую картинку, пожалуйста, и наберите формулы (краткие инструкции: «Краткий FAQ по тегу [math]» и видеоролик Как записывать формулы). Аксиоматику можно оставить картинкой.
- отсутствуют собственные содержательные попытки решения задач(и).

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

[Lia]

Тема перемещена из форума «Карантин» в форум «Помогите решить / разобраться (М)»

[arseniiv]

Всё ниже насчёт a):

Установите сначала, что если $\Gamma, \mathscr A \vdash \mathscr B$ и $\Gamma, \mathscr B \vdash \mathscr A$, то $\Gamma \vdash \mathscr A \equiv \mathscr B$ (используя 4.1.5, 4.1(j), D3 и ещё что-то).

Будем и дальше пользоваться теоремой о дедукции 4.1.5 и выводимостями 4.1(…) и вообще иметь в виду то, что если $\Gamma \vdash \mathscr A_1$, …, $\Gamma \vdash \mathscr A_n$ и $\Gamma, \mathscr A_1, \ldots, \mathscr A_n \vdash \mathscr B$, то $\Gamma \vdash \mathscr B$.

Имеем следующие вещи:
• $\neg B \mathbin\& \neg A \vdash \neg B$,
• $\neg B \mathbin\& \neg A \vdash \neg A$,

Тут приходится прерваться, потому что у вас удаление $\vee$ не предоставили. Неудобно. Попробуйте доказать сами, что $\mathscr A \Rightarrow \mathscr C, \mathscr B \Rightarrow \mathscr C \vdash \mathscr A \vee \mathscr B \Rightarrow \mathscr C$, больно полезная штука. Полезно также, и нам тоже потребуется, введение $\neg$: $\mathscr A \Rightarrow \mathscr B, \mathscr A \Rightarrow \neg \mathscr B \vdash \neg \mathscr A$. Продолжим:

• $\neg A, A \vdash B$, отсюда $\neg A \vdash A \Rightarrow B$
• $(\neg A)\vdash B \Rightarrow B$
• $A \Rightarrow B, B \Rightarrow B \vdash A \vee B \Rightarrow B$
• $\neg A \vdash A \vee B \Rightarrow B$
• но мы также имеем $\neg B \vdash A \vee B \Rightarrow \neg B$
• так что, раз $\neg A, \neg B \vdash A \vee B \Rightarrow B$ и $\neg A, \neg B \vdash A \vee B \Rightarrow \neg B$, выходит $\neg A, \neg B \vdash \neg (A \vee B)$
• так что $\neg B \mathbin\& \neg A \vdash \neg (A \vee B)$

В обратную сторону проще: контрапозицией 4.1(e, e′) мы получим $\neg (A \vee B) \vdash \neg A$ и $\neg (A \vee B) \vdash \neg B$, что в соединении с 4.1(j) даёт нам вывести нужное $\neg A \mathbin\& \neg B$.

Список производных выводимостей в вашем курсе какой-то не систематичный, и хотя дана метатеорема о дедукции, не дана метатеорема про выводимость, которую я привёл — потому остаётся гадать, насколько можно оторваться, а насколько вам придётся восполнять такие непростительные пробелы (так как задания на блуждание в тёмном лесу на ручное составление вывода на низком уровне — это довольно бессмысленная штука; нам же формализация логики не для того нужна).

Если пока можно только предъявлять составленный руками вывод, придётся разворачивать все применения метатеорем… мда.