Задача на тему исчисление высказываний.

[kola1357]

Подскажите как доказать выводимость формулы из множества гипотез.
Пример: $(B \to A) \vdash ((A \to B) \to A)$
Я знаю как упростить через формулы алгебры Буля, но в задании сказано, что надо вывести из гипотез ИВ, как это сделать, подскажите, пожалуйста. Какую тут аксиому надо применить ?

[arseniiv]

Исчисление высказываний по-разному можно аксиоматизировать. У вас какая система аксиом?

[kola1357]

arseniiv, у нас просто 10 аксиом, нам не говорили на лекции как эта система называется. Объясните, пожалуйста, на примере любой системы аксиом как решить задачу, я думаю пойму и если что переделаю под нашу систему.

[Toucan]

Тема перемещена в Карантин.

Запишите формулы в соответствии с требованиями Правил форума, т.е. в $\TeX$.
Краткие инструкции можно найти здесь: topic8355.html и topic183.html.
Кроме этого, в теме Видео-пособия для начинающих форумчан можно посмотреть видео-ролик "Как записывать формулы".

Для всех логических связок есть нормальные обозначения: $\to, \vdash$

$\to, \vdash$

После того как исправите сообщение, сообщите об этом в теме Сообщение в карантине исправлено.

-- Пн 27.05.13 22:38:01 --

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

[kola1357]

А нужно перед выводом формулы этой в примере, упростить ее справа ? То выражение справа будет просто $A$, тогда формула проще будет. Но так можно делать в этих задачах или нет ?

[arseniiv]

Нет, нельзя упрощать. В выводе можно использовать только правила вывода. Ну и вводить туда аксиомы и гипотезы.

Это уже потом показывается, что любая выводимая в исчислении высказываний формула — это тавтология алгебры высказываний, и в обратную сторону. И тогда можно смело эквивалентными преобразованиями по формуле, не боясь, что она сменит выводимость. Или не пытаться вывести какую-нибудь тождественно ложную, зная, что зато выводимо её отрицание.

kola1357 в сообщении #729207 писал(а):

у нас просто 10 аксиом, нам не говорили на лекции как эта система называется

Неужто эта?:

$$\begin{array}{l} A \to (B\to A), \\ (A \to (B \to C)) \to ((A \to B) \to (A \to C)), \\ A \wedge B \to A, \\ A \wedge B \to B, \\ A \to (B \to (A \wedge B)), \\ A \to A \vee B, \\ B \to A \vee B, \\ (A \to C) \to ((B \to C) \to (A \vee B \to C)), \\ (A \to B) \to ((A \to \neg B) \to \neg A), \\ \neg\neg A \to A. \end{array}$$

Кстати, у вас вообще задача неправильная, как оказалось. (Надо было сразу проверить. ) Невыводимо это.

[iifat]

Вообще-то, ещё и правила вывода бывают разные.

[kola1357]

arseniiv, да эта система аксиом, а как решить задачу тогда, вы говорите не выводимо. Я вот не знаю какую аксиому надо использовать для доказательства.

[arseniiv]

iifat в сообщении #729316 писал(а):

Вообще-то, ещё и правила вывода бывают разные.

Обычно к этой системе аксиом изначально приложен только Modus ponens, а производные правила, вроде бы, добавляют уже после определения вывода из гипотез, нет?

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

kola1357 в сообщении #729478 писал(а):

arseniiv, да эта система аксиом, а как решить задачу тогда, вы говорите не выводимо. Я вот не знаю какую аксиому надо использовать для доказательства.

В том и дело, что никак. Это было бы выводимо, если бы из $B \to A$ логически следовало $(A \to B) \to A$ (в исчислении высказываний), что эквивалентно тому, что $(B \to A) \to ((A \to B) \to A)$ — тавтология, чего нет. Можете сами проверить.

Видимо, задание было с опечаткой, или переписано неправильно, или ещё что-то.

[kola1357]

arseniiv, действительно опечатка в задании.
Вот так правильно: $(B \to A) \vdash ((A v B) \to A)$
Как вот это доказать, нам дали эти 10 аксиом и модус понес (правило вывода)

