Принцип Маркова , названный в честь Андрея Маркова-младшего , является условным утверждением существования, для которого существует множество эквивалентных формулировок, как обсуждается ниже.
Принцип логической достоверности классически, но не в интуиционистской конструктивной математике. Тем не менее, многие частные примеры этого можно доказать и в конструктивном контексте.
История
Этот принцип был впервые изучен и принят русской школой конструктивизма вместе с принципами выбора и часто с точки зрения реализуемости понятия математической функции.
В теории вычислимости
На языке теории вычислимости принцип Маркова - это формальное выражение утверждения о том, что если невозможно, чтобы алгоритм не завершился, то он завершится. Это эквивалентно утверждению, что если набор и его дополнение вычислимо перечислимы , то набор разрешим .
В интуиционистской логике
В логике предикатов предикат P над некоторой областью называется разрешимым, если для каждого x в области либо P ( x ) истинно, либо P ( x ) не истинно. Конструктивно это не так тривиально.
Тогда для разрешимого предиката P над натуральными числами принцип Маркова гласит:
То есть, если P не может быть ложным для всех натуральных чисел n , то это верно для некоторого n .
Правило маркова
Правило Маркова - это, как правило, формулировка принципа Маркова. В нем говорится, что выводится, как только для разрешимый. Формально,
Анне Трельстра [1] доказала, что это допустимое правило в арифметике Гейтинга . Позже логик Харви Фридман показал, что правило Маркова является допустимым правилом во всей интуиционистской логике , арифметике Гейтинга и различных других интуиционистских теориях [2], используя перевод Фридмана .
В арифметике Гейтинга
На языке арифметики это эквивалентно :
для общая рекурсивная функция от натуральных чисел.
Реализуемость
Если конструктивную арифметику перевести с помощью реализуемости в классическую метатеорию, которая доказывает-согласованность соответствующей классической теории (например, арифметики Пеано, если мы изучаем арифметику Гейтинга ), то принцип Маркова оправдан: реализатор - это постоянная функция, которая принимает реализацию, котораяне везде ложно для неограниченного поиска, который последовательно проверяет,правда. Если не везде ложно, то по -согласованность должен быть срок, на который выполняется, и в конечном итоге поиск будет проверен каждым термином. Однако еслинигде не выполняется, то область определения функции-константы должна быть пустой, поэтому, хотя поиск не останавливается, он по-прежнему бессмысленно утверждает, что функция является реализатором. По закону исключенного среднего (в нашей классической метатеории) должен либо нигде не удерживаться, либо не удерживаться нигде, поэтому эта постоянная функция является реализатором.
Если вместо этого в конструктивной мета-теории используется интерпретация реализуемости, то это не оправдано. Действительно, для арифметики первого порядка принцип Маркова точно отражает разницу между конструктивной и классической мета-теорией. В частности, утверждение доказуемо в арифметике Гейтинга с помощью тезиса Расширенного Черча тогда и только тогда, когда существует число, которое доказуемо реализует его в арифметике Гейтинга ; и это доказуемо в арифметике Гейтинга с помощью расширенного тезиса Чёрча и принципа Маркова тогда и только тогда, когда существует число, которое доказуемо реализует его в арифметике Пеано .
В конструктивном анализе
На языке реального анализа это эквивалентно следующим принципам:
- Для каждого действительного числа x , если противоречие, что x равно 0, то существует y ∈ Q такой, что 0 < y <| x |, часто выражающийся в том, что x отделен от 0 или конструктивно не равен ему .
- Для каждого действительного числа x , если противоречие, что x равно 0, то существует y ∈ R такой, что xy = 1.
Модифицированная реализуемость не оправдывает принцип Маркова, даже если в метатеории используется классическая логика: в языке просто типизированного лямбда-исчисления нет реализатора, поскольку этот язык не является полным по Тьюрингу и в нем нельзя определять произвольные циклы.
Принцип слабого Маркова
Принцип Слабого Маркова представляет собой более слабую форму принципа Маркова, который можно сформулировать на языке анализа как
Это условное утверждение о разрешимости положительности действительного числа.
Эта форма может быть оправдана принципами непрерывности Брауэра , тогда как более сильная форма им противоречит. Таким образом, он может быть выведен из интуиционистских, реализуемых и классических рассуждений, в каждом случае по разным причинам, но этот принцип недействителен в общем конструктивном смысле Бишопа. [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.