Вывод формулы в ИВ (исчисление высказываний)

[katifan]

Помогите пожалуйста построить вывод с помощью гипотез, аксиом и modus ponens.

$(A \to (B \to ¬C)) \to (¬(A \to ¬B) \to ¬C)$

(нужны объяснения так как очень плохо понимаю эту тему)

[arseniiv]

Аксиомы ИВ бывают разные. Какие у вас?

-- Пн ноя 25, 2013 17:58:10 --

(Кстати, при чём здесь гипотезы? Или у вас ещё и теорема о дедукции имеется в арсенале? Иначе они здесь никак не могут появиться.)

[katifan]

$ 1. A \to(B\toA); 2. (A \to B) \to ((A \to (B \to C)) \to (A \to C)); 3.(A \vee B) \to B; 4.(A \vee B) \to A; 5.(A \to B) \to ((A \to C) \to (A \to (B \wedge C))); 6.A \to(A \vee B); 7.A \to (B \vee A); 8.(A \to C) \to ((B \to C) \to ((A \vee B) \to C)); 9.(A \to B) \to ((A \to ¬B) \to ¬A); 10.¬¬A \to A.$

-- 25.11.2013, 22:10 --

Честно говоря у меня просто дано задание, и объяснения к нему не приложены, а когда в ВУЗе объясняли эту тему, я к своему сожалению болела, поэтому разобраться в ней не могу.

[Sonic86]

(Оффтоп)

katifan в сообщении #792561 писал(а):

$
1. A \to(B\toA);

3.(A \vee B) \to B;

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

С такими аксиомами мне ваще все задачи по плечу.

Теоремы дедукции у Вас точно нет?

katifan в сообщении #792561 писал(а):

Честно говоря у меня просто дано задание, и объяснения к нему не приложены, а когда в ВУЗе объясняли эту тему, я к своему сожалению болела, поэтому разобраться в ней не могу.

Да проблема там не в этом. Смысл-то простой - построить формальное доказательство с помощью Modus ponens и приведенных схем аксиом. А как сам вывод строить - это вопрос непростой. Можно только подсказать, что $\neg C$ можно заменить на $D$ и доказывать формулу $(A \to (B \to D)) \to (¬(A \to ¬B) \to D)$, а потом из нее в конце подстановкой получить требуемую (спасибо arseniiv, - он подсказал ).
Скорее всего понадобятся только аксиомы 1,2,9,10.
Кстати, как Вы пытались решать?

[iifat]

katifan в сообщении #792561 писал(а):

$
1. A \to(B\toA);

;$A \to(B\to A)$ — без пробела можно стыковать только с цифрами

[katifan]

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