Диссертация Чёрча (конструктивная математика)

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

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

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

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

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

Этот принцип имеет формализации в различных математических рамках. Позволять $T_{1}$ обозначим предикат T Клини , так что, например, достоверность предиката $\forall x\,\exists w\,T_{1}(e,x,w)$ выражает это $e$ — индекс полной вычислимой функции. Обратите внимание, что существуют также варианты $T_{1}$ и извлечение ценности $U$, как функции с возвращаемыми значениями. Здесь они выражаются как примитивно-рекурсивные предикаты. Писать $TU(e,x,w,y)$ сокращать $T_{1}(e,x,w)\land U(w,y)$, поскольку значения $y$ играет роль в формулировках принципа. Итак, вычислимая функция с индексом $e$ заканчивается $x$ со стоимостью $y$ если только $\exists w\,TU(e,x,w,y)$. Этот $\Sigma _{1}^{0}$-предикат тройки $e,x,y$ может быть выражено $\{e\}(x)=y$, за счет введения сокращенной записи с использованием знака, уже используемого для арифметического равенства. В теориях первого порядка, таких как ${\mathsf {HA}}$, которые не могут количественно определять отношения и функционировать напрямую, ${\mathrm {CT} }$ может быть сформулировано как схема аксиом, утверждающая, что для любого определимого тотального отношения, которое включает в себя семейство действительных утверждений о существовании $\exists y$, последние вычислимы в смысле $TU$. Для каждой формулы $\varphi (x,y)$ двух переменных, схема ${\mathrm {CT} }_{0}$ включает в себя аксиому

${\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 )}$

Словами: Если для каждого $x$ есть $y$ удовлетворяющий $\varphi$, то на самом деле существует $e$ это число Гёделя , частично рекурсивной функции которая для каждого $x$, изготовить такой $y$ удовлетворяющие формуле - и с некоторыми $w$ являющееся числом Гёделя, кодирующим проверяемое вычисление, свидетельствующее о том, что $y$ на самом деле является значением этой функции в $x$.

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

Варианты

Расширенная диссертация Чёрча

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

${\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 )}$

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

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

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

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

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

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

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

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

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

$\forall f\;\exists e\,{\big (}\forall x\;\exists w\;TU(e,x,w,f(x)){\big )}$

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

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

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

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

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

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

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

${\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 )}$

Противоположность этому приводит к тому, что любой невычислимый предикат нарушает исключенное среднее, так что в целом это по-прежнему является антиклассическим. В отличие от $\mathrm {CT} _{0}$, в принципе это совместимо с формулировками теоремы веера .

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

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

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

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

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

$\forall n\;\exists !m\;\phi (n,m)\to \exists a\;\forall k\;\phi (k,a_{k}),$

где $a$ обозначает последовательность, портит эту последовательность.

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

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

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

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

${\mathsf {HA}}+{\mathrm {ECT_{0}} }\vdash \varphi \leftrightarrow \exists n\,(n\Vdash \varphi )$

и

${\mathsf {HA}}+{\mathrm {ECT_{0}} }\vdash \varphi \;\iff \;{\mathsf {HA}}\vdash \exists n\,(n\Vdash \varphi )$

Здесь " $\leftrightarrow$" является просто эквивалентностью в теории арифметики, тогда как " $\iff$«обозначает метатеоретическую эквивалентность. Для данного $\varphi$, предикат $n\Vdash \varphi$ читается как " $n{\text{ realises }}\varphi$". На словах первый результат выше утверждает, что он доказуем в ${\mathsf {HA}}$ плюс ${\mathrm {ECT_{0}} }$ что предложение истинно тогда и только тогда, когда оно реализуемо. Но также второй результат выше утверждает, что $\varphi$ доказуемо в ${\mathsf {HA}}$ плюс ${\mathrm {ECT_{0}} }$ если только $\varphi$ доказуемо реализуемо всего за ${\mathsf {HA}}$.

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

${\mathsf {HA}}\vdash \exists n.\phi (n)\implies {\text{exists}}\;{\mathrm {n} }\ {\mathsf {HA}}\vdash \phi ({\underline {\mathrm {n} }})$

Вторая эквивалентность, приведенная выше, может быть расширена с помощью ${\mathrm {MP} }$ следующее:

${\mathsf {HA}}+{\mathrm {ECT_{0}} }+{\mathrm {MP} }\vdash \varphi \;\iff \;{\text{exists}}\;{\mathrm {n} }\ {\mathsf {PA}}\vdash ({\underline {\mathrm {n} }}\Vdash \varphi )$

Квантор существования должен быть снаружи. ${\mathsf {PA}}$ в этом случае. Другими словами, $\varphi$ доказуемо в ${\mathsf {HA}}$ плюс ${\mathrm {ECT_{0}} }$ а также ${\mathrm {MP} }$ тогда и только тогда, когда можно метатеоретически установить, что существует некоторое число ${\mathrm {n} }$ такой, что соответствующая стандартная цифра в ${\mathsf {PA}}$, обозначенный ${\underline {\mathrm {n} }}$, доказуемо осознает $\varphi$. Предполагая ${\mathrm {MP} }$ Вместе с альтернативными вариантами тезиса Чёрча было получено больше таких металогических утверждений о существовании.

См. также

• Вычислимая функция
• Свойства дизъюнкции и существования
• Реализуемость

Ссылки

• Эллиот Мендельсон (1990) «Переосмысление тезиса Чёрча и математических доказательств», Journal of Philosophy 87 (5): 225–233.