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: Discontinuous functions exist on [0,1]. But: all functions computable. Computable discontinuous. 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.

Symbol	Unicode	Meaning
MP	—	Markov's principle
CT	—	Church's thesis
{e}	—	partial recursive function
REC	—	recursive

Metatheory. Recursive analysis. CT internalized. MP. Russian school.

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

Limitations. CT controversial. Non-standard reals. Limited acceptance. Philosophical commitment.