Принцип Маркова (также известный как принцип Ленинграда [1] ), названный в честь Андрея Маркова-младшего , является условным утверждением существования, для которого существует множество эквивалентных формулировок, как обсуждается ниже. Принцип логически обоснован в классическом смысле , но не в интуиционистской конструктивной математике. Однако многие его частные случаи тем не менее доказуемы и в конструктивном контексте.
Этот принцип был впервые изучен и принят русской школой конструктивизма вместе с принципами выбора и часто с перспективой реализуемости понятия математической функции.
На языке теории вычислимости принцип Маркова является формальным выражением утверждения, что если невозможно, чтобы алгоритм не завершился, то для некоторых входных данных он завершается. Это эквивалентно утверждению, что если множество и его дополнение являются вычислимо перечислимыми , то множество является разрешимым . Эти утверждения доказуемы в классической логике.
В логике предикатов предикат P над некоторой областью называется разрешимым , если для каждого x в области либо P ( x ), либо отрицание P ( x ). Это не является тривиально верным конструктивно.
Принцип Маркова гласит: Для разрешимого предиката P над натуральными числами , если P не может быть ложным для всех натуральных чисел n , то он истинен для некоторого n . Записывается с использованием квантификаторов :
Правило Маркова — это формулировка принципа Маркова как правила. Оно утверждает, что выводимо, как только является, для разрешимого. Формально,
Энн Троелстра [2] доказала, что это допустимое правило в арифметике Гейтинга . Позже логик Харви Фридман показал, что правило Маркова является допустимым правилом в интуиционистской логике первого порядка , арифметике Гейтинга и различных других интуиционистских теориях, [3] используя перевод Фридмана .
Принцип Маркова на языке арифметики эквивалентен следующему:
для полной рекурсивной функции натуральных чисел.
При наличии принципа тезиса Чёрча принцип эквивалентен его форме для примитивных рекурсивных функций . Используя предикат Клини T , последний может быть выражен как
Если конструктивная арифметика переводится с использованием реализуемости в классическую метатеорию, которая доказывает -непротиворечивость соответствующей классической теории (например, арифметику Пеано, если мы изучаем арифметику Гейтинга ), то принцип Маркова оправдан: реализатор - это константная функция, которая переводит реализацию, которая не везде ложна, в неограниченный поиск , который последовательно проверяет, является ли она истинной. Если не везде ложно, то по -непротиворечивости должен быть терм, для которого выполняется, и каждый терм будет в конечном итоге проверен поиском. Однако если нигде не выполняется, то область константной функции должна быть пустой, поэтому, хотя поиск не останавливается, он все еще бессмысленно утверждает, что функция является реализатором. По закону исключенного третьего (в нашей классической метатеории), должно либо выполняться нигде, либо не выполняться нигде, поэтому эта константная функция является реализатором.
Если вместо этого в конструктивной метатеории используется интерпретация реализуемости, то она не оправдана. Действительно, для арифметики первого порядка принцип Маркова точно улавливает разницу между конструктивной и классической метатеорией. В частности, утверждение доказуемо в арифметике Гейтинга с расширенным тезисом Чёрча тогда и только тогда, когда существует число, которое доказуемо реализует его в арифметике Гейтинга ; и оно доказуемо в арифметике Гейтинга с расширенным тезисом Чёрча и принципом Маркова тогда и только тогда, когда существует число, которое доказуемо реализует его в арифметике Пеано .
Принцип Маркова на языке реального анализа эквивалентен следующим принципам:
Модифицированная реализуемость не оправдывает принцип Маркова, даже если в метатеории используется классическая логика: в языке просто типизированного лямбда-исчисления реализатора нет , поскольку этот язык не является полным по Тьюрингу и в нем не могут быть определены произвольные циклы.
Слабый принцип Маркова — это более слабая форма принципа. На языке анализа его можно сформулировать как условное утверждение для положительности действительного числа:
Эта форма может быть оправдана принципами непрерывности Брауэра , тогда как более сильная форма противоречит им. Таким образом, слабый принцип Маркова может быть выведен из интуиционистских, реализуемых и классических рассуждений, в каждом случае по разным причинам, но он не является верным в общем конструктивном смысле Бишопа [ 4] и не доказуем в теории множеств .
Чтобы понять, в чем заключается принцип, полезно рассмотреть более сильное утверждение. Следующее утверждение выражает, что любое действительное число , такое, что ни одно неположительное число не находится ниже него, является положительным:
где обозначает отрицание . Это более сильная импликация, поскольку антецедент слабее. Обратите внимание, что здесь логически положительное утверждение выводится из логически отрицательного. Это подразумевается слабым принципом Маркова при возвышении закона Де Моргана для до эквивалентности.
Если предположить классическое исключение двойного отрицания, то слабый принцип Маркова становится тривиальным, выражая, что число, большее всех неположительных чисел, является положительным.
Функция между метрическими пространствами называется сильно экстенсиональной , если подразумевает , что в классическом смысле является просто контрпозицией функции, сохраняющей равенство. Можно показать, что принцип Маркова эквивалентен предложению о том, что все функции между произвольными метрическими пространствами сильно экстенсиональны, в то время как слабый принцип Маркова эквивалентен предложению о том, что все функции из полных метрических пространств в метрические пространства сильно экстенсиональны.
