Подтолкните к выводу в ИВ

[Sinoid]

Здравствуйте! Я в этой теме буду писать, несколько дней. Когда уже у самого совсем ну никак. А вы сразу прямым текстом, пожалуйста, не отвечайте, просто подталкивайте в нужную сторону. А, может быть, все и одним вопросом обойдется. Итак, система аксиом ИВ такая:

По определению, запись $P\equiv Q$ обозначает $((P\supset Q)\wedge(Q\supset P))$ Нужно доказать, что $(A\equiv B)\vdash((A\wedge C)\equiv(A\wedge C))$. Вот что я навыводил:
1. $((A\supset B)\wedge(B\supset A))$ (по условию);

2. $(((A\supset B)\wedge(B\supset A))\supset(A\supset B))$ (акс. 3);

3. $(A\supset B)$ (МР‚ п. 1‚ п. 2);

4. $(((A\supset B)\wedge(B\supset A))\supset(B\supset A))$
(акс. 4);

5. $(B\supset A)$ (МР‚ п. 1‚ п. 4);
вот если бы при этих вводных удалось вывести, скажем, $((A\wedge C)\supset B)$, то, с помощью аксиом 3 и 5 я бы вывел $((A\wedge C)\supset B \wedge C)$. Меня это направление мысли привлекает еще и тем, что, с одной стороны, в рассуждении уже выведено $(A\supset B)$, а, с другой, формулка $((A\supset B)\supset((A\wedge C)\supset B))$, судя по таблице истинности, есть тавтология. А вот как вывести сей факт из аксиом ума не приложу. А я вообще на верной дороге или нет?

[Xaositect]

Дорога верная. А $(A \supset B) \supset ((B \supset C) \supset (A \supset C))$ вы уже выводили? Подумайте, что может быть средним в $(A \wedge C \supset \dots) \supset (({\dots} \supset B) \supset (A \wedge C \supset B))$, чтобы это было полезным в Вашей задаче.

[Sinoid]

Xaositect в сообщении #1188820 писал(а):

Подумайте, что может быть средним в $(A \wedge C \supset \dots) \supset (({\dots} \supset B) \supset (A \wedge C \supset B))$,

Ну, это понятно, что $A$, только

Xaositect в сообщении #1188820 писал(а):

А $(A \supset B) \supset ((B \supset C) \supset (A \supset C))$ вы уже выводили?

Нет, еще не выводил. Ближайшая задача, где может выплыть нечто похожее - буква и) данного номера $(A\equiv B)\vdash((A\supset C)\equiv(B\supset C))$, я же пока решаю букву д).

[Xaositect]

Ну тогда придумывайте подходящую подстановку во вторую аксиому. Надо получить $A\wedge C \supset B$, что можно подставить, чтобы $(A \wedge C \supset {\dots}) \supset((A\wedge C \supset ({\dots} \supset B)) \supset (A\wedge C \supset B))$ было полезным?

[Sinoid]

Xaositect в сообщении #1189072 писал(а):

Надо получить $A\wedge C \supset B$, что можно подставить, чтобы $(A \wedge C \supset {\dots}) \supset((A\wedge C \supset ({\dots} \supset B)) \supset (A\wedge C \supset B))$ было полезным?

Понял. На эту роль подходит что

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

3. $(A\supset B)$

, что

Xaositect в сообщении #1188820 писал(а):

5. $(B\supset A)$

посылку же полученной импликации получу правилом МР из первой аксиомы. Верно?

[Xaositect]

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

посылку же полученной импликации получу правилом МР из первой аксиомы. Верно?

Это верно. А вот подформулу Вы подобрали неправильно, ибо ни $A\wedge C \supset ((A\supset B)\supset B)$, ни $A\wedge C \supset ((B\supset A)\supset B)$ у Вас доказать не получится.

[Sinoid]

Понял. Нужно подставить $A$. Тогда тут

Xaositect в сообщении #1189072 писал(а):

$(A \wedge C \supset {\dots}) \supset((A\wedge C \supset ({\dots} \supset B)) \supset (A\wedge C \supset B))$

Посылка вначале формулы есть просто аксиома 3, а вторую я выведу из первой аксиомы, т.к. в рассуждении уже есть $(A\supset B)$.

-- 02.02.2017, 15:30 --

А вот типичный случай. Конъюнкцию из сомножителей я уже вывел в другой задаче. Вот мне опять понадобилось это свойство. Это что, мне повторять рассуждение по пунктам при этих сомножителях?

[Sinoid]

(Оффтоп)

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

Я в этой теме буду писать, несколько дней

Да уж... Ну ладно, через тернии и к звездам.

Решал задачи по Лаврову, Максимовой (оттуда и аксиомы). В голову (для решения одной задачи) пришла такая формула: $((A\supset B)\supset((A\supset\neg B)\supset\neg A)$. Языки и исчисления Верещагина, Шена открыл, там эта формула в числе аксиом. Казалось бы, эта формула получается из аксиомы 2 при $C=0$, но ни 0, ни $\bot$ в этих аксиомах вообще не фигурируют. Скажите, а вот эта формула вообще выводима из этих аксиом?

[Sonic86]

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

Казалось бы, эта формула получается из аксиомы 2 при $C=0$, но ни 0, ни $\bot$ в этих аксиомах вообще не фигурируют. Скажите, а вот эта формула вообще выводима из этих аксиом?

Она из них "как бы не получается", лишь в обычной модели. Здесь же - чистые аксиомы.
Скорее всего она невыводима, поскольку там есть новый символ $\neg$ - можно попытаться подобрать такую модель для аксиом, чтобы аксиома оказалась ложной. Например, посмотреть что будет, если $\neg B$ в модели означает $B$, проверить в многозначных логиках и т.п.

[Xaositect]

Sonic86, не путайте человека. У него аксиомы с отрицанием есть, 9 и 10 (в первом сообщении). Их и нужно использовать.

[Sonic86]

Ааа, прошу извинить. Мне показалось, что речь об системе из 3-х аксиом в ИВ, я про нее говорил.

[Sinoid]

Xaositect в сообщении #1196272 писал(а):

Sonic86, не путайте человека. У него аксиомы с отрицанием есть, 9 и 10 (в первом сообщении). Их и нужно использовать.

Задача сводится к выводу формулы $((A\supset B)\supset(A\supset\neg(A\supset\neg B)))$. Только я формулу $(\neg(A\supset\neg B)\equiv(A\wedge B))$ еще не знаю как выводить.

[Sinoid]

Формулу-то $(\neg(A\supset\neg B)\supset(A\wedge B))$ я выведу на раз. Вопрос, как в другую сторону? Или эта формула здесь вообще не при чем?

[Sinoid]

А так бы было замечательно: $((A\supset A)\supset((A\supset B)\supset(A\supset(A\wedge B))))$ - это же-ж вылитая пятая аксиома.

[Sinoid]

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

Формулу-то $(\neg(A\supset\neg B)\supset(A\wedge B))$ я выведу на раз. Вопрос, как в другую сторону?

Скорее всего, в обратную сторону я получу из второй аксиомы. Верно?