Принцип Маркова

Принцип Маркова — один из основных принципов логики конструктивной математики, сформулированный в начале 1950-х годов Андреем Андреевичем Марковым (младшим). Известен также под названиями «ленинградский принцип» и «принцип конструктивного подбора». Представляет собой ослабленный вариант закона двойного отрицания.

Формулировка принципа состоит в следующем: Шаблон:Рамка Пусть для некоторого свойства $𝒴$ имеется алгоритм $𝔄$, выясняющий для всякого натурального числа $N$, обладает ли $N$ свойством $𝒴$. Если опровергнуто предположение о том, что ни одно натуральное число не обладает свойством $𝒴$, то имеется натуральное число со свойством $𝒴$. Шаблон:Конец рамки Способ построения искомого числа состоит в последовательном переборе натуральных чисел, начиная с нуля, причём на каждом шаге процесса посредством алгоритма $𝔄$ устанавливается, обладает ли рассматриваемое число свойством $𝒴$.

С использованием формальных языков конструктивной математической логики (например, ступенчатой семантической системы Маркова) принцип Маркова записывается следующим образом:

$((\mathrm{\forall }X(D\vee (\mathrm{\neg }D)))\supset ((\mathrm{\neg }(\mathrm{\neg }(\mathrm{\exists }XD)))\supset (\mathrm{\exists }XD)))$.