Мат. логика, формальный вывод.

[1stpm90]

Помогите с заданием. Написать формальный вывод. и теорему дедукции.
$A\sim B$ $\mapsto$ $\overline{B}$\to $\overline{A}$$

[luitzen]

1stpm90 писал(а):

Помогите с заданием. Написать формальный вывод. и теорему дедукции.
$A\sim B$ $\mapsto$ $\overline{B}$\to $\overline{A}$$

То, как будет выглядеть вывод, сильно зависит от того, какая у Вас система аксиом и какими правилами вывода можно пользоваться. Но, наверное, где-то во первых строках нужно будет вывести из формулы $A\sim B$ формулу $A\to B$.

А теорема дедукции — вот она (вдруг пригодится): $A \vdash B \;\Rightarrow\;\, \vdash A \to B$.
Иными словами: если что-то из чего-то выводится, то оно же из него и следует .

[Профессор Снэйп]

Непонятно, кстати, что здесь за эквивалентность. То есть что подразумевается под $A \sim B$. Есть два стандартных варианта расшифровки этой "эквивалентности".

1) $A \sim B$ означает, что $A \vdash B$ и $B \vdash A$.

2) $A \sim B$ означает, что $\vdash (A \rightarrow B) \mathbin{\&} (B \rightarrow A)$.

Впрочем, легко показать (используя ту же теорему о дедукции), что для произвольных $A$ и $B$ (1) выполнено тогда и только тогда, когда выполнено (2).

Добавлено спустя 1 минуту 11 секунд:

Кстати, что автор имел в виду, когда писал стрелочку $\mapsto$, тоже непонятно.

[gefest_md]

Профессор Снэйп писал(а):

Непонятно, кстати, что здесь за эквивалентность. То есть что подразумевается под $A \sim B$. Есть два стандартных варианта расшифровки этой "эквивалентности".

1) $A \sim B$ означает, что $A \vdash B$ и $B \vdash A$.

2) $A \sim B$ означает, что $\vdash (A \rightarrow B) \mathbin{\&} (B \rightarrow A)$.

Впрочем, легко показать (используя ту же теорему о дедукции), что для произвольных $A$ и $B$ (1) выполнено тогда и только тогда, когда выполнено (2).

Если в пунктах 1) и 2) рассматривать только правую часть, то из 2) выводится 1) вообще, а обратное, 2) из 1), выводится, как я понимаю, только в ИВ. В ИП нельзя переходить произвольно от $A\vdash B$ к $\vdash A\to B.$ Ну может поэтому подразумевается 2).

[Профессор Снэйп]

gefest_md писал(а):

...обратное, 2) из 1), выводится, как я понимаю, только в ИВ. В ИП нельзя переходить произвольно от $A\vdash B$ к $\vdash A\to B.$ Ну может поэтому подразумевается 2).

Кто это Вам такую глупость сказал?

Исчисление предикатов, если можно так выразиться, "наследует" исчисление высказываний. Все аксиомы и все правила вывода, заданные в ИВ, имеют место и в ИП. Так что всё, что выводится в ИВ, в ИП также выводится.

И теорема о дедукции в ИП тоже справедлива. Хотя для её доказательства недостаточно сослаться на ИВ, поскольку в ИП новые правила вывода появляются. Так что эту теорему надо отдельно доказывать. Но она доказывается

[gefest_md]

Профессор Снэйп писал(а):

... Так что всё, что выводится в ИВ, в ИП также выводится...

Я о том, что А это не формула ИВ, а формула ИП.

[Профессор Снэйп]

gefest_md писал(а):

Я о том, что А это не формула ИВ, а предикат.

Какой, в ж..., предикат!? Если речь идёт о ИП, то $A$ --- формула ИП.

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

[gefest_md]

Исправил "предикат".

Профессор Снэйп писал(а):

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

По поводу 1) и 2) ответ был формальным, поверхностным: $\sim$ есть и в ИВ, и в ИП, а условия теорем о дедукции разные.

[Профессор Снэйп]

