Тезис Чёрча (конструктивная математика)
Аксиома

В конструктивной математике тезис Чёрча — это принцип, утверждающий, что все полные функции являются вычислимыми функциями . С Т {\displaystyle {\mathrm {CT}}}

Аналогично названный тезис Чёрча-Тьюринга утверждает, что каждая эффективно вычислимая функция является вычислимой функцией , тем самым сводя первое понятие во второе. сильнее в том смысле, что с ним каждая функция вычислима. Однако конструктивистский принцип также дан в различных теориях и воплощениях как полностью формальная аксиома. Формализации зависят от определения «функции» и «вычислимого» в рассматриваемой теории. Общим контекстом является теория рекурсии , установленная с 1930-х годов. С Т {\displaystyle {\mathrm {CT}}}

Принимая в качестве принципа, тогда для предиката формы семейства утверждений о существовании (например, ниже), которое, как доказано, не подтверждается для всех вычислимым образом, контрапозитив аксиомы подразумевает, что это затем не подтверждается никакой полной функцией (т. е. никаким отображением, соответствующим ). Таким образом, это сворачивает возможную область действия понятия функции по сравнению с базовой теорией, ограничивая ее определенным понятием вычислимой функции . В свою очередь, аксиома несовместима с системами, которые подтверждают ассоциации и оценки полного функционального значения, которые также, как доказано, не вычислимы. Более конкретно, это влияет на исчисление доказательств таким образом, что делает доказуемыми отрицания некоторых общих классически доказуемых предложений. С Т {\displaystyle {\mathrm {CT}}} ∃ ! у . φ ( х , у ) {\displaystyle \exists !y.\varphi (x,y)} х {\displaystyle x} х ↦ у {\displaystyle x\mapsto y}

Например, арифметика Пеано является такой системой. Вместо нее можно рассмотреть конструктивную теорию арифметики Гейтинга с тезисом в его формулировке первого порядка как дополнительную аксиому, касающуюся ассоциаций между натуральными числами. Эта теория опровергает некоторые универсально замкнутые варианты примеров принципа исключенного третьего . Именно таким образом аксиома показывается несовместимой с . Однако равносогласована с обоими , а также с теорией, заданной плюсом . То есть добавление либо закона исключенного третьего, либо тезиса Чёрча не делает арифметику Гейтинга противоречивой, но добавление обоих делает. П А {\displaystyle {\mathsf {PA}}} ЧАС А {\displaystyle {\mathsf {ХА}}} С Т 0 {\displaystyle {\mathrm {CT} }_{0}} П А {\displaystyle {\mathsf {PA}}} ЧАС А {\displaystyle {\mathsf {ХА}}} П А {\displaystyle {\mathsf {PA}}} ЧАС А {\displaystyle {\mathsf {ХА}}} С Т 0 {\displaystyle {\mathrm {CT} }_{0}}

Официальное заявление

Этот принцип имеет формализации в различных математических рамках. Пусть обозначает предикат T Клини , так что например, действительность предиката выражает , что является индексом полной вычислимой функции. Обратите внимание, что существуют также вариации на и извлечение значения , как функции с возвращаемыми значениями. Здесь они выражаются как примитивные рекурсивные предикаты. Запишите для сокращения , так как значения играют роль в формулировках принципа. Таким образом, вычислимая функция с индексом завершается на со значением тогда и только тогда . Этот -предикат на тройках может быть выражен как , ценой введения сокращенной нотации, включающей знак, уже используемый для арифметического равенства. В теориях первого порядка, таких как , которые не могут количественно определять отношения и функции напрямую, может быть сформулирован как схема аксиом, говорящая, что для любого определяемого полного отношения, которое включает в себя семейство действительных утверждений о существовании , последние вычислимы в смысле . Для каждой формулы из двух переменных схема включает аксиому Т 1 {\displaystyle T_{1}} ∀ х ∃ ж Т 1 ( е , х , ж ) {\displaystyle \forall x\,\exists w\,T_{1}(e,x,w)} е {\displaystyle е} Т 1 {\displaystyle T_{1}} У {\displaystyle U} Т У ( е , х , ж , у ) {\displaystyle TU(e,x,w,y)} Т 1 ( е , х , ж ) ∧ У ( ж , у ) {\displaystyle T_{1}(e,x,w)\land U(w,y)} у {\displaystyle у} е {\displaystyle е} х {\displaystyle x} у {\displaystyle у} ∃ ж Т У ( е , х , ж , у ) {\displaystyle \exists w\,TU(e,x,w,y)} Σ 1 0 {\displaystyle \Sigma _{1}^{0}} е , х , у {\displaystyle e,x,y} { е } ( х ) = у {\displaystyle \{e\}(x)=y} ЧАС А {\displaystyle {\mathsf {ХА}}} С Т {\displaystyle {\mathrm {CT}}} ∃ у {\displaystyle \exists y} Т У {\displaystyle TU} φ ( х , у ) {\displaystyle \varphi (x,y)} С Т 0 {\displaystyle {\mathrm {CT} }_{0}}

