Доказать формулу исчисления высказываний

[kantrovik]

Здравствуйте, помогите,пожалуйста доказать формулу исчисления высказываний, используя правило подстановки (А v В -> (A ->$\overline{B}$)) ->((A v B -> A) ->(A v B ->$\overline{B}$))

[Xaositect]

Эта формула - результат постановки(какой, сообразить нетрудно ) в аксиому
$(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow (A\rightarrow C))$

[gris]

Используйте знаки $\vee\,\,\wedge\,\,\to$

$$(A\vee B \to (A \to\overline{B})) \to((A \vee B \to A) \to (A \vee B \to \overline{B}))$$

Ну и что же не получилось?

[tdk]

не могу понять по какому принципу осуществляется подстановка

[kantrovik]

Xaositect написал написал вторую аксиому следствия, что с ней делать?смотрю похожие задания и тоже на могу разобрать как делается подстановка?

[Xaositect]

Так.
Как выглядит правило подстановки?

[kantrovik]

затем мы используем аксиому 1 $A\to (B \to A)$ и потом по правилу заключения получаем $(A\to B) \to(A\to A) $ ?

[Xaositect]

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

[gefest_md]

kantrovik писал(а):

затем мы используем аксиому 1 $A\to (B \to A)$ и потом по правилу заключения получаем $(A\to B) \to(A\to A) $ ?

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

[kantrovik]

Если формула А доказуема, x – некая переменная, В – некая формула, то формула в результате замены в формуле А вместо x формулы В – является доказуемой.
Т.е. |- A

|-

$$\int\limits_{x}^{B}A $$

это правило подстановки.

[gefest_md]

kantrovik
В этом случае $A(x)$ не есть высказывание, а переменный предикат. Высказыванием будет $A^0(a)$ если $A^0$ конкретный предикат определенный на некоторой области $\mathfrak{M}$ и $a\in\mathfrak{M}.$

[Xaositect]

kantrovik писал(а):

Если формула А доказуема, x – некая переменная, В – некая формула, то формула в результате замены в формуле А вместо x формулы В – является доказуемой.
Т.е. |- A

|-

$$\int\limits_{x}^{B}A $$

это правило подстановки.

Какого вида переменная $x$ имеется в виду в этом определении?

Добавлено спустя 2 часа 30 минут 45 секунд:

Скажем, в "Математической логике" Клини правило подстановки выглядит так:

Пусть $E$-формула, в которую входят только атомы $P_1, P_2,\dots, P_n$, а $E^*$ - формула, полученная из $E$ одновременной подстановкой формул $A_1, A_2,\dots, A_n$ вместо $P_1, P_2,\dots, P_n$ соответственно. Тогда, если общезначима $E$, то $E^*$ также общезначима.

Атом у Клини - это то, что также называют пропозициональной переменной, а правило подстановки можно переписать и в виде:

Пусть $E$-формула, $P$ - входящий в нее атом, а $E^*$ - формула, полученная из $E$ подстановкой формулы $A$ вместо $P$. Тогда, если общезначима $E$, то $E^*$ также общезначима.

В качестве примера применения правила подстановки можно привести следующий: если мы знаем, что формула $P\rightarrow P$ общезначима(или доказуема в классической логике высказываний), то общезначимыми будут также формулы $\neg A\rightarrow \neg A$, $(A\vee B) \rightarrow (A\vee B)$, $(A\rightarrow B) \rightarrow (A\rightarrow B)$ и т.д.

[Чудо-в-перьях]

Берем аксиому $(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow (A\rightarrow C))$, полагаем $A = A \vee B, B = A, C = \bar{B}$ и производим соответствующую замену.

[kantrovik]

Не понял, надо просто подставить $\ A =A\cupB, B = A, C =\overline{B}$ во вторую аксиому и всё решение?

[gris]

Лучше так написать:
$(X\rightarrow(Y\rightarrow Z))\rightarrow((X\rightarrow Y)\rightarrow (X\rightarrow Z))$

где $X,Y,Z$ произвольные предикаты. В частности мы можем подставить
$X = A \vee B, \,\,Y = A, \,\,Z = \bar{B}$
и получить требуемую формулу.