nLab Russian constructivism

Summary

The Russian school of constructive mathematics, associated principally with Andrey Markov Jr, was (is?) a variety of constructive mathematics focussing on recursion theory.

Principles and results

• Classically true principles (not always accepted by other constructivists):
  • Markov's principle for natural numbers: if an infinite sequence of binary digits is not all $0$, then it has a least one $1$;
  • dependent choice for natural numbers.
• Classically false principles:
  • every partial function from $\mathbb{N}$ to $\mathbb{N}$ is computable;
  • every set is a subquotient of $\mathbb{N}$.
• Classically false results (false w.r.t. classical functions and sets):
  • every total function from $\mathbb{R}$ (the real line) to $\mathbb{R}$ is pointwise continuous (Ceitin's theorem);
  • there exist continuous functions from $[0,1]$ (the unit interval) to $\mathbb{R}$ that are pointwise continuous but not uniformly continuous;
  • there exist bounded sets of real numbers with no supremum (given by Specker sequences).

References

• Hannes Diener, Constructive reverse mathematics, Habilitationsschrift Fakultät IV - Naturwissenschaftlich-Technische Fakultät, 2018. (arXiv:1804.05495, dspace:ubsi/1306)