( ∀ х ∃ у φ ( х , у ) ) → ∃ е ( ∀ х ∃ у ∃ ж Т У ( е , х , ж , у ) ∧ φ ( х , у ) ) {\displaystyle {\big (}\forall x\;\exists y\;\varphi (x,y){\big )}\;\to \;\exists e\,{\big (}\forall x\;\exists y\;\exists w\;TU(e,x,w,y)\wedge \varphi (x,y){\big )}}

Другими словами: если для каждого существует удовлетворяющее , то на самом деле существует , которое является числом Гёделя частично рекурсивной функции , которая для каждого даст такое удовлетворяющее формуле - и при этом некоторое является числом Гёделя, кодирующим проверяемое вычисление, свидетельствующее о том, что на самом деле является значением этой функции при . х {\displaystyle x} у {\displaystyle у} φ {\displaystyle \varphi} е {\displaystyle е} х {\displaystyle x} у {\displaystyle у} ж {\displaystyle w} у {\displaystyle у} х {\displaystyle x}

Соответственно, импликации этой формы могут быть установлены как конструктивные метатеоретические свойства теорий. То есть теория не обязательно должна доказывать импликацию (формулу с ), но существование металогически подтверждается. Тогда говорят, что теория закрыта относительно правила. → {\displaystyle \to} е {\displaystyle е}

Варианты

Расширенный тезис Чёрча

Утверждение расширяет требование на отношения, которые определены и являются общими для определенного типа домена. Это может быть достигнуто путем сужения сферы действия универсального квантификатора и, таким образом, может быть формально установлено схемой: Э С Т 0 {\displaystyle {\mathrm {ECT_{0}} }}

( ∀ х ψ ( х ) → ∃ у φ ( х , у ) ) → ∃ е ( ∀ х ψ ( х ) → ∃ у ∃ ж Т У ( е , х , ж , у ) ∧ φ ( х , у ) ) {\displaystyle {\big (}\forall x\;\psi (x)\to \exists y\;\varphi (x,y){\big )}\;\to \;\exists e\,{\big (}\forall x\;\psi (x)\to \exists y\;\exists w\;TU(e,x,w,y)\wedge \varphi (x,y){\big )}}

В приведенном выше примере ограничено до почти отрицательного . Для арифметики первого порядка (где схема обозначена ) это означает, что не может содержать никакой дизъюнкции , а кванторы существования могут появляться только перед (разрешимыми) формулами. При наличии принципа Маркова синтаксические ограничения могут быть несколько ослаблены. [1] ψ {\displaystyle \пси} Э С Т 0 {\displaystyle {\mathrm {ECT_{0}} }} ψ {\displaystyle \пси} Δ 0 0 {\displaystyle \Delta _{0}^{0}} М П {\displaystyle {\mathrm {MP}}}

