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

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

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

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

Історія

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

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

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

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

У логіці предикатів: предикат 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.$

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

Див. також

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

Посилання

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