Мат. логика и теория алгоритмов

[DonVito]

Доказать формально выражение $C \to (A \wedge B \to B \vee C)$, используя правило подстановки, правило "модус поненс" и системы аксиом.
Пользуясь аксиомами
$A \to (B \to A) (1)$
$(A \to (B \to C)) \to ((A \to B) \to (A \to C)) (2)$,
пришел в тупик.
Сделал подстановку $C$ вместо $A$, $A \wedge B$ вместо $B$, $B \vee C$ в аксиоме (2), получил
$(C \to (A \wedge B \to B \vee C)) \to ((C \to A \wedge B) \to (C \to B \vee C))$.
Подскажите, как можно получить выражение $C \to (A \wedge B \to B \vee C)$ в следствии после некоторых подстановок вместо пропозициональных переменных, чтобы по правилу вывода доказать выводимость выражения?
Составил таблицу истинности и выяснил, что формула есть тавтологией, значит она должна выводиться из аксиом.

[Deggial]

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

DonVito
Приведите попытки решения, укажите конкретные затруднения.
Наберите все формулы и термы $\TeX$ом правильно: каждая формула целиком заключается в одну пару долларов.
Инструкции по оформлению формул здесь или здесь (или в этом видеоролике).
См. также тему Что такое карантин, и что нужно делать, чтобы там оказаться.
После исправлений сообщите в теме Сообщение в карантине исправлено, и тогда тема будет возвращена.

[Lia]

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

[gefest_md]

Аксиом не хватает. План такой:
1. $C\to B\vee C$ - аксиома
2. $(C\to B\vee C)\to [A\wedge B\to (C\to B\vee C)]$ - аксиома
3. $A\wedge B\to (C\to B\vee C)$ - MP 1, 2
4. $[A\wedge B\to (C\to B\vee C)]\to [C\to (A\wedge B\to B\vee C)]$ - перестановка посылок
5. $C\to (A\wedge B\to B\vee C)$ - MP 3, 4
Теперь надо вставить в этот список доказательство формулы 4. Доказательство теоремы о дедукции содержит метод нахождения формальных доказательств.

[DonVito]

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

Аксиом не хватает. План такой:
1. $C\to B\vee C$ - аксиома
2. $(C\to B\vee C)\to [A\wedge B\to (C\to B\vee C)]$ - аксиома
3. $A\wedge B\to (C\to B\vee C)$ - MP 1, 2
4. $[A\wedge B\to (C\to B\vee C)]\to [C\to (A\wedge B\to B\vee C)]$ - перестановка посылок
5. $C\to (A\wedge B\to B\vee C)$ - MP 3, 4
Теперь надо вставить в этот список доказательство формулы 4. Доказательство теоремы о дедукции содержит метод нахождения формальных доказательств.

Доказывается ли формула 4 как-то без теоремы о дедукции?

[arseniiv]

Теорема о дедукции — это метатеорема, говорящая о существовании одного вывода, если существует другой. Так что да.

[Nemiroff]

$A \to B, B \to C \vdash A \to C$ умеете доказывать?

$C \to (B \to C)$ — аксиома
$(B \to C) \to (\neg(A \to B) \to (B \to C))$ — аксиома
получаем $C \to (\neg(A \to B) \to (B \to C))$.
Вместо $B$ подставляем $\neg B$, получаем требуемую формулу: $A \vee B = \neg A \to B, A \wedge B= \neg(A \to \neg B)$

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

[gefest_md]

Доказывать сразу формулу $C\to(A\wedge B\to B\vee C)$ не легко. Поэтому сначала можно доказать формулу $A\wedge B\to B\vee C$ из допущения $C$, т.е. $C\vdash A\wedge B\to B\vee C.$ Дальше есть две возможности:
1. Применяем теорему дедукции если это разрешается условием задачи.
2. Переделываем доказательство $C\vdash A\wedge B\to B\vee C$ в доказательство $\vdash C\to(A\wedge B\to B\vee C)$ так, как это показано в доказательстве теоремы о дедукции. Поэтому доказательство теоремы о дедукции полезно знать.

Итак вот доказательство формулы $A\wedge B\to B\vee C$ из допущения $C$ (данный вывод):

1. $C$ - допущение
2. $C\to B\vee C$ - аксиома
3. $B\vee C$ - МП, 1, 2.
4. $B\vee C\to(A\wedge B\to B\vee C)$ - аксиома (1)
5. $A\wedge B\to B\vee C$ - МП, 3, 4

Теперь повторяем доказательство теоремы о дедукции: приписываем спереди к каждой из формул данного вывода символы $C\to$:

...
$C\to C$
...
$C\to (C\to B\vee C)$
...
$C\to B\vee C$
...
$C\to (B\vee C\to(A\wedge B\to B\vee C))$
...
$C\to (A\wedge B\to B\vee C)$

Эта последовательность ещё не вывод формулы $C\to (A\wedge B\to B\vee C)$, но можно перед каждой формулой вставить дополнительные формулы так, чтобы она превратилась в вывод формулы $C\to (A\wedge B\to B\vee C)$.
(Предыдущий план можно оставить без внимания. Он ведёт к намного более длинному доказательству.)