Geodesic
Dialog theory of proofs for arithmetics, analysis and set theory
Izvestiya. Mathematics, Tome 44 (1995) no. 3, pp. 571-600 
V. A. Yankov. Dialog theory of proofs for arithmetics, analysis and set theory. Izvestiya. Mathematics, Tome 44 (1995) no. 3, pp. 571-600. http://geodesic.mathdoc.fr/item/IM2_1995_44_3_a6/
@article{IM2_1995_44_3_a6,
     author = {V. A. Yankov},
     title = {Dialog theory of proofs for arithmetics, analysis and set theory},
     journal = {Izvestiya. Mathematics},
     pages = {571--600},
     year = {1995},
     volume = {44},
     number = {3},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/IM2_1995_44_3_a6/}
}
TY  - JOUR
AU  - V. A. Yankov
TI  - Dialog theory of proofs for arithmetics, analysis and set theory
JO  - Izvestiya. Mathematics
PY  - 1995
SP  - 571
EP  - 600
VL  - 44
IS  - 3
UR  - http://geodesic.mathdoc.fr/item/IM2_1995_44_3_a6/
LA  - en
ID  - IM2_1995_44_3_a6
ER  - 
%0 Journal Article
%A V. A. Yankov
%T Dialog theory of proofs for arithmetics, analysis and set theory
%J Izvestiya. Mathematics
%D 1995
%P 571-600
%V 44
%N 3
%U http://geodesic.mathdoc.fr/item/IM2_1995_44_3_a6/
%G en
%F IM2_1995_44_3_a6

Voir la notice de l'article provenant de la source Math-Net.Ru

It is shown that in impredicative extensions of intuitionistic arithmetic, “intuitionistic” analysis, and “intuitionistic” Zermelo–Fraenkel set theory with the help of suitable “bar” axioms it is possible to show the consistency of classical arithmetic, classical analysis, and classical set theory. It is argued that the proofs given enable one to verify the true consistency of the classical systems.

[1] Dzh. Shenfild, Matematicheskaya logika, Nauka, M., 1975 | MR

[2] C. Spector, “Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics”, Proceedings of the Symposia in Pure Mathematics V, ed. J. C. E. Dekker (Rhode Ilsand), AMS, 1962, 1–27 | MR

[3] G. Kraizel, Issledovaniya po teorii dokazatelstv, Mir, M., 1981 | MR