[arseniiv]

Вот! Так намного лучше. (Надеюсь, у вас есть где-нибудь рядом вывод $A\to A$, а то я его не помню, а он тут нужен.)

Как прийти к доказательству? Т. к. правило у нас пока только одно — Modus ponens — мы можем вывести только то, что есть в правой части какой-нибудь импликации в аксиомах. Там, в этих правых частях, есть всё, что может попасться в довольно сложной формуле. Так что надо выбрать какую-нибудь аксиому и попробовать с ней вывести.

Например, последняя аксиома вряд ли нам бы принесла что-то полезное, хотя при желании можно было бы составить вывод и с её использованием. Давайте попробуем восьмую: $(A\to C)\to((B\to C)\to(A\vee B \to C))$. Неформально, она говорит, что если из каждой альтернативы дизъюнкции что-то следует, то и из целой дизъюнкции оно следует. А у нас как раз надо вывести, что из дизъюнкции $A \vee B$ следует $A$. Может, мы сможем переписать эту аксиому так, чтобы $(A\vee B)\to A$ могло быть выведено? Да, можем: надо только заменить $C$ на $A$. Получится такая аксиома:

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

Как с помощью неё можно было бы вывести то, что надо? Есть только Modus ponens, и он говорит, что если $\vdash A\to A$, то $\vdash (B\to A)\to(A\vee B \to A)$. И что потом если $\vdash B\to A$, то и $\vdash A\vee B \to A$. А это как раз цель.

Можем ли мы вывести $B \to A \vdash A \to A$? Да, притом гипотеза тут не используется (это я предоставляю вам). Можем ли мы вывести $B\to A \vdash B\to A$? Да: доказательством этого будет одна строка — собственно, использование гипотезы, которая одновременно и то, что надо получить.

Теперь, используя аксиому 8 в форме $(A\to A)\to((B\to A)\to(A\vee B \to A))$, два имеющихся доказательства $B \to A \vdash A \to A$ и $B\to A \vdash B\to A$, попробуйте собрать доказательство $B \to A \vdash (A\vee B)\to A$. Не получится — кто-нибудь поправит. Пробуйте!

(Кстати, это так повезло с тем, что формула «близко» к аксиомам и её можно в них как бы увидеть. В принципе, и более сложные можно так разглядывать, но обычно для этого вводят новые правила вывода. Каждый вывод $A_1, \ldots A_n \vdash B$ порождает правило вывода $\frac{A_1, \ldots, A_n}B$ — его использование всё равно что вставка доказательства $A_1, \ldots A_n \vdash B$ в использующее доказательство. Например, можно доказать $A, B \vdash A \wedge B$ и использовать потом как правило введения конъюнкции. Достаточно сложные формулы с такими правилами выводятся (если они выводимы вообще) почти автоматически.)

($\TeX$.)

Только не $v$, а $\vee$ (\vee или \lor).

[kola1357]

arseniiv, спасибо, вывод $ \vdash A \to A$ формулы нашел.



-- 28.05.2013, 17:49 --

arseniiv, еще хотел спросить еще по одному примеру.
Пример такой: $\vdash (( A \to \lnot B) \to ( B \to \neg A))$
Как тут лучше начать выводить, с какой аксиомы.

И еще я попробовал это сначала упростить, но в результате у меня получилось, что это выражение всегда истинно, так как после упрощения у меня получилось $\vdash 1$ И что тут доказывать уже я не понял, это ведь уже тавталогия.
Ребят, как ставить логическое отрицание в формулах.

[Deggial]

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

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

[Toucan]

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

[iifat]

Пара мелочей.

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

Обычно к этой системе аксиом изначально приложен только Modus ponens

Обычно к этой — несомненно. Но я встречал где-то и другую систему, к ней был приложен Modus tollens. Впрочем, этот вопрос уже решён.

kola1357 в сообщении #729537 писал(а):

как ставить логическое отрицание в формулах

$\bar X$