При рассмотрении области всех чисел (например, принимая за тривиальное ) вышеизложенное сводится к предыдущей форме тезиса Чёрча. ψ ( х ) {\displaystyle \пси (x)} х = х {\displaystyle х=х}

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

Расширенный тезис Чёрча используется школой конструктивной математики, основанной Андреем Марковым .

Функциональное помещение

С Т 0 ! {\displaystyle {\mathrm {CT} }_{0}!} обозначает более слабый вариант принципа, в котором предпосылка требует единственного существования ( ), т.е. возвращаемое значение уже должно быть определено. у {\displaystyle у}

Формулировка более высокого порядка

Первая формулировка тезиса выше также называется арифметической формой принципа, поскольку в ее формулировке появляется только квантор по числам. Она использует общее отношение в своем антецеденте. В такой структуре, как теория рекурсии, функции могут быть представлены как функциональное отношение, предоставляя уникальное выходное значение для каждого входа. φ {\displaystyle \varphi}

В системах более высокого порядка, которые могут количественно определять (общие) функции напрямую, форма может быть сформулирована как одна аксиома, утверждающая, что каждая функция от натуральных чисел до натуральных чисел вычислима. В терминах примитивных рекурсивных предикатов, С Т {\displaystyle {\mathrm {CT}}}

∀ ф ∃ е ( ∀ х ∃ ж Т У ( е , х , ж , ф ( х ) ) ) {\displaystyle \forall f\;\exists e\,{\big (}\forall x\;\exists w\;TU(e,x,w,f(x)){\big )}}

Это постулирует, что все функции вычислимы, в смысле Клини, с индексом в теории. Таким образом, таковы все значения . Можно написать с обозначающим экстенсиональное равенство . ф {\displaystyle f} е {\displaystyle е} у = ф ( х ) {\displaystyle y=f(x)} ∀ ф ∃ е ф ≅ { е } {\displaystyle \forall f\;\exists e\,f\cong \{e\}} ф ≅ г {\displaystyle f\cong g} ∀ х . ф ( х ) = г ( х ) {\displaystyle \forall xf(x)=g(x)}

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

Принцип можно рассматривать как идентификацию пространства с набором полных рекурсивных функций. В топологии реализуемости этот экспоненциальный объект объекта натуральных чисел также можно идентифицировать с менее ограничивающими наборами карт. Н Н {\displaystyle {\mathbb {N} }^{\mathbb {N} }}

Более слабые заявления

Существуют и более слабые формы тезиса, называемые по-разному . Вт С Т {\displaystyle {\mathrm {WCT} }}

Вставляя двойное отрицание перед утверждением о существовании индекса в версии более высокого порядка, утверждается, что нерекурсивных функций не существует. Это все еще ограничивает пространство функций, не составляя аксиому выбора функции.

Связанное утверждение состоит в том, что любое разрешимое подмножество натуральных чисел не может быть исключено как вычислимое в том смысле, что

( ∀ х   χ ( х ) ∨ ¬ χ ( х ) ) → ¬ ¬ ∃ е ( ∀ х ( ∃ ж Т 1 ( е , х , ж ) ) ↔ χ ( х ) ) {\displaystyle {\big (}\forall x\ \chi (x)\lor \neg \chi (x){\big )}\;\to \;\neg \neg \exists e\,{\big (}\forall x\,{\big (}\exists w\;T_{1}(e,x,w){\big )}\leftrightarrow \chi (x){\big )}}

Контрапозитив этого делает любой невычислимый предикат нарушением исключенного третьего, так что это все еще в целом антиклассично. В отличие от , как принцип это совместимо с формулировками теоремы веера . С Т 0 {\displaystyle \mathrm {CT} _{0}}

Могут быть определены варианты для связанных предпосылок . Например, принцип, всегда допускающий существование полной рекурсивной функции в некотором дискретном двоичном наборе, который подтверждает один из дизъюнктов. Без двойного отрицания это может быть обозначено . ∀ х   ψ л е ф т ( х ) ∨ ψ г я г час т ( х ) {\displaystyle \forall x\ \psi _{\mathrm {left} }(x)\lor \psi _{\mathrm {right} }(x)} Н → { л е ф т , г я г час т } {\displaystyle {\mathbb {N} }\to \{\mathrm {слева},\mathrm {справа} \}} С Т 0 ∨ {\displaystyle \mathrm {CT} _{0}^{\lor }}

