Abstract:
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.