Преобразования генценовских формализмов в гильбертовские

[arseniiv]

Хотелось бы просто ссылку на литературу. Это уж точно где-нибудь в полноте расписано. Конкретнее, интересует натуральная дедукция, а sequent calculus, хотя в принципе и интересует немного тоже, но в практической задаче формулировки именно в первом виде.

Заранее спасибо, конечно же.

[arseniiv]

[Time skip]

Кому интересно, я потом от этого стремления ушёл. Мне нужно было просто записывать натуральную дедукцию более скромно, линейно, а это можно устроить, используя старых добрых Карри—Говарда, собирая выводы некой штуки в соответствующий тип и конкретным выводам сопоставляя терм-значение, а выводам из гипотез $\gamma_1,\ldots,\gamma_n$ — термы вида $\lambda\gamma_1.\cdots\lambda\gamma_n.t$, ну и т. д., получается какая-нибудь теория типов. Гипотетические выводы в посылках меня только и путали.