Связь с классической логикой

Схема , добавленная к конструктивным системам, таким как , подразумевает отрицание универсально квантифицированной версии закона исключенного третьего для некоторых предикатов. Например, проблема остановки , как доказано, невычислимо разрешима , но, предполагая классическую логику, что тавтология заключается в том, что каждая машина Тьюринга либо останавливается, либо не останавливается на заданном входе. Далее, предполагая тезис Чёрча, в свою очередь, заключаем, что это вычислимо — противоречие. Немного подробнее: в достаточно сильных системах, таких как , можно выразить отношение, связанное с вопросом об остановке, связывая любой код из перечисления машин Тьюринга и значения из . Предполагая классическую тавтологию выше, это отношение может быть доказано полным, т. е. оно представляет собой функцию, которая возвращает, если машина останавливается и если она не останавливается. Но plus опровергает это следствие закона исключенного третьего, например. С Т 0 {\displaystyle {\mathrm {CT} }_{0}} ЧАС А {\displaystyle {\mathsf {ХА}}} ЧАС А {\displaystyle {\mathsf {ХА}}} час {\displaystyle ч} { 0 , 1 } {\displaystyle \{0,1\}} 1 {\displaystyle 1} 0 {\displaystyle 0} ЧАС А {\displaystyle {\mathsf {ХА}}} С Т 0 {\displaystyle {\mathrm {CT} }_{0}}

Принцип также отвергает такие принципы, как сдвиг двойного отрицания (коммутативность всеобщей квантификации с двойным отрицанием).

Форма с одной аксиомой с вышеприведенным согласуется с некоторыми слабыми классическими системами, которые не обладают силой для формирования функций, таких как функция предыдущего абзаца. Например, классическая слабая арифметика второго порядка согласуется с этой единственной аксиомой, поскольку имеет модель, в которой каждая функция вычислима. Однако форма с одной аксиомой становится несовместимой с исключенным третьим в любой системе, которая имеет аксиомы, достаточные для доказательства существования функций, таких как функция . Например, принятие вариантов счетного выбора , таких как уникальный выбор для числовых квантификаторов, С Т {\displaystyle {\mathrm {CT}}} ∀ ф {\displaystyle \forall f} Р С А 0 {\displaystyle {\mathsf {RCA_{0}}}} Р С А 0 {\displaystyle {\mathsf {RCA_{0}}}} час {\displaystyle ч}

∀ н ∃ ! м ϕ ( н , м ) → ∃ а ∀ к ϕ ( к , а к ) , {\displaystyle \forall n\;\exists !m\;\phi (n,m)\to \exists a\;\forall k\;\phi (k,a_{k}),}

где обозначает последовательность, портят эту согласованность. а {\displaystyle а}

Формулировка первого порядка уже включает в себя силу такого принципа понимания функций посредством перечисляемых функций. С Т 0 {\displaystyle {\mathrm {CT} }_{0}}

Конструктивно сформулированные подтеории обычно можно показать закрытыми в соответствии с правилом Церкви, и соответствующий принцип, таким образом, совместим. Но как следствие ( ) это не может быть доказано такими теориями, поскольку это сделало бы более сильную классическую теорию непоследовательной. З Ф {\displaystyle {\mathsf {ZF}}} → {\displaystyle \to}

Реализаторы и металогика

Этот тезис выше можно охарактеризовать как утверждение, что предложение истинно, если оно вычислимо реализуемо . Это отражено в следующих метатеоретических эквивалентностях: [2]

ЧАС А + Э С Т 0 ⊢ φ ↔ ∃ н ( н ⊩ φ ) {\displaystyle {\mathsf {HA}}+{\mathrm {ECT_{0}} }\vdash \varphi \leftrightarrow \exists n\, (n\Vdash \varphi)}

