There are four papers by Vladimir Alfeevich Kuznetsov, which discuss the above titled topic: **(1)** Some problems in set theory from the standpoint of a formal system G+ of Gentzen type. (Russian) Akad. Nauk Ukrainy Inst. Mat. Preprint 1992, no. 21, 51 pp. **(2)** The forcing method from the point of view of a formal system G+ of Gentzen type. (Russian) Akad. Nauk Ukrain. SSR Inst. Mat. Preprint 1991, no. 19, 59 pp. **(3)** Classical descriptive set theory from the point of view of the Gentzen-type formal system G+. (Russian) Akad. Nauk Ukrain. SSR Inst. Mat. Preprint 1990, no. 40, 63 pp. **(4)** Set theory from the point of view of the Gentzen-type formal system G+. (Russian) Akad. Nauk Ukrain. SSR Inst. Mat. Preprint 1990, no. 13, 63 pp. The papers are in Russian, and I even could not find any access to them. Also their review in [Mathscinet](http://www.ams.org/mathscinet/index.html) do not say much about the results of the papers. >**I wonder to know if someone can explain in some details the results obtained in the above papers, in particular paper no. 2.** > >**Also I am interested in finding some reference in English related to the above papers.** Thanks in advance. **Remark.** As an example, the review of the second paper in Mathscinet is as follows: "This paper is devoted to a systematic presentation of the forcing method in a nontraditional focus: we present proofs of theorems in the form of trees of a formal system $G^+$ of Gentzen type in the Zermelo-Fraenkel and Morse axiom systems. The proofs presented contain practically all the nuances of set-theoretic constructions.'' See [here](http://www.ams.org/mathscinet/pdf/batch.pdf?b=1218015&b=1160626&b=1108685&b=1070403) for the review of the papers.