Можно без двойного отрицания?

[Sinoid]

Здравствуйте! Система аксиом такая:

Связка $\equiv$ определяется как $((A\supset B)\&(B\supset A))$. Нужно доказать $(A\equiv B)\vdash(\neg A\equiv\neg B)$. Перед этим была такая задача: $(A\equiv B),\,(B\equiv C)\vdash(A\equiv C)$. Возникает искушение решить поставленную задачу с помощью соотношения $B\equiv\neg\neg B$, но проблема в том, что перед этим такой задачи нет. Возникает подозрение, что решить поставленную задачу можно как-то без этой немаловажной формулы, а вот как, ума не приложу. Верно ли это? Или перед этим все-таки нужно выводить двойное отрицание?

[knizhnik]

У вас есть

Цитата:

Аксиома 10: $\neg \neg A \supset A$

и

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

Связка $\equiv$ определяется как $((A\supset B)\&(B\supset A))$.

Что еще нужно-то? Двойное отрицание фактически уже есть, уже им можно пользоваться.

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

Возникает подозрение, что решить поставленную задачу можно как-то без этой немаловажной формулы, а вот как, ума не приложу. Верно ли это? Или перед этим все-таки нужно выводить двойное отрицание?

Не факт, что это возможно. То есть возможны конечно разные нетривиальные варианты вывода. Но скорее всего вы впустую потратите время и калории.

[mihaild]

knizhnik в сообщении #1187768 писал(а):

Что еще нужно-то?

Еще нужно $A \supset \neg\neg A$ и $A supset (B \supset (A & B))$.

Но да, смысла искать обходные пути скорее всего нет.

[knizhnik]

mihaild в сообщении #1187770 писал(а):

Еще нужно $A \supset \neg\neg A$

Для этого надо взять аксиому 9 и вместо $B$ подставить в нее $A$, а вместо $A$ подставить $\neg A$.

[Sinoid]

А вот на скорую руку. Вот в рассуждении есть формулы $(A)$ и $(B)$. Я же правильно понимаю, что их конъюнкция выводится из пятой аксиомы с применением первой?

[arseniiv]

Кажется, не только их двоих.

[Sinoid]

arseniiv в сообщении #1187847 писал(а):

Кажется, не только их двоих.

Ну как же, смотрите. Имеем $(A)$, $(B)$.
1. $(A)$ (по условию);
2. $(B)$ (по условию);
3. $(A\supset(A\supset B))$ (акс. 1‚ пп. 1‚ 2);
4. $(A\supset B)$ (МР‚ п. 1‚ п. 3);
5. $(A\supset(A\supset A))$ (акс 1);
6. $(A\supset A)$ (МР‚ п. 1‚ п. 5);
7. $((A\supset A)\supset((A\supset B)\supset(A\supset(A\&B))))$ (акс. 5);
8. $((A\supset B)\supset(A\supset(A\&B))))$ (МР‚ п. 6‚ п. 7);
9. $((A\supset B)\supset(A\supset(A\&B)))$ (МР‚ п. 4‚ п. 8);
10.$(A\supset(A\&B))$ (МР‚ п. 4‚ п. 9);
11. $(A\&B)$ (МР‚ п. 1‚ п. 10).
верно?

[mihaild]

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

3. $(A\supset(A\supset B))$ (акс. 1‚ пп. 1‚ 2);

Вот это вы как получили? Что подставляли в аксиому?

[Sinoid]

mihaild в сообщении #1188024 писал(а):

Sinoid в сообщении #1187990

писал(а):
3. $(A\supset(A\supset B))$ (акс. 1‚ пп. 1‚ 2);
Вот это вы как получили? Что подставляли в аксиому?

я, очевидно, хотел написать $(B\supset(A\supset B))$.

-- 28.01.2017, 21:32 --

с соответствующим изменением обоснования четвертого пункта.

[arseniiv]

Тогда да. Только у вас там шаг лишний.

-- Сб янв 28, 2017 23:34:06 --

Кстати, если это та книжка, про которую думаю, там есть как раз набор задач о допустимых правилах вывода, одна из них про $\frac{A,\quad B}{A\mathbin\& B}$, допустимость которого вы сейчас показали. Можете теперь применять его в выводах как ещё одно правило вывода.

[Sinoid]

arseniiv в сообщении #1188079 писал(а):

Тогда да. Только у вас там шаг лишний.

Какой?

[arseniiv]

9.

[Sinoid]

Да что ты будешь делать! В трех соснах блужу. Вот зачем, спрашивается, я два раза написал одно и то же заключение?

[arseniiv]

(Оффтоп)

Видимо, при наборе заредактировались. Вполне естественно, особенно если код формул длинный.

[Sinoid]

Всем спасибо.