gefest_md писал(а):

...а условия теорем о дедукции разные.

Да ну? И в чём же разница?

Я вообще не понимаю, что Вы хотите сказать. Не то, чтобы ваши утверждения были ложными... Я просто смысла в них не вижу! Какой-то набор слов на заданную тему!!!

[1stpm90]

Профессор Снэйп писал(а):

Кстати, что автор имел в виду, когда писал стрелочку $\mapsto$, тоже непонятно.

Имелось ввиду вот это \vdash
$A\sim B$ $\vdash$ $\overline{B}$\to $\overline{A}$$

[Профессор Снэйп]

1stpm90 писал(а):

Профессор Снэйп писал(а):

Кстати, что автор имел в виду, когда писал стрелочку $\mapsto$, тоже непонятно.

Имелось ввиду вот это \vdash
$A\sim B$ $\vdash$ $\overline{B}$\to $\overline{A}$$

Э-э-э... Тогда либо вообще полная глупость получается, либо под $A \sim B$ подразумевается просто формула $(A \rightarrow B) \mathbin{\&} (B \rightarrow A)$. А что, тоже вариант

[gefest_md]

Отвлекусь от пунктов 1) 2). Объясню как я понял ТД в ИП. Предположим учитель предложил ученикам сделать вывод из $x^2-2x-3=0.$ У одной группы учеников получится такой вывод

$$x^2-2x-3=0\ \Rightarrow\ \ldots\ \Rightarrow\ x=3\vee x=-1.$$

$$x^2-2x-3=0\vdash x=3\vee x=-1.$$

У других

$$x^2-2x-3=0\ \Rightarrow\ 2^2-2\cdot 2-3=0\ \Rightarrow\ -3=0.$$

$$x^2-2x-3=0\vdash -3=0.$$

Теперь для второго вывода попробуем применить ТД. Получим теорему

$$x^2-2x-3=0\to -3=0.$$

Далее:

$$\vdash\forall x(x^2-2x-3=0\to -3=0).\quad\forall\mbox{-введение}$$

$$\vdash 3^2-2\cdot 3-3=0\to -3=0.\quad\mbox{аксиома}$$

$$\vdash 0=0\to -3=0.$$

$$\vdash -3=0.\qquad\mbox{MP}$$

Поэтому ТД была использована ошибочно. И есть случаи когда ТД не может, без специальных оговорок, обосновать переход от $A\vdash B$ к $\vdash A\to B.$

[luitzen]

gefest_md писал(а):

У одной группы учеников получится такой вывод

$$x^2-2x-3=0\ \Rightarrow\ \ldots\ \Rightarrow\ x=3\vee x=-1.$$

Вы бы это, не сильно увлекались использованием значка $\Rightarrow$…
Я его употреблял в качестве знака некоей метатеории (теорема дедукции в каком-то смысле является метатеоремой), а лучше просто писать «если… то…».

В вашем случае рассуждения учеников должны быть записаны как-то так: $(x^2-2x-3=0)\ \vdash\ (x=3\vee x=-1)$.
Или, на худой конец, так: \vdash x^2-2x-3=0\ \Rightarrow\ \vdash x=3\vee x=-1$.

Пусть Профессор Снэйп меня поправит, если что. Я квадратных уравнений давно не решал .

[gefest_md]

luitzen писал(а):

....
В вашем случае рассуждения учеников должны быть записаны как-то так: $(x^2-2x-3=0)\ \vdash\ (x=3\vee x=-1)$.
...

Пусть Профессор Снейп меня поправит, если что.

Мой основной учебник по МЛ - "Клини". Он объясняет почему $\vdash A\to B$ надо читать как $\vdash(A\to B)$, а не $(\vdash A)\to B.$

[luitzen]

Того понимания, которое Вы мне приписываете, у себя не нашёл. Отредактировал цитированное Вами сообщение, убрав бессмысленные скобки, и говорю словами: в варианте «на худой конец» главным знаком является $\Rightarrow$, а следующие по «главности» — это два $\vdash$.