Dialog theory of proofs for arithmetics, analysis and set theory
Izvestiya. Mathematics, Tome 44 (1995) no. 3, pp. 571-600
Cet article a éte moissonné depuis 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.
@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/}
}
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/
[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