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

Принцип Маркова (также известный как Ленинградский принцип). ^{[ 1 ]}), названный в честь Андрея Маркова-младшего , представляет собой условное утверждение существования, для которого существует множество эквивалентных формулировок, как обсуждается ниже. Этот принцип логически обоснован в классической , но не в интуиционистской конструктивной математике. Однако многие частные случаи этого тем не менее доказуемы и в конструктивном контексте.

История

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

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

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

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

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

Принцип Маркова тогда гласит: для разрешимого предиката P над натуральными числами , если P не может быть ложным для всех натуральных чисел n , то он истинен для некоторого n . Написано с использованием кванторов :

{\Big (}\forall n{\big (}P(n)\vee \neg P(n){\big )}\wedge \neg \forall n\,\neg P(n){\Big )}\rightarrow \exists n\,P(n)

правило Маркова

Правило Маркова — это формулировка принципа Маркова как правила. В нем говорится, что $\exists n\;P(n)$ выводится, как только $\neg \neg \exists n\;P(n)$ это для $P$ разрешимо. Формально,

\forall n{\big (}P(n)\lor \neg P(n){\big )},\ \neg \neg \exists n\;P(n)\ \ \vdash \ \ \exists n\;P(n)

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

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

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

\neg \neg \exists n\;f(n)=0\rightarrow \exists n\;f(n)=0

для $f$ полная рекурсивная функция натуральных чисел.

При наличии тезиса Чёрча этот принцип эквивалентен своей форме для примитивно-рекурсивных функций . Используя предикат T Клини , последний можно выразить как

\forall e\;\forall x\;{\big (}\neg \neg \exists w\;T_{1}(e,x,w)\rightarrow \exists w\;T_{1}(e,x,w){\big )}

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

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

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

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

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

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

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

Слабый принцип Маркова

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

\forall (x\in \mathbb {R} )\,{\Big (}\forall (y\in \mathbb {R} ){\big (}\neg \neg (0<y)\lor \neg \neg (y<x){\big )}{\Big )}\,\to \,(0<x).

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

Чтобы понять, в чем заключается этот принцип, полезно рассмотреть более сильное утверждение. Следующее выражает, что любое действительное число $x$ , такой, что нет неположительных $y$ не ниже него, положительно:

\nexists (y\leq 0)\,x\leq y\,\to \,(0<x),

где $x\leq y$ означает отрицание $y<x$ . Это более сильный импликация, поскольку антецедент более свободен. Обратите внимание, что здесь логически положительное утверждение выводится из логически отрицательного. Это подразумевается слабым принципом Маркова при повышении закона Де Моргана для $\neg A\lor \neg B$ к эквивалентности.

Если предположить классическое исключение двойного отрицания, слабый принцип Маркова становится тривиальным, выражая, что число, большее, чем все неположительные числа, является положительным.

Расширение функций

Функция $f:X\to Y$ между метрическими пространствами называется сильно экстенсиональным, если $d(f(x),f(y))>0$ подразумевает $d(x,y)>0$ , что классически является просто противоположностью функции, сохраняющей равенство. Можно показать, что принцип Маркова эквивалентен утверждению, что все функции между произвольными метрическими пространствами сильно экстенсиональны, в то время как слабый принцип Маркова эквивалентен утверждению, что все функции из полных метрических пространств в метрические пространства сильно экстенсиональны.

См. также

Ссылки

^ Маргенштерн, Морис (1995). «Конструктивная школа Маркова» . Журнал истории математики . 1 (2): 271–305 . Проверено 27 марта 2024 г.
^ Энн С. Троэльстра. Метаматематическое исследование интуиционистской арифметики и анализа, Springer Verlag (1973), теорема 4.2.4, 2-е издание.
^ Харви Фридман. Классически и интуиционистски доказуемо рекурсивные функции. Скотт, Д.С. и Мюллер, редакторы GH, Теория высших множеств, том 699 конспектов лекций по математике, Springer Verlag (1978), стр. 21–28.
^ Ульрих Коленбах , « О слабом принципе Маркова ». Mathematical Logic Quarterly (2002), том 48, выпуск S1, стр. 59–65.

Внешние ссылки

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

[MarkovSchool-1] Маргенштерн, Морис (1995). «Конструктивная школа Маркова» . Журнал истории математики . 1 (2): 271–305 . Проверено 27 марта 2024 г.

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

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

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

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]