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

Принцип Маркова, названий на честь Андрія Маркова-молодшого, є принципом умовного існування, що має багато формулювань.

Художнє зображення машини Тьюрінга. Принцип Маркова стверджує, що якщо машина Тьюринга ніколи не зупиниться, то вона повинна зупинитися.

Принцип класично доводиться, але не за допомогою конструктивної логіки. Але для багатьох конкретних випадків цей принцип все ж можна довести, використовуючи обидві логіки.

Історія

Вперше принцип був запропонований російською школою конструктивізму разом із аксіомами залежного вибору та часто використовувався для перевірки існування математичної функції.

У теорії обчислюваності

На мові теорії обчислюваності принцип Маркова формально стверджує, що якщо неможливо, щоб алгоритм зупинявся, то для деяких вхідних даних він зупиниться. Це еквівалентно твердженню, що якщо множина і її доповнення є перерахованою множиною, то множина є обчислюваною.

В логіці предикатів

У логіці предикатів: предикат P над деякою множиною називається обчислювальним, якщо для кожного x в множини або P (x) є істинним, або P (x) не є істинним.

Для обчислювального предикату P над натуральними числами принцип Маркова звучить так:

$(\forall n(P(n)\vee \neg P(n))\wedge \neg \forall n\,\neg P(n))\rightarrow \exists n\,P(n)$

Тобто, якщо предикат P не є хибним для всіх натуральних чисел n, то він є істинним для деяких n .

Правило Маркова

Правило Маркова — це формулювання принципу Маркова як правила. Воно стверджує, що $\exists n\;P(n)$ можна отримати, тільки якщо виконується $\neg \neg \exists n\;P(n)$ для $P$. Формально,

$\forall n(P(n)\lor \neg P(n)),\ \neg \neg \exists n\;P(n)\ \vdash \ \exists n\;P(n)$

В логіці Гейтінга

Якщо використовувати мову математичного аналізу, то принцип Маркова можна сформулювати так:

$\neg \neg \exists n\;f(n)=0\rightarrow \exists n\;f(n)=0,$

де$f$ — обчислювальна функція на натуральних числах.

В аналізі функції дійсних змінних

Принцип Маркова можна сформулювати використовуючи аналіз функції дійсної змінної

• Якщо для кожного дійсного числа x, твердження, що x дорівнює 0 є хибним, то існує y ∈ Q таке, що 0 < y < | x |
• Якщо для кожного дійсного числа x, твердження, що x дорівнює 0 є хибним, то існує y ∈ R такий, що x*y = 1.

Слабкий принцип Маркова

Слабкий принцип Маркова — це слабша форма принципу Маркова, яку мовою аналізу можна висловити як

$\forall x\in \mathbb {R} \ \ (\forall y\in \mathbb {R} \ \ \neg \neg (0<y)\vee \neg \neg (y<x))\to 0<x.$

Це умовне твердження про обчислюваність позитивності дійсного числа.

Див. також

• Конструктивний аналіз
• Дисертація Черча (конструктивна математика)
• Обмежений принцип всезнання

Посилання

• Конструктивна математика (Стенфордська енциклопедія філософії)