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

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

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

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

Історія

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

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

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

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

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

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

$(\mathrm{\forall }n(P(n)\vee \mathrm{\neg }P(n))\wedge \mathrm{\neg }\mathrm{\forall }n\mathrm{\neg }P(n))\to \mathrm{\exists }nP(n)$

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

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

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

$\mathrm{\forall }n(P(n)\vee \mathrm{\neg }P(n)),\mathrm{\neg }\mathrm{\neg }\mathrm{\exists }nP(n)⊢\mathrm{\exists }nP(n)$

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

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

$\mathrm{\neg }\mathrm{\neg }\mathrm{\exists }nf(n)=0\to \mathrm{\exists }nf(n)=0,$

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

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

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

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

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

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

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

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

Див. також

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

Посилання

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