Помогите решить задачу по мат.логике.

[diff]

Доброго времени суток.

Очень прошу помочь в решении данной задачи.
У самого уже целую неделю не получается.

Задача из курса "Математическая логика и теория алгоритмов".
Доказать задачу нужно в исчислении высказываний.
При решении пользоваться только ниже приведенными аксиомами и теоремами!



Задача (доказать в исчислении высказываний).

A v (A&B)= A

Схемы Аксиом:
1) A -> (B -> A)
2) (A -> (B -> C)) -> ((A -> B) -> (A -> C))
3) (-B -> -A) -> (( -B -> A) -> B)

Теоремы:
1) A -> B , B -> C, |- A -> C
2) A -> (B -> C), B |- A -> C
3) --A -> A
4) A -> --A
5) -A -> (A -> B)
6) (-B -> -A) -> (A -> B)
7) (A -> B) -> (-B -> -A)
8) A -> (-B -> -(A -> B))
9) (A -> B) -> (( -A -> B) -> B)

-A = отрицание
--A = двойное отрицание
-(A v B) отрицание на всю скобку.


Известно что решение примера должно строится следующим образом:

A v (A&B) = A (= это есть эквивалентность тройное ровно)

Также известно что A&B = -(A -> -B) ; A v B = -A -> --B


Нужно доказать 2 системы когда

A v (A&B) |- A

и

A |- A v (A&B)



HELP..........

Доп. информация есть в книге Э.Мендельсона "Введение в мат.логику".
Если нужно вышлю на E-mail.

[luitzen]

Вот Вам эскиз доказательства для $A \rightarrow (\neg A \rightarrow \neg (A \rightarrow \neg B))$ и $(\neg A \rightarrow \neg (A \rightarrow\neg B)) \rightarrow A$.
Вы уж как-нибудь подверстайте его под Вашу задачу.

Первая формула является подстановкой в формулу $(A \rightarrow (\neg A \rightarrow B))$, которую легко получить из Вашей
теоремы 5 (подумайте, как).

Вторая формула является подстановкой в консеквент аксиомы 3. Чем тогда будет антецедент? Кажется, его легко можно вывести с использованием теорем 4 и 5 (подумайте, как).

[diff]

Помогите доказать c помощью моих аксиом и теорем вот это:

(-A -> A) |- A


очень нужно.


help!

[luitzen]

1. Знаете ли Вы, что значит знак $\;\vdash$ ?
2. Подставьте в Вашу девятую теорему $\neg A$ вместо $A$ и $A$ вместо $B$. Дальше просто.

[diff]

>> 1. Знаете ли Вы, что значит знак |- ?

ну вроде как он означает следует.
Я прав?

[luitzen]

Я бы лучше сказал «выводимо». Ну а как насчёт (2) ? Всё получилось?

[diff]

Ну а как насчёт (2) ? Всё получилось?

Вы знаете неуверен в правильности решения.
Не могли бы показать свой вариант решения?

[luitzen]

diff писал(а):

Не могли бы показать свой вариант решения?

Правила этого раздела и пункт (III.3) правил форума не рекомендуют делать это.

В общих чертах. Запишите гипотезу $(\neg A\rightarrow A)$. Осуществите описанную выше подстановку в теорему 9. Затем по modus ponens отбросьте посылку. У того, что получилось, снова отбросьте посылку по modus ponens (она сильно похожа на одну из Ваших теорем) и получите долгожданное однобуквенное заключение. В соответствии с определением штопора Вы доказали то, что хотели.

P.S. Неплохо все-таки указывать modus ponens в числе разрешенных к использованию схем аксиом, теорем и правил вывода.

[diff]

1) (-A -> A) –гипотеза

теорема (9) (A -> B) -> (( -A -> B) -> B)
-A = A ; A = B ;

2) (-A -> A ) -> ((-A -> A) -> A)
3) (-A -> A) MP (2)
4) (-A -> A) -> A
5) (-A -> A) MP (4)

Посмотрите, так правильно будет?

Если нет, то скажите где ошибся.

Заранее спасибо.

[luitzen]

Что пишется в анализе вывода, в строке, соответствующей формуле, полученной на том или ином шаге вывода? Пишется объяснение того, как она была получена. И это пишется для формулы, получаемой на любом шаге. И отнюдь не пишется объяснение того, зачем она нам может пригодиться (как это сделано, по-видимому, для шага 2).

Если формула является результатом подстановки во что-то «уже имеющееся», то указывается, где это имеющееся имеется, и, по возможности, описывается, чтo взамен чего мы подставляли.

Если формула получена через modus ponens, то указываются обе формулы, из которых она была получена по этому правилу вывода.

В выводе же нету ничего кроме шагов (а у Вас есть что-то между шагами 1 и 2). И венчается вывод тем, что мы, собственно, выводим. А поскольку доказываем мы, совсем строго говоря, метатеорему, постольку в конце должно быть ещё небольшое дополнительное рассуждение.

Я начну, а Вы продолжайте.

\begin{align*} 1.\quad & (\neg A \rightarrow A ) &\hbox{гипотеза} \\ 2.\quad & (\neg A \rightarrow A ) \rightarrow ((\neg \neg A \rightarrow A) \rightarrow A) & \hbox{Т9:~} A = \neg A, B = A \\ 3.\quad & (\neg \neg A \rightarrow A) \rightarrow A & 1, 2, \hbox{MP}\\ 4.\quad & \ldots \end{align*}

[diff]

Спасибо, разобрался с задачей!


p.s. только решение строилось на схеме 3.