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

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

Формулировка принципа состоит в следующем:

Пусть для некоторого свойства $\mathcal Y$ имеется алгоритм $\mathfrak A$, выясняющий для всякого натурального числа $N$, обладает ли $N$ свойством $\mathcal Y$. Если опровергнуто предположение о том, что ни одно натуральное число не обладает свойством $\mathcal Y$, то имеется натуральное число со свойством $\mathcal Y$.

Способ построения искомого числа состоит в последовательном переборе натуральных чисел, начиная с нуля, причём на каждом шаге процесса посредством алгорифма $\mathfrak A$ устанавливается, обладает ли рассматриваемое число свойством $\mathcal Y$.

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

$((\forall X(D\lor (\neg D)))\supset((\neg(\neg (\exists XD)))\supset(\exists XD)))$.