What does the law of the exeluted middle follow from?
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VI, Tome 40 (1974), pp. 30-37
Citer cet article
Voir la notice du chapitre de livre provenant de la source Math-Net.Ru
Theories considered contain Heyting arithmetic and the axiom of existence of functions 1.4. Elementary theory of real numbers is constructed along the usual lines (e.g.[4]). It is proved that the law of excluded middle (as a scheme for arithmetic formulae) follows from the statements: the equality of real numbers is decidable; every non-decreasing bounded sequence converges; every partial function can be extended to a total one. The following three theorems are equivalent modulo Markov principles a) decidability of equality, b) the above-mentioned theorem about non-decreasing sequences, c) Bolzano–Weierstrass theorem that every bounded sequence has a convergent subsequence. Lebesgue's theorem that every denumerable open covering of [0,1] contains a finite subcovering follows from each one of a)–c) and is weaker than any of them.