Принцип Маркова — логічний принцип конструктивної математики, названий на честь Андрія Маркова-молодшого. Він стверджує, що для розв'язної властивості натуральних чисел неможливість того, що жодне число не має цієї властивості, дає підставу стверджувати існування числа, яке її має.
Формально, якщо — предикат над натуральними числами, для якого щодо кожного можна встановити, чи виконується , то принцип Маркова має вигляд:
За умови розв'язності предиката це можна записати коротше як обмежену форму усунення подвійного заперечення:
З обчислювального погляду принцип відповідає необмеженому пошуку: значення послідовно перевіряють, доки не буде знайдено число, для якого виконується. Доведення того, що такий пошук не може тривати нескінченно, гарантує його завершення, хоча не обов'язково дає наперед відому межу кількості кроків.
У класичній логіці принцип Маркова випливає із загального усунення подвійного заперечення. В інтуїціоністській логіці він загалом не виводиться, тому в деяких напрямах конструктивної математики його приймають як окремий додатковий принцип. Зокрема, він був прийнятий у рекурсивному конструктивізмі школи Маркова.
Історія Вперше принцип був запропонований російською школою конструктивізму разом із аксіомами залежного вибору та часто використовувався для перевірки існування математичної функції. Обчислювальна інтерпретація
Нехай — розв'язний предикат над натуральними числами, тобто для кожного конкретного можна за скінченний час установити, чи виконується . Розглянемо алгоритм, який послідовно перевіряє
і завершується, щойно знаходить число , для якого істинне. Кожна окрема перевірка завершується, але наперед може бути невідомо, скільки значень доведеться перевірити. Якщо відповідного числа не існує, пошук триватиме нескінченно.
Твердження
означає, що припущення про відсутність такого числа приводить до суперечності. Принцип Маркова дозволяє перейти від цього твердження до
тобто вважати описаний необмежений пошук допустимим конструктивним способом отримання результату. Доведення гарантує завершення пошуку, хоча може не містити ані самого значення , ані наперед відомої верхньої межі кількості кроків.
У термінах машини Тюрінга можна побудувати машину, яка перебирає натуральні числа та зупиняється після знаходження із властивістю . Тоді принцип Маркова стверджує: якщо припущення, що це конкретне обчислення ніколи не зупиниться, приводить до суперечності, то обчислення зупиниться.
Принцип Маркова не розв'язує проблему зупинки і не дає алгоритму, який визначає завершуваність довільної програми. Для його застосування вже потрібно мати доведення того, що незавершення конкретного пошуку неможливе; сам принцип не надає способу отримати таке доведення.
В логіці предикатів У логіці предикатів: предикат P над деякою множиною називається обчислювальним, якщо для кожного x в множини або P (x) є істинним, або P (x) не є істинним.
Для обчислювального предикату P над натуральними числами принцип Маркова звучить так:
Тобто, якщо предикат P не є хибним для всіх натуральних чисел n, то він є істинним для деяких n .
В арифметиці Гейтінга
Арифметика Гейтінга (, скорочено HA) — інтуїціоністський аналог арифметики Пеано. Обидві теорії описують натуральні числа за допомогою однакової мови першого порядку та арифметичних аксіом, зокрема схеми математичної індукції. Відмінність полягає в логіці: арифметика Пеано використовує класичну логіку, тоді як арифметика Гейтінга — інтуїціоністську.
Одну з поширених арифметичних форм принципу Маркова записують так:
де — всюди визначена рекурсивна функція над натуральними числами, представлена в арифметиці. Оскільки для кожного конкретного значення можна обчислити, рівність є розв'язною властивістю.
Еквівалентно принцип можна сформулювати для примітивно-рекурсивного або безкванторного предиката :
Ця схема не є теоремою арифметики Гейтінга: її примітивно-рекурсивна форма незалежна від HA. Тому принцип Маркова можна додати до арифметики Гейтінга як окрему схему аксіом, але його не можна отримати лише з аксіом HA та правил інтуїціоністської логіки.
Водночас для арифметики Гейтінга є допустимим правило Маркова. Для відповідного розв'язного предиката воно має метаматематичний вигляд:
Тобто якщо в HA вже існує доведення твердження , то це доведення можна перетворити на доведення .
Допустимість правила не означає, що відповідна імплікація доводиться всередині теорії. Принцип Маркова дозволяв би застосовувати перехід від подвійного заперечення до існування всередині доведень, зокрема за наявності додаткових припущень. Правило Маркова є твердженням про перетворення вже завершених доведень теорії. Тому правило може бути допустимим у HA, хоча сам принцип Маркова в ній не виводиться. Арифметика Гейтинга.Арифметика Гейтинга.Арифметика Гейтинга. В аналізі функції дійсних змінних Принцип Маркова можна сформулювати використовуючи аналіз функції дійсної змінної
Якщо для кожного дійсного числа x, твердження, що x дорівнює 0 є хибним, то існує y ∈ Q таке, що 0 < y < | x | Якщо для кожного дійсного числа x, твердження, що x дорівнює 0 є хибним, то існує y ∈ R такий, що x*y = 1.
Правило Маркова
Правило Маркова — метаматематичне правило про перетворення доведень у формальних системах з інтуїціоністською логікою. На відміну від принципу Маркова, воно не є формулою, яку додають до теорії як аксіому, а описує співвідношення між довідністю двох формул.
Для формальної теорії і розв'язного предиката одну зі стандартних форм правила записують так:
Цей запис означає: якщо в теорії уже доведено, що неможливо, аби не існувало числа із властивістю , то існує спосіб перетворити це доведення на доведення існування такого числа.
Правило називають допустимим для теорії, якщо його застосування не дозволяє довести жодної нової теореми: кожне доведення, отримане за допомогою правила, можна замінити доведенням, що використовує лише початкові аксіоми та правила теорії. Зокрема, правило Маркова є допустимим для арифметики Гейтінга та низки інших формальних систем з інтуїціоністською логікою.
Допустимість правила Маркова не означає, що відповідний принцип доводиться всередині теорії. Принцип Маркова мав би форму:
і дозволяв би застосовувати цей перехід усередині доведення, зокрема за наявності додаткових припущень. Правило Маркова стосується лише випадку, коли формула уже є теоремою системи. Тому правило може бути допустимим у формальній теорії, навіть якщо відповідна імплікація в ній не виводиться.
З обчислювального погляду це означає: якщо формальна система доводить, що певний конкретний ефективний пошук не може не завершитися, то з такого доведення можна отримати доведення того, що пошук завершується. При цьому правило Маркова, як і сам принцип, не надає загального способу визначати завершуваність довільних алгоритмів.
Слабкий принцип Маркова Слабкий принцип Маркова — це слабша форма принципу Маркова, яку мовою аналізу можна висловити як
Це умовне твердження про обчислюваність позитивності дійсного числа.
Див. також Конструктивний аналіз Дисертація Черча (конструктивна математика) Обмежений принцип всезнання
Посилання Конструктивна математика (Стенфордська енциклопедія філософії)
Примітки