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

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

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

Этот принцип логически верен классически, но не в интуиционистской конструктивной математике. Тем не менее, многие частные примеры этого можно доказать и в конструктивном контексте.

История

Этот принцип был впервые изучен и принят русской школой конструктивизма вместе с принципами выбора и часто с точки зрения реализуемости понятия математической функции.

В теории вычислимости

На языке теории вычислимости принцип Маркова - это формальное выражение утверждения о том, что если невозможно, чтобы алгоритм не завершился, то для некоторого входа он действительно завершится. Это эквивалентно утверждению, что если набор и его дополнение вычислимо перечислимы , то набор разрешим .

В интуиционистской логике

В логике предикатов предикат P над некоторой областью называется разрешимым, если для каждого x в области либо P ( x ) истинно, либо P ( x ) не истинно. Конструктивно это не так тривиально.

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

{\ displaystyle (\ forall n (P (n) \ vee \ neg P (n)) \ клин \ neg \ forall n \, \ neg P (n)) \ rightarrow \ существует n \, P (n)}

То есть, если P не может быть ложным для всех натуральных чисел n , то это верно для некоторого n .

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

Правило Маркова - это формулировка принципа Маркова, как правило. Он утверждает, что выводимо, как только есть, для разрешимости. Формально, ${\ Displaystyle \ существует п \; P (п)}$ ${\ Displaystyle \ neg \ neg \ существует п \; P (n)}$ ${\ displaystyle P}$

{\ Displaystyle \ forall п (п (п) \ лор \ нег Р (п)), \ \ нег \ нег \ существует п \; Р (п) \ \ vdash \ существует п \; Р (п)}

Анне Трельстра ^[1] доказала, что это допустимое правило в арифметике Гейтинга . Позже логик Харви Фридман показал, что правило Маркова является допустимым правилом во всей интуиционистской логике , арифметике Гейтинга и различных других интуиционистских теориях ^[2], используя перевод Фридмана .

В арифметике Гейтинга

Принцип Маркова на языке арифметики эквивалентен :

{\ Displaystyle \ Ne \ Ne \ существует п \; е (п) = 0 \ стрелка вправо \ существует п \; е (п) = 0,}

для в общей рекурсивной функции на множестве натуральных чисел. ${\ displaystyle f}$

Реализуемость

Если конструктивная арифметика переводится с использованием реализуемости в классическую метатеорию, которая доказывает -согласованность соответствующей классической теории (например, арифметики Пеано, если мы изучаем арифметику Гейтинга ), то принцип Маркова оправдан: реализатор - это постоянная функция, которая принимает реализацию, которая не везде ложна, в неограниченный поиск, который последовательно проверяет истинность. Если не везде ложно, то по -согласованности должен быть термин, для которого выполняется, и каждый термин будет в конечном итоге проверяться поиском. Однако если ${\ displaystyle \ omega}$ ${\ displaystyle P}$ $P(0),P(1),P(2),\dots$ $P$ $\omega$ $P$ $P$ нигде не выполняется, то область определения функции-константы должна быть пустой, поэтому, хотя поиск не останавливается, он по-прежнему бессмысленно утверждает, что функция является реализатором. По Закону Исключенного Середина (в нашей классической метатеории), оно должно либо нигде не держаться, либо нигде не держаться, поэтому эта постоянная функция является реализатором. $P$

Если вместо этого в конструктивной мета-теории используется интерпретация реализуемости, то это не оправдано. Действительно, для арифметики первого порядка принцип Маркова точно отражает разницу между конструктивной и классической мета-теорией. В частности, утверждение доказуемо в арифметике Гейтинга с помощью тезиса Расширенного Черча тогда и только тогда, когда существует число, которое доказуемо реализует его в арифметике Гейтинга ; и это доказуемо в арифметике Гейтинга с помощью расширенного тезиса Чёрча и принципа Маркова тогда и только тогда, когда существует число, которое доказуемо реализует это в арифметике Пеано .

В конструктивном анализе

Принцип Маркова эквивалентен на языке реального анализа следующим принципам:

Для каждого действительного числа x , если противоречие, что x равно 0, то существует y ∈ Q такой, что 0 < y <| x |, часто выражающийся в том, что x отделен от 0 или конструктивно не равен ему .
Для каждого действительного числа x , если противоречие, что x равно 0, то существует y ∈ R такой, что xy = 1.

Модифицированная реализуемость не оправдывает принцип Маркова, даже если в мета-теории используется классическая логика: в языке просто типизированного лямбда-исчисления нет реализатора, поскольку этот язык не является полным по Тьюрингу и в нем нельзя определять произвольные циклы.

Принцип слабого Маркова

Принцип слабого Маркова - это более слабая форма принципа Маркова, которую можно сформулировать на языке анализа как

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

Это условное утверждение о разрешимости положительности действительного числа.

Эта форма может быть оправдана принципами непрерывности Брауэра , тогда как более сильная форма им противоречит. Таким образом, он может быть выведен из интуиционистских, реализуемых и классических рассуждений, в каждом случае по разным причинам, но этот принцип недействителен в общем конструктивном смысле Бишопа . ^[3]

Смотрите также

Конструктивный анализ
Тезис Черча (конструктивная математика)
Ограниченный принцип всеведения

использованная литература

^ Энн С. Трельстра. Метаматематическое исследование интуиционистской арифметики и анализа, Springer Verlag (1973), теорема 4.2.4, 2-е издание.
^ Харви Фридман. Классически и интуитивно доказуемо рекурсивные функции. В Скотт, Д.С. и Мюллер, GH Editors, Higher Set Theory, Volume 699 of Lecture Notes по математике, Springer Verlag (1978), стр. 21–28.
^ Ульрих Коленбах , " О слабом принципе Маркова ". Mathematical Logic Quarterly (2002), том 48, выпуск S1, стр. 59–65.

внешняя ссылка

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

[1] Энн С. Трельстра. Метаматематическое исследование интуиционистской арифметики и анализа, Springer Verlag (1973), теорема 4.2.4, 2-е издание.

[2] Харви Фридман. Классически и интуитивно доказуемо рекурсивные функции. В Скотт, Д.С. и Мюллер, GH Editors, Higher Set Theory, Volume 699 of Lecture Notes по математике, Springer Verlag (1978), стр. 21–28.

[3] Ульрих Коленбах , " О слабом принципе Маркова ". Mathematical Logic Quarterly (2002), том 48, выпуск S1, стр. 59–65.

[1]