и

ЧАС А + Э С Т 0 ⊢ φ ⟺ ЧАС А ⊢ ∃ н ( н ⊩ φ ) {\displaystyle {\mathsf {HA}}+{\mathrm {ECT_{0}} }\vdash \varphi \;\iff \;{\mathsf {HA}}\vdash \exists n\,(n\Vdash \varphi )}

Здесь " " — это просто эквивалентность в арифметической теории, тогда как " " обозначает метатеоретическую эквивалентность. Для заданного предикат читается как " ". На словах первый результат выше утверждает, что доказуемо в plus , что предложение истинно, если и только если оно реализуемо. Но также второй результат выше утверждает, что доказуемо в plus, если и только если доказуемо реализуемо в just . ↔ {\displaystyle \leftrightarrow } ⟺ {\displaystyle \iff } φ {\displaystyle \varphi } n ⊩ φ {\displaystyle n\Vdash \varphi } n  realises  φ {\displaystyle n{\text{ realises }}\varphi } H A {\displaystyle {\mathsf {HA}}} E C T 0 {\displaystyle {\mathrm {ECT_{0}} }} φ {\displaystyle \varphi } H A {\displaystyle {\mathsf {HA}}} E C T 0 {\displaystyle {\mathrm {ECT_{0}} }} φ {\displaystyle \varphi } H A {\displaystyle {\mathsf {HA}}}

Для следующей металогической теоремы напомним, что она неконструктивна и не имеет свойства существования , тогда как арифметика Гейтинга его демонстрирует: P A {\displaystyle {\mathsf {PA}}}

H A ⊢ ∃ n . ϕ ( n ) ⟹ exists n   H A ⊢ ϕ ( n _ ) {\displaystyle {\mathsf {HA}}\vdash \exists n.\phi (n)\implies {\text{exists}}\;{\mathrm {n} }\ {\mathsf {HA}}\vdash \phi ({\underline {\mathrm {n} }})}

Второе приведенное выше равенство можно расширить следующим образом: M P {\displaystyle {\mathrm {MP} }}

H A + E C T 0 + M P ⊢ φ ⟺ exists n   P A ⊢ ( n _ ⊩ φ ) {\displaystyle {\mathsf {HA}}+{\mathrm {ECT_{0}} }+{\mathrm {MP} }\vdash \varphi \;\iff \;{\text{exists}}\;{\mathrm {n} }\ {\mathsf {PA}}\vdash ({\underline {\mathrm {n} }}\Vdash \varphi )}

В этом случае квантификатор существования должен быть снаружи . На словах, доказуемо в плюсе, а также тогда и только тогда, когда можно метатеоретически установить, что существует некоторое число , такое что соответствующее стандартное число в , обозначенное , доказуемо реализует . Предполагая вместе с альтернативными вариантами тезиса Чёрча, было получено больше таких металогических утверждений о существовании. P A {\displaystyle {\mathsf {PA}}} φ {\displaystyle \varphi } H A {\displaystyle {\mathsf {HA}}} E C T 0 {\displaystyle {\mathrm {ECT_{0}} }} M P {\displaystyle {\mathrm {MP} }} n {\displaystyle {\mathrm {n} }} P A {\displaystyle {\mathsf {PA}}} n _ {\displaystyle {\underline {\mathrm {n} }}} φ {\displaystyle \varphi } M P {\displaystyle {\mathrm {MP} }}

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

Ссылки

  1. ^ Троелстра, А.С., ван Дален Д., Конструктивизм в математике: введение 1 ; Исследования по логике и основаниям математики; Springer, 1988; стр. 206
  2. ^ Троелстра, А.С. Метаматематическое исследование интуиционистской арифметики и анализа . Том 344 Lecture Notes in Mathematics; Springer, 1973
Retrieved from "https://en.wikipedia.org/w/index.php?title=Church%27s_thesis_(constructive_mathematics)&oldid=1220047003"