Markov's Principle and Russian Constructivism

Origin. A.A. Markov (1950s). Russian constructive mathematics. Computable sequences. Church's thesis. Foundation of recursive mathematics.

Models. All objects computable. Markov's principle: ¬¬∃ implies ∃ for decidable predicates. Church's thesis internalized. Recursive mathematics.

Formalism.

Markov's principle (MP): ∀n(P(n) ∨ ¬P(n)) ∧ ¬¬∃n.P(n) → ∃n.P(n). If P decidable and not-not-exists, then exists. Unbounded search terminates. Constructive?

Church's thesis (CT): Every function ℕ → ℕ is computable. All sequences recursive. Strong assumption. Russian constructivism.

CT formally: ∀f:ℕ→ℕ. ∃e. ∀n. {e}(n) = f(n). Every function has index. Extensionally computable. Recursive analysis.

Russian recursive mathematics: All reals computable. Functions on reals computable. CT + MP. Different from Bishop.

Consequences of CT: Ceitin's theorem (also Kreisel–Lacombe–Shoenfield): every function from a complete separable metric space to a metric space is pointwise continuous. There are no discontinuous functions at all — the opposite of the classical picture. Specker: there is a computable bounded increasing sequence of rationals with no computable limit, so the constructive reals are not order-complete. Consequently [0,1] is not compact in RUSS: Heine–Borel fails, and there is a continuous function on [0,1] that is unbounded. Different real line.

MP justification: If ¬¬∃n.P(n) and P decidable: Search: test P(0), P(1), ... Termination: if doesn't terminate, ¬∃n.P(n), contradicting ¬¬∃. So terminates: witness found. Argument valid?

Relation to intuitionism: Brouwer: MP fails. Markov: MP acceptable. Different views on search. Philosophical divide.

Symbols.

Metatheory. MP is exactly double-negation elimination restricted to Σ⁰₁ formulas, and it is not derivable in Heyting arithmetic, so it is a genuine addition rather than a reformulation. What it adds is nevertheless invisible at the level of computational content: Markov's rule — from ⊢ ¬¬∃n.P(n) infer ⊢ ∃n.P(n) — is admissible in HA, which Friedman's A-translation (1978) proves, and HA + MP is Π⁰₂-conservative over HA. The status of CT is settled by realizability. Kleene's 1945 number realizability interprets HA and validates the extended Church's thesis ECT₀; Troelstra's characterization theorem closes the circle, since HA + ECT₀ proves A ↔ "A is realizable", so realizability is not merely sound for that theory but exactly axiomatizes it. The resulting analysis is not classical analysis with fewer theorems but a different subject: Ceitin and, independently, Kreisel, Lacombe and Shoenfield make every function continuous; Specker's sequence refutes order-completeness; Kleene's singular tree refutes the fan theorem, so RUSS contradicts Brouwerian intuitionism as well as classical mathematics.

Applies to. Constructive mathematics. Computability. Foundations. Russian tradition.

Limitations. MP has no BHK justification: the search is known to terminate only because non-termination was refuted, and a refutation of non-termination is not a construction, which is precisely why Brouwer rejected it. Even granted, it yields a witness and no bound, so a program extracted through MP has no complexity guarantee whatever — unbounded search is the whole content of the principle. CT is not a neutral addition but a partition of the field: it is inconsistent with classical mathematics, and Kleene's singular tree makes it inconsistent with Brouwer's fan theorem too, so RUSS, INT and CLASS are pairwise incompatible extensions of Bishop's common core and results do not transfer between them. The recursive real line loses order-completeness by Specker's sequence, loses the Heine–Borel theorem, and admits a continuous unbounded function on [0,1]; and Ceitin's theorem removes discontinuous functions entirely, so step functions and characteristic functions of undecidable sets are simply not available as objects.

© 2026 Lingenic LLC