Принцип Маркова - Markovs principle

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

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

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

История

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

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

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

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

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

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

{ displaystyle ( forall n (P (n) vee neg P (n)) клин neg forall n , neg P (n)) rightarrow существует n , P (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}$ не везде ложно неограниченный поиск это последовательно проверяет, если ${ Displaystyle P (0), P (1), P (2), точки}$ правда. Если ${ displaystyle P}$ не везде ложно, то по ${ displaystyle omega}$ -согласованность должен быть срок, на который ${ displaystyle P}$ выполняется, и в конечном итоге поиск будет проверяться каждым термином. Однако если ${ displaystyle P}$ нигде не выполняется, то область определения функции-константы должна быть пустой, поэтому, хотя поиск не останавливается, он все еще остается пустым, что функция является реализатором. По закону исключенного среднего (в нашей классической метатеории) ${ displaystyle P}$ должен либо нигде не удерживаться, либо не удерживаться нигде, поэтому эта постоянная функция является реализатором.

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

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

Это эквивалентно на языке реальный анализ, на следующие принципы:

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

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

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

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

{ displaystyle forall x in mathbb {R} ( forall y in mathbb {R} neg neg (0

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

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

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

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

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

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

[2] Харви Фридман. Классически и интуиционистски доказуемо рекурсивные функции. В Скотт, Д. С. и Мюллер, Г. Х. Редакторы, Высшая теория множеств, том 699 конспектов лекций по математике, Springer Verlag (1978), стр. 21–28.

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

[1]

[2]

[3]