Выводимость формулы

[Lady000]

Здравствуйте!
подскажите,пожалуйста,как справиться с заданием:
вывести исходя из аксиом Черчелля, следствий, Modus Ponus, теоремы о дедукции и правил
$\neg(A\&B)\rightarrow C\vdash(A\rightarrow(B\rightarrow C))$
АТЧ:
$1)~A\rightarrow(B\rightarrow A)$
$2)~(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A \rightarrow C))$
$3)~(($\neg A)\rightarrow(\neg B))\rightarrow(B\rightarrow A)$
у меня были мысли сначала написать,что
1)$\neg\neg(A\rightarrow(\neg B))\rightarrow C$(гипотеза)
дальше вообще ничего понять не могу(

[Toucan]

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

Чтобы оттуда выбраться

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

2. Приведите свои попытки решения задачи и объясните, что конкретно вызывает затруднения. Заодно выпишите, пожалуйста, "аксиомы Черчелля".

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

________________
Всякий, кто поступил в университет, но не хочет сам учиться - враг своей страны, подрывающий ее научно-технический, интеллектуальный и оборонный потенциалы.
(c) по мотивам сообщения Yuri Gendelman.

[Toucan]

Немного поправил формулу и вернул.

Отрицание набирается так: $\neg A$

\neg A

[Maslov]

Проверьте задание: там точно отрицание есть перед $(A~\&~B)$?

[Xaositect]

Ну раз нам надо доказать $A\to(\dots)$, то в качестве гипотезы логично взять не то, что Вы там написали, а просто $A$. Напишите частный случай теоремы о дедукции, который позволит получить то, что нужно, взяв гипотезу $A$.

Lady000 в сообщении #570315 писал(а):

аксиом Черчелля

Чьих аксиом?

[Maslov]

Надо бы сначала по таблице истинности на всякий случай проверить

[Lady000]

Maslov в сообщении #570480 писал(а):

Проверьте задание: там точно отрицание есть перед $(A~\&~B)$?

да,отрицание там есть точно

мне посоветовали раскрыть отрицание,а дальше вообще ничего понять не могу(

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

Ну раз нам надо доказать $A\to(\dots)$, то в качестве гипотезы логично взять не то, что Вы там написали, а просто $A$. Напишите частный случай теоремы о дедукции, который позволит получить то, что нужно, взяв гипотезу $A$.

Lady000 в сообщении #570315 писал(а):

аксиом Черчелля

Чьих аксиом?


аксиом четчя,или как там его, я не помню(

[Maslov]

Lady000 в сообщении #570547 писал(а):

аксиом четчя

Это Алонзо Чёрч (Alonzo Church)

Могу, конечно, ошибаться, но если рассмотреть соответствующую формулу алгебры высказываний и положить $A = T, B = T, C = F$, то получится

$\models (\neg(T \& T) \to F) \to (T \to (T \to F))$

$\models T \to F$

что, по-моему, как-то не очень хорошо.

[Lady000]

насколько я помню,нам что-то говорили,что нужно сделать,именно исходя из аксиом,MP,следсвий и правил
http://kurs.ido.tpu.ru/courses/disk_mat ... tema12.htm
что-то из этого вроде...
так как вы сделали, я не совсем понимаю..

[Maslov]

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

В данном случае достаточно только половины теоремы о полноте, а именно, "каждая теорема исчисления высказываний является тавтологией алгебры высказываний" (теорема 2.8 по приведенной Вами ссылке).

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

[Lady000]

а допустим,если бы не было отрицания перед первой скобкой?как бы тогда она выводилась?

[Maslov]

Для начала попробуйте доказать выводимость

$A, B \vdash A ~ \& ~ B$

[Lady000]

$A,B\vdash A\&B$(это будет по правилу П3)
а дальше?

[Maslov]

Дальше -- намек.

Если нам надо доказать выводимость

$\Gamma \vdash F \to G$

мы можем сначала доказать

$\Gamma, F \vdash G$

а потом применить теорему о дедукции.

[Lady000]

а по какой теореме или правилу мы это докажем??
и что мы берём за гипотезу?