Вывести пропозициональные тавтологии

[Kosat]

Делаю и обсуждаю большое задание, сейчас решаю номер четыре.
На с.142-143 есть доказательство теоремы о дедукции для исчисления предикатов, но там лишь намечены нужные пропозициональные тавтологии. Мне их надо вывести через аксиомы и правила вывода. То, что у меня есть, слишком длинно (получается из одной строки исходного вывода 100-130 строк модифицированного). Может кто-то знает, как решить иначе? Перепишу требуемые пропозициональные тавтологии, но попытку решения копировать из вышеуказанной темы не буду - она получена несовершенным машинным способом и правда СЛИШКОМ длинна.

$$X \to Y \to Z\vdash Y \to X \to Z $$ $$X \to Y \to Z\vdash X \wedge Y \to Z $$ $$X \wedge Y \to Z\vdash X \to Y \to Z $$ $

Укажу используемые схемы аксиом Клини для исчисления высказываний (есть ещё правило вывода modus ponens):
\begin{gather} F\to(G\to F) \\ (F\to G)\to((F\to(G\to H))\to(F\to H)) \\ F\to(G\to F\wedge G) \\ F\to F\vee G \\ F\to G\vee F \\ F\wedge G\to F \\ F\wedge G\to G \\ (F\to G)\to((H\to G)\to(F\vee H\to G)) \\ (F\to G)\to((F\to\neg G)\to\neg F) \\ \neg\neg F\to F \end{gather}

\vdash $\vdash$

[Kosat]

Импликация правоассоциативна.

[Kosat]

Вторая тавтология неправильно скорректировалась. Правильно будет так:

$$$X \to Y \to Z \vdash X \wedge Y \to Z $$$

[Deggial]

Поправил.