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

[Korner]

Здравствуйте. Давно являюсь читателем форума, а сейчас наконец зарегистрировался, чтобы совета спросить.
Свой диплом получил много лет назад, а сейчас племянница попросила помочь с заданием по математической логике. Разобрался со всеми пунктами, застрял на одном. Понимаю, что решение должно быть тривиальным, но похоже маразм уже подкрадывается. Не прошу полного ответа, просто подскажите начальные шаги, пожалуйста.
Как в исчислении высказываний вывести формулу:
A$\to$(B$\to$(C$\to$(D$\to$A)))

Правка. Заново внес формулу в соответствии с правилами

[arseniiv]

Честно говоря, у исчисления высказываний есть разные аксиоматизации. Несколько распространённых совпадают в наличии двух аксиом

$$\begin{array}{ll} \mathsf K. & A\to(B\to A) \\ \mathsf S. & (A\to(B\to C))\to(A\to B)\to(A\to C) \end{array}$$

Если в относящейся к задаче аксиоматизации они есть, то можно начинать.

Если воспользоваться изоморфизмом Карри—Говарда, эти аксиомы соответствуют типам двух функций $K, S$ таких, что $Kxy = x$, $Sxyz = xz(yz)$. Надо через них выразить функцию $Xxyzw = x$. Видно, что $Xxyz = Kx$, $Xxy = K(Kx)$, $Xx = K(K(Kx))$, $X = \lambda x.K(K(Kx))$, после чего можно применить правило $\lambda z.AB = S(\lambda z.A)(\lambda z.B)$, выводимое из выражения для $S$, и получить

$$X = S(\lambda x.K)(\lambda x.K(Kx)) = S(KK)(S(\lambda x.K)(\lambda x.Kx)) = S(KK)(S(KK)(S(KK)(\lambda x.x))),$$

после чего нельзя ничего сделать, если не вспомнить $\lambda x.x = SKK$ (т. к. $SKKx = Kx(Kx) = x$; кстати, отсюда видно, что сгодится и $SK(\text{что угодно})$). Итого $X = S(KK)(S(KK)(S(KK)(SKK)))$, и остаётся применить изоморфизм в обратную сторону, превращая $AB$ в результат применения Modus ponens к $A$ и $B$.

(Выше замаскированно была использована и частично выведена теорема о дедукции.)

[Lia]

Korner
Формулы оформляйте по правилам.

Korner
Вот так

[math]A$\to$(B$\to$(C$\to$(D$\to$A)))[/math]

не надо, надо один доллар в начале формулы, один в конце. И никаких - в середине.

[arseniiv]

А, да, тут использовано соглашение писать $abcd\ldots$ вместо $a(b(c(d\ldots)))$. Т. е. конвертировать назад надо $(S(KK))((S(KK))((S(KK))((SK)K)))$. Очевидно, у вывода будет столько шагов, сколько здесь открывающих скобок, плюс один.

[Korner]

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

А, да, тут использовано соглашение писать $abcd\ldots$ вместо $a(b(c(d\ldots)))$. Т. е. конвертировать назад надо $(S(KK))((S(KK))((S(KK))((SK)K)))$. Очевидно, у вывода будет столько шагов, сколько здесь открывающих скобок, плюс один.

Спасибо. Попробую сейчас всё это проделать.