Конструктивная теория множеств

Аксиоматическая конструктивная теория множеств — это подход к математическому конструктивизму, следующий программе аксиоматической теории множеств . Тот же язык первого порядка с " $=$" и " $\in$Обычно используется классическая теория множеств, поэтому ее не следует путать с подходом конструктивных типов . С другой стороны, некоторые конструктивные теории действительно мотивированы своей интерпретируемостью в теориях типов .

Помимо отказа от принципа исключенного третьего ( ${\mathrm {PEM} }$), конструктивные теории множеств часто требуют, чтобы некоторые логические кванторы в их аксиомах были ограниченными , мотивированные результатами, связанными с непредикативностью .

Введение

Конструктивный взгляд

об использовании интуиционистской

Логика обсуждаемых здесь теорий множеств конструктивна в том смысле, что она отвергает принцип исключенного среднего. ${\mathrm {PEM} }$, т.е. что дизъюнкция $\phi \lor \neg \phi$ автоматически выполняется для всех предложений $\phi$. Как правило, для доказательства исключенного третьего в предложении $P$, т.е. доказать частную дизъюнкцию $P\lor \neg P$, или $P$ или $\neg P$необходимо явно доказать. Когда любое из таких доказательств установлено, говорят, что предложение разрешимо, и тогда это логически подразумевает, что дизъюнкция имеет место. Аналогично и чаще всего предикат $Q(x)$ для $x$ в домене $X$ называется разрешимым, если более сложное утверждение $\forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )}$доказуемо. Неконструктивные аксиомы могут позволить получить доказательства, формально претендующие на разрешимость таких аксиом. $P$ (и/или $Q$) в том смысле, что они оказываются исключенными средними для $P$(соответственно утверждение с использованием приведенного выше квантора) без демонстрации истинности какой-либо стороны дизъюнкции. Это часто бывает в классической логике. Напротив, аксиоматические теории, считающиеся конструктивными, как правило, не допускают многих классических доказательств утверждений, включающих свойства, которые, как доказано, неразрешимы с помощью вычислений .

Закон непротиворечия представляет собой частный случай пропозициональной формы modus ponens . Использование первого с любым отрицательным утверждением $\neg P$, один действительный закон Де Моргана, таким образом, подразумевает $\neg \neg (P\lor \neg P)$уже в более консервативной минимальной логике . На словах интуиционистская логика по-прежнему утверждает: невозможно одновременно исключить предложение и исключить его отрицание, и, таким образом, отказ от любого конкретизированного исключенного среднего утверждения для отдельного предложения непоследовательен. Здесь двойное отрицание означает, что утверждение о дизъюнкции теперь уже доказано никогда не может быть исключено или отвергнуто, даже в тех случаях, когда дизъюнкция не может быть доказуема (например, путем демонстрации одного из дизъюнктов, тем самым решая $P$) из принятых аксиом.

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

Интуиционистская логика, лежащая в основе обсуждаемых здесь теорий множеств, в отличие от минимальной логики, по-прежнему допускает устранение двойного отрицания для отдельных предложений. $P$для которого исключено среднее. В свою очередь, формулировки теорем относительно конечных объектов, как правило, не отличаются от своих классических аналогов. Учитывая модель всех натуральных чисел, эквивалент предикатов, а именно принцип Маркова , не выполняется автоматически, но может рассматриваться как дополнительный принцип.

В обитаемой области и при помощи взрыва дизъюнкция $P\lor \exists (x\in X).\neg Q(x)$ подразумевает утверждение о существовании $\exists (x\in X).(Q(x)\to P)$, что, в свою очередь, подразумевает ${\big (}\forall (x\in X).Q(x){\big )}\to P$. Классически эти последствия всегда обратимы. Если одно из первых является классически справедливым, возможно, стоит попытаться обосновать его во второй форме. Для особого случая, когда $P$ отвергается, мы имеем дело с утверждением о существовании контрпримера $\exists (x\in X).\neg Q(x)$, что обычно конструктивно сильнее, чем заявление об отказе $\neg \forall (x\in X).Q(x)$: Пример $t$ такой, что $Q(t)$ противоречиво, конечно, означает, что это не тот случай, что $Q$ держится для всех возможных $x$. Но можно также продемонстрировать, что $Q$ держась за всех $x$логически привело бы к противоречию без помощи конкретного контрпримера, да еще и при невозможности его построить. В последнем случае конструктивно здесь не оговаривается утверждение существования.

Налагаемые ограничения на теорию множеств

По сравнению с классическим аналогом, здесь обычно меньше шансов доказать существование отношений, которые невозможно реализовать. Ограничение на конструктивное прочтение априорного существования приводит к ужесточению требований относительно того, какие характеристики множества $f\subset X\times Y$включающие неограниченные коллекции, составляют (математическую и, следовательно, всегда означающую общую ) функцию. Часто это происходит потому, что предикат в предполагаемом определении по регистру может оказаться неразрешимым. Принимая стандартное определение равенства множеств через экстенсиональность, полная Аксиома выбора представляет собой такой неконструктивный принцип, который подразумевает ${\mathrm {PEM} }$для формул, разрешенных в принятой схеме разделения, по теореме Диаконеску . Аналогичные результаты верны и для утверждения о существовании аксиомы регулярности , как показано ниже. Последний имеет классически эквивалентную индуктивную замену. Таким образом, подлинно интуиционистское развитие теории множеств требует переформулировки некоторых стандартных аксиом в классически эквивалентные. Помимо требований вычислимости и оговорок, снижающих степень непредикативности, Технический вопрос относительно того, какие нелогические аксиомы эффективно расширяют основную логику теории, также является самостоятельным предметом исследования.

Metalogic

уже возникают вычислимо неразрешимые предложения Поскольку в арифметике Робинсона , даже простое предикативное разделение позволяет легко определять неуловимые подмножества. В отличие от классической концепции, конструктивные теории множеств могут быть замкнуты по правилу, согласно которому любое свойство, разрешимое для всех множеств, уже эквивалентно одному из двух тривиальных: $\top$ или $\bot$. действительную линию можно считать неразложимой Также в этом смысле . Неразрешимость дизъюнкций также влияет на утверждения о полных порядках, таких как порядок всех порядковых числительных , что выражается в доказуемости и отклонении положений в порядке, определяющем дизъюнкцию. $(\alpha \in \beta )\lor (\alpha =\beta )\lor (\beta \in \alpha )$. Это определяет, является ли отношение трихотомическим . Ослабленная теория ординалов, в свою очередь, влияет на силу теории доказательства, определенную в ординальном анализе .

Взамен конструктивные теории множеств могут проявлять привлекательные свойства дизъюнкции и существования , как это известно из изучения конструктивных арифметических теорий. Это особенности фиксированной теории, которые металогически связывают суждения о доказуемых в теории утверждениях. Особенно хорошо изучены те особенности, которые могут быть выражены в арифметике Гейтинга с помощью кванторов над числами и которые часто могут быть реализованы с помощью чисел, как это формализовано в теории доказательств . В частности, это свойство числового существования и тесно связанное с ним дизъюнктивное свойство, а также замкнутость по правилу Чёрча любой заданной функции , свидетельствующая о вычислимости .

Теория множеств не только выражает теоремы о числах, поэтому можно рассмотреть более общее, так называемое сильное свойство существования, которое, как будет обсуждаться, труднее обнаружить. Теория обладает этим свойством, если можно установить следующее: для любого свойства $\phi$, если теория доказывает, что существует множество, обладающее этим свойством, т. е. если теория утверждает утверждение о существовании, то существует также свойство $\psi$который однозначно описывает такой экземпляр набора. Более формально, для любого предиката $\phi$ есть предикат $\psi$ так что

${\mathsf {T}}\vdash \exists x.\phi (x)\implies {\mathsf {T}}\vdash \exists !x.\phi (x)\land \psi (x)$

Роль, аналогичную роли реализованных чисел в арифметике, здесь играют определенные множества, существование которых доказано теорией (или согласно ей). Вопросы, касающиеся силы аксиоматической теории множеств и ее связи с построением терминов, являются тонкими. Хотя многие обсуждаемые теории имеют тенденцию обладать всеми различными числовыми свойствами, свойство существования может быть легко испорчено, как будет обсуждаться далее. Сформулированы более слабые формы свойств существования.

Некоторые теории с классическим пониманием существования на самом деле также могут быть ограничены, чтобы продемонстрировать свойство сильного существования. В теории множеств Цермело–Френкеля, где все множества считаются порядково определяемыми , теория обозначается ${\mathsf {ZF}}+({\mathrm {V} }={\mathrm {OD} })$, множеств без такой определимости не существует. Это свойство также реализуется через постулат конструируемой вселенной в ${\mathsf {ZF}}+({\mathrm {V} }={\mathrm {L} })$. Для контраста рассмотрим теорию ${\mathsf {ZFC}}$ данный ${\mathsf {ZF}}$плюс полный выбора постулат существования : Напомним, что этот набор аксиом доказывает теорему о хорошем порядке , подразумевающую, что хороший порядок существует для любого множества. В частности, это означает, что отношения $W\subset {\mathbb {R} }\times {\mathbb {R} }$ формально существуют, которые устанавливают упорядоченность ${\mathbb {R} }$ (т.е. теория утверждает существование наименьшего элемента для всех подмножеств ${\mathbb {R} }$в отношении этих отношений). И это несмотря на то, что определимость такого упорядочения, как известно, зависит не от ${\mathsf {ZFC}}$. Последнее означает, что ни для какой конкретной формулы $\psi$Говоря языком теории, доказывает ли теория, что соответствующее множество является хорошо упорядоченным отношением действительных чисел. Так ${\mathsf {ZFC}}$ формально доказывает существование подмножества $W\subset {\mathbb {R} }\times {\mathbb {R} }$ обладающий свойством быть вполне упорядоченным отношением, но в то же время не имеющим определенного множества $W$ для которого свойство может быть проверено, возможно, может быть определено.

Антиклассические принципы

Как уже говорилось выше, конструктивная теория ${\mathsf {T}}$ может проявлять свойство числового существования, ${\mathsf {T}}\vdash \exists e.\psi (e)\implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})$, для некоторого числа ${\mathrm {e} }$ и где ${\underline {\mathrm {e} }}$обозначает соответствующую цифру в формальной теории. Здесь необходимо тщательно различать доказуемые импликации между двумя утверждениями: ${\mathsf {T}}\vdash P\to Q$и свойства теории вида ${\mathsf {T}}\vdash P\implies {\mathsf {T}}\vdash Q$. Когда металогически установленная схема последнего типа принимается в качестве правила вывода исчисления доказательств и ничего нового доказать невозможно, говорят, что теория ${\mathsf {T}}$ закрыто по этому правилу.

Вместо этого можно рассматривать присоединение к правилу, соответствующему метатеоретическому свойству, как импликацию (в смысле « $\to$") к ${\mathsf {T}}$в виде схемы аксиом или в количественной форме. Обычно изучается ситуация с фиксированным ${\mathsf {T}}$ демонстрирующее метатеоретическое свойство следующего типа: для примера из некоторого набора формул определенной формы, зафиксированного здесь с помощью $\phi$ и $\psi$, установлено существование ряда ${\mathrm {e} }$ так что ${\mathsf {T}}\vdash \phi \implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})$. Тогда можно постулировать $\phi \to \exists (e\in {\mathbb {N} }).\psi (e)$, где граница $e$— числовая переменная на языке теории. Например, правило Чёрча является допустимым правилом в арифметике Гейтинга первого порядка. ${\mathsf {HA}}$ и, кроме того, соответствующий тезисный принцип Чёрча ${\mathrm {CT} }_{0}$может быть последовательно принята как аксиома. Новая теория с добавленным принципом является антиклассической, поскольку она, возможно, больше не будет последовательной, если принять также ${\mathrm {PEM} }$. Аналогично, присоединение к принципу исключенного третьего ${\mathrm {PEM} }$ к некоторой теории ${\mathsf {T}}$, полученная таким образом теория может доказать новые, строго классические положения, а это может испортить некоторые метатеоретические свойства, ранее установленные для ${\mathsf {T}}$. Таким образом, ${\mathrm {CT} }_{0}$ не может быть принят в ${\mathsf {HA}}+{\mathrm {PEM} }$, также известная как арифметика Пеано ${\mathsf {PA}}$.

В этом подразделе основное внимание будет уделено теориям множеств с количественной оценкой полностью формального понятия бесконечного пространства последовательностей, то есть функционального пространства, как оно будет представлено ниже. Перевод правила Чёрча на язык самой теории можно прочитать здесь:

$\forall (f\in {\mathbb {N} }^{\mathbb {N} }).\exists (e\in {\mathbb {N} }).{\Big (}\forall (n\in {\mathbb {N} }).\exists (w\in {\mathbb {N} }).T(e,n,w)\land U(w,f(n)){\Big )}$

Предикат Клини T вместе с извлечением результата выражает, что любое входное число $n$ отображается в число $f(n)$ есть, через $w$, засвидетельствованное как вычислимое отображение. Здесь ${\mathbb {N} }$ теперь обозначает модель теории множеств стандартных натуральных чисел и $e$— индекс относительно фиксированного перечисления программы. Были использованы более сильные варианты, которые распространяют этот принцип на функции. $f\in {\mathbb {N} }^{X}$ определено в доменах $X\subset {\mathbb {N} }$низкой сложности. Принцип отвергает разрешимость предиката. $Q(e)$ определяется как $\exists (w\in {\mathbb {N} }).T(e,e,w)$, выражая это $e$— индекс вычислимой функции, останавливающейся на собственном индексе. Можно также рассмотреть более слабые формы принципа с двойным отрицанием, которые не требуют существования рекурсивной реализации для каждого $f$, но которые по-прежнему делают несовместимыми принципы, утверждающие существование функций, которые, как доказано, не имеют рекурсивной реализации. Некоторые формы тезиса Чёрча как принципа даже согласуются с классической, слабой, так называемой второго порядка. арифметической теорией ${\mathsf {RCA}}_{0}$, подсистема двусортной теории первого порядка ${\mathsf {Z}}_{2}$.

Совокупность вычислимых функций классически подсчетна , что в классическом смысле то же самое, что быть счетной. Но классические теории множеств обычно утверждают, что ${\mathbb {N} }^{\mathbb {N} }$содержит и другие функции, кроме вычислимых. Например, есть доказательство ${\mathsf {ZF}}$что полные функции (в смысле теории множеств) действительно существуют, которые не могут быть уловлены машиной Тьюринга . Если серьезно отнестись к вычислимому миру как к онтологии, ярким примером антиклассической концепции, связанной с марковской школой, является разрешенная подсчетность различных несчетных коллекций. При принятии счетности совокупности всех бесконечных последовательностей натуральных чисел ( ${\mathbb {N} }^{\mathbb {N} }$) как аксиома в конструктивной теории, «малость» (в классических терминах) этого набора в некоторых теоретических реализациях уже фиксируется самой теорией. Конструктивная теория может также не принимать ни классических, ни антиклассических аксиом и, таким образом, оставаться агностиком в отношении любой возможности.

Конструктивные принципы уже доказывают $\forall (x\in X).\neg \neg {\big (}Q(x)\lor \neg Q(x){\big )}$ для любого $Q$. И так для любого данного элемента $x$ из $X$, то соответствующее исключенное среднее высказывание предложения не может быть отвергнуто. Действительно, для любого данного $x$, по непротиворечивости нельзя исключить $Q(x)$и исключить его отрицание одновременно, и соответствующее правило Де Моргана применяется, как указано выше. Но в некоторых случаях теория может также допускать заявление об отказе. $\neg \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )}$. Принятие этого не требует предоставления специального $t\in X$ свидетельствовать о неудаче исключенного третьего для конкретного предложения $Q(t)$, то есть свидетельствовать о противоречивом $\neg {\big (}Q(t)\lor \neg Q(t){\big )}$. Предикаты $Q(x)$ на бесконечном домене $X$соответствуют решению проблем . Руководствуясь доказанно вычислимо неразрешимыми проблемами , можно отвергнуть возможность разрешимости предиката, не делая при этом никаких утверждений о существовании предиката. $X$. Другой пример: такая ситуация реализуется в интуиционистском анализе Брауэра в случае, когда квантор распространяется на бесконечное множество бесконечных двоичных последовательностей и $Q(x)$ утверждает, что последовательность $x$везде равен нулю. Что касается этого свойства окончательной идентификации как вечно постоянной последовательности, принятие принципа непрерывности Брауэра строго исключает возможность доказать, что это разрешимо для всех последовательностей.

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

История и обзор

Исторически предметом конструктивной теории множеств (часто также « ${\mathsf {CST}}$») началось с работы Джона Майхилла над теориями, также называемыми ${\mathsf {IZF}}$ и ${\mathsf {CST}}$. В 1973 году он предложил первую теорию множеств первого порядка, основанную на интуиционистской логике и взяв наиболее общий фундамент. ${\mathsf {ZFC}}$и отбросив Аксиому выбора, а также принцип исключенного третьего, изначально оставив все остальное как есть. Однако различные формы некоторых из ${\mathsf {ZFC}}$ аксиомы, которые эквивалентны в классической ситуации, неэквивалентны в конструктивной ситуации, а некоторые формы подразумевают ${\mathrm {PEM} }$, как будет показано. В этих случаях последовательно принимались интуиционистски более слабые формулировки. Гораздо более консервативная система ${\mathsf {CST}}$ также является теорией первого порядка, но нескольких видов и с ограниченной количественной оценкой, стремящейся обеспечить формальную основу для Эрретта Бишопа программы конструктивной математики .

Основное обсуждение представляет собой последовательность теорий на том же языке, что и ${\mathsf {ZF}}$, что привело к Питеру Акселю хорошо изученному ${\mathsf {CZF}}$, и за его пределами. Многие современные результаты восходят к Ратьену и его ученикам. ${\mathsf {CZF}}$также характеризуется двумя особенностями, присутствующими и в теории Майхилла: С одной стороны, он использует предикативное разделение вместо полной, неограниченной схемы разделения. Ограниченность можно рассматривать как синтаксическое свойство или, альтернативно, теории можно консервативно расширить с помощью предиката более высокой ограниченности и его аксиом. Во-вторых, непредикативная аксиома Powerset отбрасывается, как правило, в пользу родственных, но более слабых аксиом. Сильная форма очень часто используется в классической общей топологии . Добавление ${\mathrm {PEM} }$ теории, даже более слабой, чем ${\mathsf {CZF}}$ выздоравливает ${\mathsf {ZF}}$, как подробно описано ниже. Система, которая стала известна как интуиционистская теория множеств Цермело – Френкеля ( ${\mathsf {IZF}}$), является сильной теорией множеств без ${\mathrm {PEM} }$. Это похоже на ${\mathsf {CZF}}$, но менее консервативен или предикативен . Теория обозначала ${\mathsf {IKP}}$ это конструктивная версия ${\mathsf {KP}}$, классическая теория множеств Крипке – Платека без формы Powerset и где даже аксиома коллекции ограничена.

Модели

Многие теории, изучаемые в конструктивной теории множеств, представляют собой просто ограничения теории множеств Цермело – Френкеля ( ${\mathsf {ZF}}$) относительно их аксиомы, а также лежащей в их основе логики. Такие теории затем можно интерпретировать в любой модели мира. ${\mathsf {ZF}}$.

Арифметика Пеано ${\mathsf {PA}}$ биинтерпретируема данной с теорией, ${\mathsf {ZF}}$минус бесконечность и отсутствие бесконечных множеств, плюс существование всех транзитивных замыканий . (Последнее также подразумевается после продвижения Регулярность для схемы « установки индукции », которая обсуждается ниже.) Аналогично, конструктивная арифметика также может быть принята как апология большинства аксиом, принятых в ${\mathsf {CZF}}$: Приветствующая арифметика ${\mathsf {HA}}$ биинтерпретируема со слабой конструктивной теорией множеств, как также описано в статье о ${\mathsf {HA}}$. Можно арифметически охарактеризовать отношение принадлежности». $\in$" и с его помощью докажите - вместо существования множества натуральных чисел $\omega$ - что все множества в его теории находятся в биекции с (конечным) естественным фон Нейманом , принцип, обозначаемый ${\mathrm {V} }={\mathrm {Fin} }$. Этот контекст дополнительно проверяет экстенсиональность, спаривание, объединение, двоичное пересечение (которое связано со схемой аксиомы предикативного разделения ) и схему индукции множеств. Взятые в качестве аксиом, вышеупомянутые принципы составляют теорию множеств, которая уже идентична теории, данной ${\mathsf {CZF}}$ минус существование $\omega$ цель больше ${\mathrm {V} }={\mathrm {Fin} }$как аксиома. Все эти аксиомы подробно обсуждаются ниже. Соответственно, ${\mathsf {CZF}}$также доказывает, что наследственно конечные множества удовлетворяют всем предыдущим аксиомам. Это результат, который сохраняется при переходе к ${\mathsf {PA}}$ и ${\mathsf {ZF}}$ минус бесконечность.

Что касается конструктивных реализаций, то существует соответствующая теория реализуемости . Соответственно, теория Акцеля конструктивна Цермело-Френкелю. ${\mathsf {CZF}}$ интерпретировался в теориях типа Мартина-Лёфа , как это показано в разделе, посвященном ${\mathsf {CZF}}$. Таким образом, теоремы, доказуемые в этой и более слабых теориях множеств, являются кандидатами на компьютерную реализацию.

предпучковые Также были представлены модели для конструктивных теорий множеств. Они аналогичны моделям предпучков интуиционистской теории множеств, разработанной Даной Скотт в 1980-х годах. Модели реализуемости ${\mathsf {CZF}}$ внутри эффективных топосов были идентифицированы, которые, скажем, сразу обосновывают полное разделение, релятивизированный зависимый выбор. ${\mathrm {RDC} }$, независимость помещения ${\mathrm {IP} }$ для множеств, но и счетность всех множеств, принцип Маркова ${\mathrm {MP} }$ и диссертация Чёрча ${\mathrm {CT} _{0}}$ в формулировке для всех предикатов.

Обозначения

В аксиоматической теории множеств множества — это сущности, обладающие свойствами. Но тогда существует более сложная связь между понятием множества и логикой. Например, свойство быть натуральным числом меньше 100 можно переформулировать как член множества чисел с этим свойством. Аксиомы теории множеств управляют существованием множеств и, таким образом, определяют, какие предикаты могут быть материализованы как сущность сама по себе в этом смысле. Спецификация также напрямую регулируется аксиомами, как обсуждается ниже. Для практического рассмотрения рассмотрим свойство последовательности результатов подбрасывания монеты, в которой в целом больше орлов, чем решек. Это свойство можно использовать для выделения соответствующего подмножества любого набора конечных последовательностей подбрасываний монеты. Соответственно, теоретико-мерная формализация вероятностного события явно основана на множествах и предоставляет гораздо больше примеров.

В этом разделе представлены объектный язык и вспомогательные понятия, используемые для формализации этой материализации.

Язык

Пропозициональные связочные символы, используемые для образования синтаксических формул, стандартны. Аксиомы теории множеств дают средство доказать равенство ». $=$«множеств, и этот символ может, злоупотребляя обозначениями , использоваться для классов. Множество, в котором предикат равенства разрешим, также называется дискретным . Отрицание» $\neg$«равенство иногда называют отрицанием равенства и обычно пишут « $\neq$Однако в контексте отношений обособленности , например, при работе с последовательностями, последний символ также иногда используется для чего-то другого.

Общая трактовка, также принятая здесь, формально лишь расширяет лежащую в основе логику одним примитивным бинарным предикатом теории множеств». $\in$«.Как и равенство, отрицание стихийности» $\in$"часто пишут" $\notin$".

Переменные

Ниже греческого $\phi$ обозначает переменную предложения или предиката в схемах аксиом и $P$ или $Q$используется для конкретных таких предикатов. Слово «предикат» иногда используется как синоним слова «формулы», даже в унарном случае .

Кванторы всегда варьируются только по множествам, и они обозначаются строчными буквами. Как обычно, для выражения предикатов можно использовать скобки аргументов, чтобы выделить определенные свободные переменные в их синтаксическом выражении, как в « $Q(z)$". Уникальное существование $\exists !x.Q(x)$ здесь означает $\exists x.\forall y.{\big (}y=x\leftrightarrow Q(y){\big )}$.

Классы

используется нотация компоновщика множеств Как обычно, для классов , которая в большинстве контекстов не является частью объектного языка, а используется для краткого обсуждения. В частности, можно ввести объявления обозначений соответствующего класса через " $A=\{z\mid Q(z)\}$", с целью выражения какого-либо $Q(a)$ как $a\in A$. Для представления одного и того же класса можно использовать логически эквивалентные предикаты. Еще один пишет $\{z\in B\mid Q(z)\}$ как сокращение для $\{z\mid z\in B\land Q(z)\}$. Например, можно рассмотреть $\{z\in B\mid z\notin C\}$ и это также обозначается $B\setminus C$.

Один сокращает $\forall z.{\big (}z\in A\to Q(z){\big )}$ к $\forall (z\in A).Q(z)$ и $\exists z.{\big (}z\in A\land Q(z){\big )}$ к $\exists (z\in A).Q(z)$. Синтаксическое понятие ограниченной количественной оценки в этом смысле может играть роль в формулировке схем аксиом, как видно из обсуждения аксиом ниже. Выразить подкласса утверждение $\forall (z\in A).z\in B$, то есть $\forall z.(z\in A\to z\in B)$, к $A\subset B$. Для предиката $Q$, тривиально $\forall z.{\big (}(z\in B\land Q(z))\to z\in B{\big )}$. И отсюда следует, что $\{z\in B\mid Q(z)\}\subset B$. Понятие кванторов, ограниченных подмножеством, как в $\forall (z\subset A).z\in B$, также использовался в теоретических исследованиях множеств, но здесь не будет далее освещаться.

Если доказано, что существует набор, то есть внутри класса $\exists z.(z\in A)$, то его называют обитаемым . Можно также использовать количественную оценку в $A$ выразить это как $\exists (z\in A).(z=z)$. Класс $A$тогда доказано, что это не пустое множество, представленное ниже. Хотя это классически эквивалентно, конструктивно непустое понятие является более слабым и имеет два отрицания, и его следует называть необитаемым . К сожалению, слово, обозначающее более полезное понятие «обитаемый», редко используется в классической математике.

Два способа выразить, что классы не пересекаются, действительно отражают многие интуиционистски допустимые правила отрицания: ${\big (}\forall (x\in A).x\notin B{\big )}\leftrightarrow \neg \exists (x\in A).x\in B$. Используя приведенные выше обозначения, это чисто логическая эквивалентность, и в этой статье предложение, кроме того, будет выражаться как $A\cap B=\{\}$.

Подкласс $A\subset B$ называется отделяемым от $B$ если релятивизированный предикат принадлежности разрешим, т. е. если $\forall (x\in B).x\in A\lor x\notin A$держит. Его еще называют разрешимым, если суперкласс ясен из контекста — часто это набор натуральных чисел.

Экстенсиональная

Обозначим через $A\simeq B$ утверждение, выражающее, что два класса имеют одни и те же элементы, т.е. $\forall z.(z\in A\leftrightarrow z\in B)$или эквивалентно $(A\subset B)\land (B\subset A)$. Это не следует путать с понятием равночисленности, которое также используется ниже.

С $A$ стоящий за $\{z\mid Q(z)\}$, удобное обозначение между $x\in A$ и $Q(x)$, аксиомы вида $\exists a.\forall z.{\big (}z\in a\leftrightarrow Q(z){\big )}$ постулировать, что класс всех множеств, для которых $Q$Hold фактически образует набор . Менее формально это можно выразить как $\exists a.a\simeq A$. Аналогично, предложение $\forall a.(a\simeq A)\to P(a)$ передает " $P(A)$ когда $A$ входит в число множеств теории». Для случая, когда $P$ является тривиально ложным предикатом, то предложение эквивалентно отрицанию предыдущего утверждения о существовании, выражающему несуществование $A$ как набор.

Дальнейшие расширения обозначений понимания классов, приведенные выше, обычно используются в теории множеств, придавая смысл таким утверждениям, как « $\{f(z)\mid Q(z)\}\simeq \{\langle x,y,z\rangle \mid T(x,y,z)\}$", и так далее.

Синтаксически более общий набор $w$ также можно охарактеризовать с помощью другого 2-арного предиката $R$ впадина $\forall x.x\in w\leftrightarrow R(x,w)$, где правая часть может зависеть от фактической переменной $w$и, возможно, даже о членстве в $w$ сам.

Подтеории ZF

Здесь представлен ряд знакомых аксиом или их соответствующие небольшие переформулировки. Подчеркивается, что отсутствие ${\mathrm {PEM} }$ в логике затрагивается то, что доказуемо, и выделяется, какие неклассические аксиомы, в свою очередь, непротиворечивы.

Равенство

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

Экстенсиональность $\forall x.\forall y.\ \ x\simeq y\to x=y$

В конструктивной интерпретации элементы подкласса $A=\{z\in B\mid Q(z)\lor \neg Q(z)\}$ из $B$ может содержать больше информации, чем те, которые $B$в том смысле, что иметь возможность судить $b\in A$ способен судить $Q(b)\lor \neg Q(b)$. И (если вся дизъюнкция не следует из аксиом) в интерпретации Брауэра–Хейтинга–Колмогорова это означает доказать $Q(b)$или отвергнув его. Как $\{z\in B\mid Q(z)\}$ не может быть отсоединен от $B$, то есть как $Q$ может быть неразрешимым для всех элементов $B$, два класса $A$ и $B$ априори необходимо различать.

Рассмотрим предикат $Q$ что доказано справедливо для всех элементов множества $y$, так что $y\simeq \{z\in y\mid Q(z)\}$и предположим, что класс в правой части установлен как множество. Обратите внимание, что даже если этот набор справа неформально также связан с релевантной для доказательства информацией о достоверности $Q$аксиома экстенсиональности постулирует, что для всех элементов в нашей теории множеств множество в правой части считается равным множеству в левой части. Приведенный выше анализ также показывает, что утверждение вида $\forall (x\in w).Q(x)$, что в неформальной нотации класса может быть выражено как $w\subset \{x\mid Q(x)\}$, тогда эквивалентно выражается как $\{x\in w\mid Q(x)\}=w$. Это означает, что установление такого $\forall$-теоремы (например, доказуемые с помощью полной математической индукции) позволяют заменить подкласс $w$ в левой части равенства для всего $w$, в любой формуле.

Обратите внимание, что принятие " $=$«как символ в теории логики предикатов делает равенство двух членов выражением, свободным от кванторов.

Альтернативные

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

Вместо этого современные теории типов могут быть направлены на определение требуемой эквивалентности». $\simeq$В терминах функций см., например, эквивалентность типов . Соответствующая концепция экстенсиональности функции часто не принимается в теории типов.

Вместо этого другие концепции конструктивной математики могут требовать особого правила равенства или обособленности элементов. $z\in x$ из каждого набора $x$обсуждалось. Но и в подходе к множествам, подчеркивающим обособленность, можно использовать приведенное выше определение в терминах подмножеств для характеристики понятия равенства». $\simeq$" из этих подмножеств. Соответственно, расплывчатое представление о дополнении двух подмножеств $u\subset x$ и $v\subset x$ дается, когда любые два члена $s\in u$ и $t\in v$доказуемо отделены друг от друга. Коллекция дополняющих пар. $\langle u,v\rangle$ хорошо себя алгебраически ведет.

Объединение наборов

Определите обозначение класса для соединения нескольких заданных элементов посредством дизъюнкций. Например $z\in \{a,b\}$ это утверждение без кванторов $(z=a)\lor (z=b)$, и аналогично $z\in \{a,b,c\}$ говорит $(z=a)\lor (z=b)\lor (z=c)$, и так далее.

Два других основных постулата существования при наличии других наборов заключаются в следующем. Во-первых,

Сопряжение $\forall x.\forall y.\ \ \exists p.\{x,y\}\subset p$

Учитывая приведенные выше определения, $\{x,y\}\subset p$ расширяется до $\forall z.(z=x\lor z=y)\to z\in p$, так что здесь используется равенство и дизъюнкция. Аксиома гласит, что для любых двух множеств $x$ и $y$, есть хотя бы один набор $p$, которые содержат по крайней мере эти два набора.

С ограниченным разделением ниже также класс $\{x,y\}$существует как множество. Обозначим через $\langle x,y\rangle$ стандартная упорядоченной пары модель $\{\{x\},\{x,y\}\}$, так что, например, $q=\langle x,y\rangle$ обозначает другую ограниченную формулу на формальном языке теории.

А затем, используя экзистенциальную квантификацию и союз,

Союз $\forall x.\ \ \exists u.\forall z.{\Big (}{\big (}\exists (y\in x).z\in y{\big )}\to z\in u{\Big )}$

говоря, что для любого набора $x$, есть хотя бы один набор $u$, который содержит все члены $z$, из $x$члены $y$. Минимальным таким набором является объединение .

Две аксиомы обычно формулируются более строго: $\leftrightarrow$"вместо просто" $\to$", хотя это технически избыточно в контексте ${\mathsf {BCST}}$: Поскольку приведенная ниже аксиома разделения сформулирована как « $\leftrightarrow$", для заявлений $\exists t.\forall z.\phi (z)\to z\in t$ эквивалентность может быть получена, если теория допускает разделение с помощью $\phi$. В случаях, когда $\phi$ является экзистенциальным утверждением, как здесь в аксиоме объединения, есть и другая формулировка , использующая квантор универсальности.

Также, используя ограниченное разделение, две только что сформулированные вместе аксиомы подразумевают существование бинарного объединения двух классов. $a$ и $b$, когда установлено, что они являются множествами, обозначаемыми $\bigcup \{a,b\}$ или $a\cup b$. Для фиксированного набора $z$, чтобы подтвердить членство $z\in a\cup b$ в объединении двух данных множеств $y=a$ и $y=b$, необходимо подтвердить $z\in y$ часть аксиомы, что можно сделать путем проверки дизъюнкции предикатов, определяющих множества $a$ и $b$, для $z$. С точки зрения связанных множеств это делается путем проверки дизъюнкции $z\in a\lor z\in b$.

Объединение и другие обозначения, образующие множества, также используются для классов. Например, предложение $z\in A\land z\notin C$ написано $z\in A\setminus C$. Пусть сейчас $B\subset A$. Данный $z\in A$, разрешимость принадлежности к $B$, т.е. потенциально независимое утверждение $z\in B\lor z\notin B$, также может быть выражено как $z\in B\cup (A\setminus B)$. Но, что касается любого исключенного среднего утверждения, двойное отрицание последнего справедливо: этот союз не населен не $z$. Это показывает, что секционирование также является более сложным понятием с конструктивной точки зрения.

Установить существование

Свойство, являющееся ложным для любого множества, соответствует пустому классу, который обозначается $\{\}$ или ноль, $0$. То, что пустой класс является множеством, легко следует из других аксиом существования, таких как аксиома бесконечности, приведенная ниже. Но если, например, кто-то явно заинтересован в исключении бесконечных множеств из своего исследования, на этом этапе он может принять

Аксиома пустого множества : $\exists x.\forall y.\,\neg (y\in x)$

Введение символа $\{\}$(как сокращенное обозначение выражений с использованием характеризующих свойств) оправдано, поскольку уникальность этого набора может быть доказана. Как $y\in \{\}$ ложно для любого $y$, аксиома тогда читается $\exists x.x\simeq \{\}$.

Писать $1$ для $S0$, что равно $\{\{\}\}$, то есть $\{1\}$. Аналогично, напишите $2$ для $S1$, что равно $\{\{\},\{\{\}\}\}$, то есть $\{0,1\}$. Тогда простым и заведомо ложным утверждением будет, например, $\{\}\in \{\}$, соответствующий $0<0$в стандартной арифметической модели. Опять же, здесь такие символы, как $\{\}$ рассматриваются как удобные обозначения, и любое предложение действительно преобразуется в выражение, использующее только « $\in$» и логические символы, включая кванторы. В сочетании с метаматематическим анализом того, что возможности новых теорий эффективно эквивалентны, формальные расширения с помощью таких символов, как $0$ также можно рассмотреть.

В более общем случае для набора $x$, определите набор преемников $Sx$ как $x\cup \{x\}$. Взаимодействие операции-преемника с отношением членства имеет рекурсивное предложение в том смысле, что $(y\in Sx)\leftrightarrow (y\in x\lor y=x)$. В силу рефлексивности равенства, $x\in Sx$, и в частности $Sx$ всегда заселен.

BCST

Далее используются схемы аксиом , т.е. аксиомы для некоторого набора предикатов. Некоторые из заявленных схем аксиом также должны допускать любой набор заданных параметров (то есть любые конкретные именованные переменные). $v_{0},v_{1},\dots ,v_{n}$). То есть допускаются экземпляры схемы, в которых предикат (некоторый конкретный $\phi$) также зависит от ряда дополнительных переменных множества, и утверждение аксиомы понимается с соответствующими дополнительными внешними универсальными замыканиями (как в $\forall v_{0}.\forall v_{1}.\cdots \forall v_{n}.$).

Разделение

Основная конструктивная теория множеств ${\mathsf {BCST}}$состоит из нескольких аксиом, также являющихся частью стандартной теории множеств, за исключением того, что так называемая «полная» аксиома разделения ослаблена. Помимо четырех вышеперечисленных аксиом, он постулирует предикативное разделение, а также схему замены.

Схема аксиом разделения предикатов : для любого ограниченного предиката $\phi$, с параметрами и с заданной переменной $y$ не свободен в этом, $\forall y.\,\exists s.\forall x.{\big (}x\in s\,\leftrightarrow \,(x\in y\land \phi (x)){\big )}$

Эта аксиома сводится к постулированию существования множества $s$ получается пересечением любого множества $y$ и любой предикативно описанный класс $\{x\mid \phi (x)\}$. Для любого $z$ оказывается множеством, когда предикат принимается как $\phi (x):=x\in z$, получаем бинарное пересечение множеств и записываем $s=y\cap z$. Пересечение соответствует соединению аналогично тому, как объединение соответствует дизъюнкции.

Когда предикат принимается как отрицание $\phi (x):=x\notin z$, получается разностный принцип, допускающий существование любого множества $y\setminus z$. Обратите внимание, что наборы типа $y\setminus y$ или $\{x\in y\mid \neg (x=x)\}$всегда пусты. Итак, как отмечалось, из разделения и существования хотя бы одного множества (например, Бесконечности ниже) будет следовать существование пустого множества. $\{\}$ (также обозначается $0$). В этом консервативном контексте ${\mathsf {BCST}}$, схема предикативного разделения фактически эквивалентна пустому множеству плюс существование двоичного пересечения для любых двух множеств. Последний вариант аксиоматизации не использует схему-формулу.

Предикативное разделение — это схема, которая учитывает синтаксические аспекты предикатов, определяющих множество, с точностью до доказуемой эквивалентности. Разрешенные формулы обозначаются $\Delta _{0}$, самый низкий уровень в теоретической иерархии Леви . Общие предикаты в теории множеств никогда синтаксически не ограничиваются таким образом, и поэтому на практике родовые подклассы множеств все еще являются частью математического языка. Поскольку область действия подклассов, которые являются доказуемыми множествами, чувствительна к тому, какие множества уже существуют, эта область действия расширяется при добавлении дополнительных постулатов существования множеств.

Для предложения $P$, повторяющимся приемом в конструктивном анализе теории множеств является рассмотрение предиката $x=0\land P$ как подкласс $B:=\{x\in 1\mid P\}$ второго ординала $1:=S0=\{0\}$. Если доказано, что $P$ держится, или $\neg P$, или $\neg \neg P$, затем $B$является обитаемым, или пустым (необитаемым), или непустым (необитаемым) соответственно. Четко, $P$ эквивалентно как предложению $0\in B$, а также $B=1$. Так же, $\neg P$ эквивалентно $B=0$ и, что то же самое, также $\neg (0\in B)$. Так вот, $B$ будучи отделяемым от $1$ именно означает $P\lor \neg P$. В модели натуральных чисел, если $B$ это число, $0\in B$ также выражает это $0$ меньше, чем $B$. Объединение, которое является частью приведенного выше определения операции-преемника, может использоваться для выражения исключенного среднего оператора как $0\in SB$. В словах, $P$ разрешима тогда и только тогда, когда преемник $B$ больше наименьшего порядкового номера $0$. Предложение $P$ решается в любом случае путем установления того, как $0$ меньше: по $0$ уже меньше, чем $B$или по $0$ существование $SB$прямой предшественник. Еще один способ выразить исключенное среднее для $P$ это существование наименьшего числа членов обитаемого класса $b:=B\cup \{1\}$.

Если аксиома разделения допускает разделение с $P$, затем $B$ подмножество представляет собой , которое можно назвать значением истинности, связанным с $P$. Два значения истинности можно доказать равными как множества, доказав эквивалентность. В терминах этой терминологии совокупность доказательных значений априори можно понимать как богатую. Неудивительно, что разрешимые предложения имеют один из двоичных наборов истинностных значений. Исключенная средняя дизъюнкция для этого $P$ тогда также подразумевается глобальным утверждением $\forall b.(0\in b)\lor (0\notin b)$.

Нет универсального набора

При использовании неформальной терминологии классов любое множество также считается классом. В то же время возникают так называемые собственные классы, которые не могут иметь расширения как множество. Когда в теории есть доказательство $\neg \exists x.A\subset x$, затем $A$должно быть правильно. (В ${\mathsf {ZF}}$, который имеет полное разделение, подходящие классы обычно считаются «слишком большими», чтобы быть набором. Говоря более технически, они являются подклассами совокупной иерархии , выходящей за пределы любых порядковых границ.)

Согласно замечанию в разделе о слиянии множеств, набор не может последовательно исключаться из числа членов класса вида $A\cup \{x\mid x\notin A\}$. Конструктивное доказательство того, что он принадлежит к этому классу, содержит информацию. Сейчас если $A$ это множество, то класс $\{x\mid x\notin A\}$является доказуемо правильным. Нижеследующее демонстрирует это в частном случае, когда $A$ пусто, т.е. когда правая часть представляет собой универсальный класс.

Для любого отношения справедливо следующее $E$. Это дает чисто логическое условие, что два члена $s$ и $y$ не может быть $E$- связанные друг с другом.

${\big (}\forall x.xEs\leftrightarrow (xEy\land \neg xEx){\big )}\to \neg (yEs\lor sEs\lor sEy)$

Самое главное здесь — отказ от окончательного дизъюнкта, $\neg sEy$. Выражение $\neg (x\in x)$не предполагает неограниченной количественной оценки и поэтому допускается при разделении. Конструкция Рассела, в свою очередь, показывает, что $\{x\in y\mid x\notin x\}\notin y$. Итак, для любого набора $y$, само по себе предикативное разделение подразумевает, что существует множество, которое не является членом $y$. В частности, никакого универсального множества в этой теории не может существовать .

В теории, далее принимающей аксиому регулярности , например ${\mathsf {ZF}}$, доказано $x\in x$ ложно для любого набора $x$. Тогда это означает, что подмножество $\{x\in y\mid x\notin x\}$ равно $y$ сам по себе, и что класс $\{x\mid x\in x\}$ пустое множество.

Уже частный случай $s=y$ в приведенной выше формуле подразумевает, что подкласс $\{x\mid x\notin x\}$универсального класса также является правильным. Но даже в ${\mathsf {ZF}}$ без регулярности вполне логично существование собственного класса одиночных элементов, каждый из которых содержит в точности самих себя.

Кроме того, в теории со стратификацией , такой как «Интуиционистские новые основания» , синтаксическое выражение $x\in x$может быть запрещен при разделении. В свою очередь, приведенное выше доказательство отрицания существования универсального множества в этой теории невозможно.

Предикативность

Схема аксиом предикативного разделения также называется $\Delta _{0}$-Разделение или ограниченное разделение, как в разделе «Разделение», только для кванторов, ограниченных множеством . (Предупреждающее примечание: номенклатура иерархии Леви аналогична $\Delta _{0}^{0}$в арифметической иерархии , хотя сравнение может быть тонким: арифметическая классификация иногда выражается не синтаксически, а в терминах подклассов натуральных чисел. Кроме того, нижний уровень арифметической иерархии имеет несколько общих определений, некоторые из которых не позволяют использовать некоторые итоговые функции. Подобное различие не актуально на уровне $\Sigma _{1}^{0}$или выше. Наконец, обратите внимание, что $\Delta _{0}$ классификация формулы может быть выражена с точностью до эквивалентности в теории.)

Эта схема также является способом, которым Мак Лейн ослабляет систему, близкую к теории множеств Цермело. ${\mathsf {Z}}$, для математических основ , связанных с теорией топоса . Он также используется при изучении абсолютности и является частью формулировки теории множеств Крипке-Платека .

Ограничением аксиомы также являются непредикативные определения: в лучшем случае не следует утверждать о существовании объектов, которые не поддаются явному описанию или чье определение включает в себя самих себя или ссылку на соответствующий класс, например, когда проверяемое свойство включает в себя квантор универсальности. . Итак, в конструктивной теории без аксиомы степенного множества , когда $R$ обозначает некоторый 2-арный предикат, обычно не следует ожидать подкласса $s$ из $y$ быть множеством, если оно определено, например, как в

$\{x\in y\mid \forall t.{\big (}(t\subset y)\to R(x,t){\big )}\}$,

или через аналогичные определения, включающие любую количественную оценку наборов $t\subset y$. Обратите внимание: если этот подкласс $s$ из $y$ доказано является множеством, то само это подмножество также находится в неограниченной области действия переменной set. $t$. Другими словами, как свойство подкласса $s\subset y$ выполняется, именно этот набор $s$, определяемый с помощью выражения $R(x,s)$, будет играть роль в его собственной характеристике.

В то время как предикативное разделение приводит к меньшему количеству заданных определений классов, можно подчеркнуть, что многие определения классов, которые являются классически эквивалентными, не являются таковыми, если ограничиваться более слабой логикой. Из-за потенциальной неразрешимости общих предикатов понятия подмножества и подкласса автоматически становятся более сложными в конструктивных теориях множеств, чем в классических. Таким образом, можно получить более широкую теорию. Это остается верным, если принимается полное разделение, например, в теории ${\mathsf {IZF}}$, что, однако, портит свойство существования , а также теоретические интерпретации стандартного типа и, таким образом, портит восходящий взгляд на конструктивные множества. Кроме того, поскольку подтипирование не является необходимой особенностью конструктивной теории типов , можно сказать, что конструктивная теория множеств сильно отличается от этой концепции.

Замена

Далее рассмотрим

Схема аксиом замены : для любого предиката $\phi$ с заданной переменной $r$ не свободен в этом, $\forall d.\ \ \forall (x\in d).\exists !y.\phi (x,y)\to \exists r.\forall y.{\big (}y\in r\leftrightarrow \exists (x\in d).\phi (x,y){\big )}$

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

Через замену существование любой пары $\{x,y\}$ также следует из результатов любой другой конкретной пары, например $\{0,1\}=2=SS0$. Но поскольку бинарное объединение, используемое в $S$ уже использовал аксиому спаривания, этот подход затем требует постулировать существование $2$ над тем из $0$. В теории с непредикативной аксиомой Powerset существование $2\subset {\mathcal {P}}{\mathcal {P}}0$ также можно продемонстрировать с помощью разделения.

С помощью схемы замены изложенная до сих пор теория доказывает, что классы эквивалентности или индексированные суммы являются множествами. В частности, декартово произведение , содержащее все пары элементов двух множеств, является множеством. В свою очередь, для любого фиксированного числа (в метатеории) соответствующее выражение произведения, скажем $x\times x\times x\times x$, можно построить как множество. Аксиоматические требования к множествам, рекурсивно определенным в языке, обсуждаются ниже. Множество $x$ дискретно, т.е. равенство элементов внутри множества $x$ разрешимо, если соответствующее отношение как подмножество $x\times x$ разрешимо.

Замена важна для понимания функции и может рассматриваться как форма понимания в более общем плане. Только при условии ${\mathrm {PEM} }$Замена уже подразумевает полное Разделение. В ${\mathsf {ZF}}$Замена наиболее важна для доказательства существования множеств высокого ранга , а именно с помощью примеров схемы аксиом, где $\phi (x,y)$ относится к относительно небольшому набору $x$ к более крупным, $y$.

Конструктивные теории множеств обычно имеют схему аксиом замены, иногда ограничивающуюся ограниченными формулами. Однако когда другие аксиомы отбрасываются, эта схема на самом деле часто усиливается — не более чем ${\mathsf {ZF}}$, а вместо этого просто для того, чтобы вернуть себе некоторую силу доказуемости. Существуют такие более сильные аксиомы, которые не портят сильные свойства существования теории, как обсуждается ниже.

Если $i_{X}$ доказано является функцией $X$ и он оснащен кодоменом $Y$ (подробно все описано ниже), изображение затем $i_{X}$ является подмножеством $Y$. В других подходах к концепции множества понятие подмножеств определяется таким образом в терминах «операций».

Наследственно конечные множества

Подвески элементов класса наследственно конечных множеств $H_{\aleph _{0}}$может быть реализован на любом распространенном языке программирования. Обсуждаемые выше аксиомы абстрагируются от общих операций над заданным типом данных : объединение, разделение и замена связаны со сглаживанием , фильтрацией и пониманием . Замены вместе с индукцией множеств (представленной ниже) достаточно, чтобы аксиомизировать $H_{\aleph _{0}}$ конструктивно и эта теория изучается и без Бесконечности.

Своего рода смесь спаривания и союза, аксиома, которую легче отнести к преемнику, — это аксиома присоединения . Такие принципы актуальны для стандартного моделирования отдельных ординалов Неймана . Хотя постулирование замены не является необходимостью при разработке слабой конструктивной теории множеств, которая двояко интерпретируется арифметикой Гейтинга ${\mathsf {HA}}$, это некая форма индукции. Для сравнения рассмотрим очень слабую классическую теорию, называемую общей теорией множеств , которая интерпретирует класс натуральных чисел и их арифметику посредством только экстенсиональности, присоединения и полного разделения.

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

ЭКСТ

Для некоторого фиксированного предиката $I$ и набор $a$, заявление $I(a)\land {\big (}\forall y.I(y)\to a\subset y{\big )}$ выражает это $a$ является наименьшим (в смысле " $\subset$") среди всех наборов $y$ для которого $I(y)$ верно, и что это всегда подмножество таких $y$. Цель аксиомы бесконечности состоит в том, чтобы в конечном итоге получить уникальное наименьшее индуктивное множество .

В контексте аксиом общей теории множеств одним из утверждений о бесконечности является утверждение, что класс обитаем, а также включает в себя цепочку членства (или, альтернативно, цепочку надмножеств). То есть,

$\exists z.(z\in A)\land \forall (x\in A).\exists (s\in A).x\in s$.

Более конкретно, обозначим через $\mathrm {Ind} _{A}$ индуктивное свойство,

$(0\in A)\land \forall (x\in A).Sx\in A$.

С точки зрения предиката $Q$ лежащий в основе класса, так что $\forall x.(x\in A)\leftrightarrow Q(x)$, последнее переводится как $Q(0)\land \forall x.{\big (}Q(x)\to Q(Sx){\big )}$.

Писать $\bigcap B$ для общего перекрестка $\{x\mid \forall (y\in B).x\in y\}$. (Можно рассмотреть вариант этого определения, требующий $\cap B\subset \cup B$, но мы используем это понятие только для следующего вспомогательного определения.)

Обычно определяют класс $\omega =\bigcap \{y\mid \mathrm {Ind} _{y}\}$, пересечение всех индуктивных множеств. (Варианты этой обработки могут работать по формуле, которая зависит от заданного параметра $w$ так что $\omega \subset w$.) Класс $\omega$ точно все держит $x$ выполнение неограниченного свойства $\forall y.\mathrm {Ind} _{y}\to x\in y$. Идея состоит в том, что если индуктивные множества вообще существуют, то класс $\omega$ делит с ними каждое общее натуральное число, а затем предложение $\omega \subset A$по определению " $\subset$", подразумевает, что $Q$справедливо для каждого из этих натуральных чисел. Хотя ограниченного разделения недостаточно для доказательства $\omega$ Чтобы быть желаемым набором, язык здесь формирует основу для следующей аксиомы, допускающей индукцию натуральных чисел для предикатов, составляющих набор.

Элементарная конструктивная теория множеств ${\mathsf {ECST}}$ имеет аксиому ${\mathsf {BCST}}$ а также постулат

Сильная бесконечность $\exists w.{\Big (}\mathrm {Ind} _{w}\,\land \,{\big (}\forall y.\mathrm {Ind} _{y}\to w\subset y{\big )}{\Big )}$

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

Символы, называемые нулем и преемником, находятся в подписи теории Пеано . В ${\mathsf {BCST}}$, определенный выше преемник любого числа также находится в классе $\omega$следуют непосредственно из характеристики природных явлений нашей моделью фон Неймана. Поскольку преемник такого набора содержит самого себя, также обнаруживается, что ни один преемник не равен нулю. Итак, две аксиомы Пеано , касающиеся символов нуля, и аксиома, касающаяся замкнутости символов. $S$прийти легко. В-четвертых, в ${\mathsf {ECST}}$, где $\omega$ это набор, $S$ на $\omega$ можно доказать, что это инъективная операция.

Для некоторого предиката множеств $P$, заявление $\forall S.(S\subset \omega \to P(S))$ претензии $P$справедливо для всех подмножеств множества натуральных чисел. И теперь аксиома доказывает, что такие множества действительно существуют. Такая количественная оценка возможна и в арифметике второго порядка .

Парный порядок" $<$"на естественных условиях отражается их отношение членства" $\in$". Важно отметить, что теория доказывает, что порядок, а также отношение равенства на этом множестве разрешимы. Мало того, что не существует числа , меньшего $0$, но индукция подразумевает, что среди подмножеств $\omega$, это именно пустое множество, в котором нет наименьшего члена. Противоположное этому доказывает существование дважды отрицательного наименьшего числа для всех непустых подмножеств $\omega$. Другой действительный принцип, также классически эквивалентный ему, - это существование наименьшего числа для всех обитаемых отделимых подмножеств. Тем не менее, простое утверждение о существовании обитаемого подмножества $b:=\{z\in 1\mid P\}\cup \{1\}$ из $\omega$ эквивалентно исключенному среднему для $P$, и поэтому конструктивная теория не докажет $\omega$ быть упорядоченным .

бесконечности

Если потребуется мотивация, то удобство постулирования неограниченного набора чисел по отношению к другим индуктивным свойствам станет очевидным при обсуждении арифметики в теории множеств ниже. Но, как известно из классической теории множеств, можно сформулировать и слабые формы Бесконечности. Например, можно просто постулировать существование некоторого индуктивного множества, $\exists y.\mathrm {Ind} _{y}$ - такого постулата существования достаточно, когда полное разделение может быть использовано для выделения индуктивного подмножества. $w$натуральных чисел, общего подмножества всех индуктивных классов. В качестве альтернативы могут быть приняты более конкретные постулаты простого существования. В любом случае индуктивный набор удовлетворяет следующим условиям: $\Delta _{0}$ Свойство существования предшественника в смысле модели фон Неймана :

$\forall m.(m\in w)\leftrightarrow {\big (}m=0\lor \exists (p\in w).Sp=m{\big )}$

Без использования обозначения ранее определенного обозначения преемника экстенсиональное равенство преемнику $Sp=m$ захвачен $\forall n.(n\in m)\leftrightarrow (n=p\lor n\in p)$. Это означает, что все элементы $m$ либо равны $0$ или сами содержат набор предшественников $p\in w$ который разделяет всех остальных членов с $m$.

Заметьте, что через выражение « $\exists (p\in w)$"в правой части свойство, характеризующее $w$ его членами $m$ здесь синтаксически снова содержится символ $w$сам. Из-за восходящей природы натуральных чисел, здесь это несложно. Предполагая $\Delta _{0}$-установить индукцию сверху ${\mathsf {ECST}}$, никакие два разных множества не обладают этим свойством. Также обратите внимание, что существуют и более длинные формулировки этого свойства, избегающие " $\exists (p\in w)$«в пользу неограниченных кванторов.

Границы числа

Приняв аксиому бесконечности, количественную оценку, ограниченную множеством, допустимую в предикатах, используемых в $\Delta _{0}$-Тогда разделение явно допускает числовые неограниченные кванторы - не следует путать два значения слова «ограниченный». С $\omega$ под рукой, вызовите класс номеров $I\subset \omega$ ограничен следующее утверждение существования , если выполняется

$\exists (m\in \omega ).\forall (n\in \omega ).(n\in I\to n<m)$

Это утверждение конечности, также эквивалентно сформулированное через $m\leq n\to n\notin I$. Аналогично, чтобы более подробно отразить обсуждение функций ниже, рассмотрим приведенное выше условие в форме $\exists (m\in \omega ).\forall (n\in I).(n<m)$. Для разрешимых свойств это $\Sigma _{2}^{0}$-утверждения в арифметике, но с Аксиомой Бесконечности два квантора привязаны к множествам.

Для класса $C$, логически положительное утверждение неограниченности

$\forall (k\in \omega ).\exists (j\in \omega ).(k\leq j\land j\in C)$

теперь также является одним из бесконечности. Это $\Pi _{2}^{0}$в разрешимом арифметическом случае. Для проверки бесконечности набора это свойство работает даже в том случае, если набор содержит другие элементы, помимо бесконечного числа членов. $\omega$.

ECST

Далее начальный сегмент натуральных чисел, т.е. $\{n\in \omega \mid n<m\}$ для любого $m\in \omega$ и включая пустое множество, обозначается $\{0,1,\dots ,m-1\}$. Это множество равно $m$ и так на данный момент" $m-1$" — это просто обозначение своего предшественника (т. е. без использования функции вычитания).

Поучительно вспомнить, каким образом теория с пониманием множеств и экстенсиональностью в конечном итоге кодирует логику предикатов. Как и любой класс теории множеств, множество можно рассматривать как соответствующее предикату множеств. Например, целое число является четным, если оно является членом набора четных целых чисел, или натуральное число имеет преемника, если оно является членом набора натуральных чисел, имеющих преемника. Для менее примитивного примера исправьте некоторый набор $y$ и разреши $Q(n)$ обозначают экзистенциальное утверждение о том, что функциональное пространство на конечном ординале превращается в $y$существовать. Предикат будет обозначаться $\exists h.h\simeq y^{\{0,1,\dots ,n-1\}}$ниже, и здесь квантор существования не является просто квантором натуральных чисел и не ограничен каким-либо другим множеством. Теперь такое утверждение, как принцип конечного возведения в степень $\forall (n\in \omega ).Q(n)$ и, менее формально, равенство $\omega =\{n\in \omega \mid Q(n)\}$ — это всего лишь два способа сформулировать одно и то же желаемое утверждение, а именно $n$-индексированное соединение экзистенциальных предложений, где $n$колеблется по множеству всех натуральных чисел. Посредством экстенсиональной идентификации вторая форма выражает утверждение, используя обозначения для понимания подкласса, а объект в скобках с правой стороны может даже не составлять набор. Если этот подкласс не является доказуемо множеством, его фактически нельзя использовать во многих принципах теории множеств при доказательствах и установлении универсального замыкания. $\forall (n\in \omega ).Q(n)$как теорема может быть невозможна. Таким образом, теорию множеств можно усилить за счет большего количества аксиом существования множеств, которые будут использоваться с предикативным ограниченным разделением, а также просто постулируя более сильные постулаты. $\forall$-заявления.

Второй универсально квантифицированный конъюнкт в сильной аксиоме Бесконечности выражает математическую индукцию для всех $y$во вселенной дискурса, т.е. для множеств. Это связано с тем, что следствие этого пункта, $\omega \subset y$, утверждает, что все $n\in \omega$выполнить соответствующий предикат. Умение использовать предикативное разделение для определения подмножеств $\omega$, теория доказывает индукцию для всех предикатов $\phi (n)$с участием только кванторов, ограниченных множеством. Эта роль кванторов, ограниченных множеством, также означает, что большее количество аксиом существования множеств влияет на силу этого принципа индукции, что дополнительно мотивирует аксиомы функционального пространства и коллекции, которые будут в центре внимания оставшейся части статьи. Примечательно, ${\mathsf {ECST}}$ уже подтверждает индукцию с кванторами по натуральным числам и, следовательно, индукцию, как в теории арифметики первого порядка. ${\mathsf {HA}}$. Так называемая аксиома полной математической индукции для любого предиката (т.е. класса), выраженная через язык теории множеств, намного сильнее, чем принцип ограниченной индукции, действительный в ${\mathsf {ECST}}$. Первый принцип индукции можно было бы использовать напрямую, более точно отражая арифметику второго порядка. В теории множеств это также следует из полного (то есть неограниченного) разделения, которое гласит, что все предикаты на $\forall$представляют собой наборы. Математическая индукция также заменяется (полной) аксиомой индукции множества.

Предупреждение: называя утверждения индукции, нужно стараться не смешивать терминологию с арифметическими теориями. Схема индукции первого порядка теории арифметики натуральных чисел требует индукции для всех предикатов, определяемых на языке арифметики первого порядка , а именно для предикатов простых чисел. Итак, чтобы интерпретировать схему аксиом ${\mathsf {HA}}$, интерпретируют эти арифметические формулы. В этом контексте ограниченная количественная оценка конкретно означает количественную оценку в конечном диапазоне чисел. Можно также говорить об индукции в теории первого порядка, но двусортной, так называемой арифметики второго порядка. ${\mathsf {Z}}_{2}$, в форме, явно выраженной для подмножеств натуральных чисел. Этот класс подмножеств можно считать соответствующим более богатому набору формул, чем определяемые арифметикой первого порядка. В программе обратной математики все обсуждаемые математические объекты кодируются как натуральные числа или подмножества натуральных чисел. Подсистемы ${\mathsf {Z}}_{2}$с очень низкой сложностью понимания, изучаемой в этой структуре, есть язык, который не просто выражает арифметические множества , в то время как все множества натуральных чисел, в частности такие теории, доказывают свое существование, являются просто вычислимыми множествами . Теоремы в них могут быть подходящей отправной точкой для слабых теорий множеств с набором натуральных чисел, предикативным разделением и лишь некоторыми дополнительными ограниченными формами индукции. Конструктивная обратная математика существует как область, но менее развита, чем ее классический аналог. ${\mathsf {Z}}_{2}$ кроме того, не следует путать с формулировкой арифметики Пеано второго порядка. ${\mathsf {PA}}_{2}$. Типичные теории множеств, подобные той, что обсуждается здесь, также относятся к первому порядку, но эти теории не являются арифметическими, поэтому формулы могут также давать количественные оценки подмножествам натуральных чисел. Обсуждая силу аксиом, касающихся чисел, также важно иметь в виду, что арифметическая и теоретическая основы не имеют общей сигнатуры . Аналогично, всегда следует проявлять осторожность при понимании совокупности функций. В теории вычислимости оператор µ позволяет использовать все частично общерекурсивные функции (или программы в том смысле, что они вычислимы по Тьюрингу), включая, например, непримитивно-рекурсивные, но ${\mathsf {PA}}$-всего, например, функция Аккермана . Определение оператора включает предикаты над натуральными числами, поэтому теоретический анализ функций и их совокупности зависит от формальной структуры и имеющегося исчисления доказательств.

Функции

Общие сведения о программах и функциях

Естественно, смысл утверждений о существовании представляет собой предмет интереса конструктивизма, будь то теория множеств или любая другая концепция. Позволять $R$ выражать свойство так, чтобы математическая основа подтверждала то, что составляет утверждение

$\forall (a\in A).\exists (c\in C).R(a,c)$

Конструктивное исчисление доказательств может подтвердить такое суждение с точки зрения программ на представленных областях и некоторого объекта, представляющего конкретное задание. $a\mapsto c_{a}$, обеспечивая конкретный выбор значения в $C$ ( уникальный ), для каждого входа из $A$. Выражено через переписывание $\forall (a\in A).R(a,c_{a})$, этот функциональный объект можно понимать как свидетельствующий о предложении. Рассмотрим, например, понятия доказательства в теории сквозной реализуемости или функциональные термины в теории типов с понятием кванторов. Последний фиксирует доказательство логического предложения с помощью программ через соответствие Карри-Ховарда .

В зависимости от контекста слово «функция» может использоваться в связи с конкретной моделью вычислений , и это априори уже, чем то, что обсуждается в настоящем контексте теории множеств. Одно понятие программы формализовано частично рекурсивными «функциями» в теории вычислимости . Но имейте в виду, что здесь слово «функция» используется таким образом, что оно также включает в себя частичные функции , а не только «полные функции». Здесь для ясности используются пугающие кавычки, поскольку в контексте теории множеств технически нет необходимости говорить о полных функциях , поскольку это требование является частью определения теоретической функции множеств, а пространства частичных функций можно моделировать посредством объединений. В то же время, в сочетании с формальной арифметикой, программы частичных функций дают особенно четкое представление о совокупности функций. По теореме Клини о нормальной форме каждая частично рекурсивная функция натуральных чисел вычисляет для значений, где она заканчивается, то же самое, что и $a\mapsto U(\mu w.T_{1}(e,a,w))$, для некоторого индекса частичной функции программы $e\in {\mathbb {N} }$, и любой индекс будет представлять собой некоторую частичную функцию. Программа может быть связана с $e$ и можно сказать, что это $T_{1}$-всего всякий раз, когда теория подтверждается $\forall a.\exists w.T_{1}(e,a,w)$, где $T_{1}$ представляет собой примитивную рекурсивную программу и $w$ связано с выполнением $e$. Крейзель доказал, что класс частично рекурсивных функций доказан $T_{1}$-всего по ${\mathsf {HA}}$ не обогащается, когда ${\mathrm {PEM} }$ добавлен. В качестве предиката в $e$, эта совокупность представляет собой неразрешимое подмножество индексов, подчеркивая, что рекурсивный мир функций между натуральными числами уже захвачен набором, в котором доминируют ${\mathbb {N} }$. В качестве третьего предупреждения обратите внимание, что это понятие на самом деле относится к программам, и несколько индексов фактически представляют собой одну и ту же функцию в экстенсиональном смысле.

Теории логики первого порядка , такие как аксиоматические теории множеств, обсуждаемые здесь, имеют совместное понятие общего и функционального для бинарного предиката. $R$, а именно $\forall a.\exists !c.R(a,c)$. Подобные теории относятся к программам лишь косвенно. Если $S$ обозначает последующую операцию на формальном языке изучаемой теории, тогда любое число, например ${\mathrm {SSS0} }$ (число три) может металогически быть связано со стандартным числом, например ${\underline {\mathrm {SSS0} }}=SSS0$. Точно так же программы в частично рекурсивном смысле могут быть развернуты до предикатов, и достаточно слабых предположений, чтобы такой перевод соблюдал равенство их возвращаемых значений. Среди конечно аксиомизируемых подтеорий ${\mathsf {PA}}$, классическая арифметика Робинсона ${\mathsf {Q}}$именно это выполняет. Заявления о его существовании касаются только натуральных чисел, и вместо использования полной схемы математической индукции для арифметических формул аксиомы теорий постулируют, что каждое число либо равно нулю, либо что для него существует число-предшественник. Сфокусироваться на $T_{1}$-тотальные рекурсивные функции здесь, это метатеорема, согласно которой язык арифметики выражает их с помощью $\Sigma _{1}$-предикаты $G$ кодируя их граф так, что ${\mathsf {Q}}$ представляет их в том смысле, что правильно доказывает или отвергает $G({\underline {\mathrm {a} }},{\underline {\mathrm {c} }})$ для любой пары чисел ввода-вывода $\mathrm {a}$ и $\mathrm {c}$в метатеории. Теперь, учитывая правильное представление $G$, предикат $G_{\mathrm {least} }(a,c)$ определяется $G(a,c)\land \forall (n<c).\neg G(a,n)$ также представляет рекурсивную функцию, и поскольку это явно проверяет только наименьшее возвращаемое значение, теория также доказывает функциональность для всех входных данных. ${\mathrm {a} }$ в смысле ${\mathsf {Q}}\vdash \exists !c.G_{\mathrm {least} }({\underline {\mathrm {a} }},c)$. Учитывая представляющий предикат, то за счет использования ${\mathrm {PEM} }$, всегда можно и систематически (т.е. с помощью $\forall a.$) докажите, что граф тотально функционален.

Какие предикаты доказуемо функциональны для различных входных данных или даже полностью функциональны в своей области, обычно зависит от принятых аксиом теории и исчисления доказательств. Например, для задачи диагональной остановки , которая не может иметь $T_{1}$-общий индекс, это ${\mathsf {HA}}$-независимо от того, соответствует ли соответствующий предикат графа ${\mathbb {N} }\times \{0,1\}$ ( проблема решения ) полностью функциональна, но ${\mathrm {PEM} }$подразумевает, что это так. Иерархии теоретических функций доказательства предоставляют примеры предикатов, доказавших полную функциональность в системах, выходящих за рамки ${\mathsf {PA}}$. Какие множества, существование которых доказано, действительно составляют полную функцию в смысле, введенном ниже, также всегда зависит от аксиом и исчисления доказательств. Наконец, обратите внимание, что обоснованность утверждений об остановке является металогическим свойством, выходящим за рамки согласованности, т. е. теория может быть последовательной, и на ее основе можно доказать, что некоторая программа в конечном итоге остановится, несмотря на то, что на самом деле этого никогда не происходит при запуске указанной программы. Более формально, предположение о непротиворечивости теории не означает, что она также арифметически арифметична. $\Sigma _{1}$-звук .

функциональные

На языке теории множеств будем говорить о функциональном классе, когда $f\subset A\times C$ и доказано

$\forall (a\in A).\,\exists !(c\in C).\langle a,c\rangle \in f$.

Примечательно, что это определение включает в себя квантор, явно требующий существования – аспект, который особенно важен в конструктивном контексте. На словах: Для каждого $a$, это требует уникального существования $c$ так что $\langle a,c\rangle \in f$. В этом случае можно использовать приложения функции и написать скобочную запись $f(a)=c$. Вышеупомянутое свойство может быть тогда сформулировано как $\forall (a\in A).\,\exists !(c\in C).f(a)=c$. Это обозначение может быть расширено до равенства значений функции. Некоторые удобства обозначений, связанные с применением функций, будут работать только в том случае, если множество действительно является функцией. Позволять $C^{A}$ (также написано $^{A}C$) обозначают класс множеств, которые удовлетворяют свойству функции. Это класс функций из $A$ к $C$в чистой теории множеств. Под обозначением $x\to y$ также используется для $y^{x}$, чтобы отличить его от порядкового возведения в степень. Когда функции понимаются как просто графики функций, как здесь, утверждение о принадлежности $f\in C^{A}$ также написано $f\colon A\to C$. Логическое значение $\chi _{B}\colon A\to \{0,1\}$ входят в число классов, обсуждаемых в следующем разделе.

По построению любая такая функция соблюдает равенство в том смысле, что $(x=y)\to f(x)=f(y)$, для любых входных данных от $A$. Об этом стоит упомянуть, поскольку в математической литературе существуют и более широкие концепции «процедур присваивания» или «операций», которые в целом могут не учитывать это. варианты определения функционального предиката с использованием отношений обособленности на сетоидах Определены также . Подмножество функции по-прежнему остается функцией, и предикат функции также может быть доказан для расширенных выбранных наборов кодоменов. Как уже отмечалось, следует проявлять осторожность с номенклатурой «функция», словом, которое используется в большинстве математических структур. Когда набор функций сам по себе не привязан к определенному кодомену, тогда этот набор пар также является членом функционального пространства с большим кодоменом. Этого не происходит, когда словом обозначается подмножество пар, спаренных с набором кодоменов, т.е. формализация в терминах $(A\times C)\times \{C\}$. В основном это вопрос бухгалтерского учета, но он влияет на определение других предикатов, а также на вопрос размера. Этот выбор также просто поддерживается некоторыми математическими структурами. Аналогичные соображения применимы к любому рассмотрению частичных функций и их областей определения.

Если оба домена $A$ и считается кодоменом $C$являются множествами, то указанный выше предикат функции включает только ограниченные кванторы. Общие понятия, такие как инъективность и сюръективность, также могут быть выражены ограниченным образом, как и биективность . И то, и другое связано с понятием размера. Важно отметить, что существование инъекции между любыми двумя наборами обеспечивает предварительный порядок . Класс власти не привносится в его базовый набор, и последний не отображается на первый. Сюръективность формально является более сложным определением. Обратите внимание, что инъективность должна определяться положительно, а не через ее противоположность, что является обычной практикой в ​​​​классической математике. Вариант без отрицаний иногда называют слабоинъективным. Существование коллизий значений является сильным понятием неинъективности. Что касается сюръективности, аналогичные соображения существуют и для производства выбросов в кодомене.

Можно ли считать подкласс (или предикат, если уж на то пошло) набором функций или даже полным функционалом, будет зависеть от силы теории, то есть от принятых аксиом. Примечательно, что общий класс также может выполнять указанный выше определяющий предикат, не являясь подклассом продукта. $A\times C$, т.е. свойство выражает не больше и не меньше, чем функциональность относительно входных данных от $A$. Теперь, если областью определения является множество, принцип понимания функций, также называемый аксиомой единственного выбора или невыбора, говорит, что функция как набор с некоторой кодоменой существует хорошо. (И этот принцип справедлив в такой теории, как ${\mathsf {CZF}}$. Также сравните с аксиомой замены .) То есть информация об отображении существует как набор и имеет пару для каждого элемента в домене. Конечно, для любого набора из некоторого класса всегда можно связать уникальный элемент синглтона. $1$, который показывает, что просто выбранного диапазона, являющегося набором, недостаточно для предоставления набора функций. Это метатеорема для теорий, содержащих ${\mathsf {BCST}}$что добавление функционального символа для доказанной полной функции класса является консервативным расширением, несмотря на то, что формально это меняет область действия ограниченного Separation . Таким образом, в контексте теории множеств основное внимание уделяется выявлению конкретных полных отношений , которые являются функциональными. Чтобы отделить понятие функции в теориях предыдущего подраздела (двухарный логический предикат, определенный для выражения графика функции вместе с утверждением о том, что он тотален и функционален) от теоретического понятия «материального» множества здесь, можно явно вызвать последний график функции , анафункции или функции установки . Схема аксиом замены также может быть сформулирована в терминах диапазонов таких функций множества.

Конечность

Один определяет три различных понятия, включающих сюръекции. То, что общее множество ( бишоп -) конечное , означает, что существует биективная функция по отношению к натуральному множеству. Если существование такой биекции доказано невозможно, множество называется неконечным . Во-вторых, для понятия более слабого, чем конечное, быть конечно индексированным (или -конечным по Куратовскому ) будет означать, что на него существует сюръекция натурального числа фон Неймана. С точки зрения программирования, элементы такого набора доступны в (конечном) цикле for , и только те, хотя невозможно определить, произошло ли повторение. В-третьих, назовите множество субконечным , если оно является подмножеством конечного множества, которое, таким образом, вводится в это конечное множество. Здесь цикл for будет иметь доступ ко всем членам набора, а также, возможно, к другим. Для другого комбинированного понятия, более слабого, чем конечно индексированное, быть субконечно индексированным означает находиться в сюръективном образе субконечного множества, и в ${\mathsf {ETCS}}$это просто означает, что это подмножество конечно индексированного набора, а это означает, что подмножество также может быть взято на стороне изображения, а не на стороне домена. Множество, демонстрирующее любое из этих понятий, можно понимать как мажорируемое конечным множеством, но во втором случае связь между членами множества не обязательно полностью понята. В третьем случае проверка членства в наборе, как правило, более сложна, и даже не требуется полностью понимать принадлежность его члена к некоторому надмножеству набора. Утверждение о том, что конечность всех множеств эквивалентна субконечности, эквивалентно ${\mathrm {PEM} }$. Дополнительные свойства конечности множества $X$ могут быть определены, например, выражая существование некоторого достаточно большого натурального числа, такого, что определенный класс функций на натуральных числах всегда не может отображаться в отдельные элементы в $X$. Одно определение рассматривает некоторое понятие неинъективности в $X$. Другие определения рассматривают функции из фиксированного надмножества $X$ с большим количеством элементов.

Терминология условий конечности и бесконечности может различаться. Примечательно, что множества с субконечной индексацией (понятие, обязательно включающее сюръекции) иногда называют субконечными (которые можно определить без функций). Свойство конечной индексации также можно было бы обозначить как «конечно счетное», чтобы соответствовать логике именования, но некоторые авторы также называют его конечно перечислимым (что может сбивать с толку, поскольку предполагает введение в другом направлении). Соответственно, существование биекции с конечным набором не установлено, можно сказать, что набор не конечен, но тогда такое использование языка слабее, чем утверждение, что набор неконечен. Та же проблема применима к счетным множествам (недоказанная счетность или доказанность несчетности) и так далее. Сюръективную карту также можно назвать перечислением.

Бесконечность

Набор $\omega$само по себе явно неограничено. Действительно, для любой сюръекции из конечной области на $\omega$, можно создать элемент, отличный от любого элемента в диапазоне функций. При необходимости это понятие бесконечности также может быть выражено через отношение обособленности на рассматриваемом множестве. Быть неконечным по Куратовскому означает быть неконечным, и действительно, натуральные числа не должны быть конечными ни в каком смысле. Обычно слово «бесконечный» используется для обозначения негативного понятия «неконечность». Далее заметьте, что $\omega$, в отличие от любого из его членов, может быть поставлен в биекцию с некоторыми из его собственных неограниченных подмножеств, например, с теми, которые имеют форму $w_{m}:=\{k\in \omega \mid k>m\}$ для любого $m\in \omega$. Это подтверждает формулировки Дедекинда-бесконечности . Таким образом, в более общем смысле, чем свойство бесконечности, о котором говорилось в предыдущем разделе об границах чисел, можно назвать множество бесконечным в логически положительном смысле, если можно ввести $\omega$внутрь. Множество, находящееся в биекции даже с $\omega$можно назвать счетно бесконечным. Множество является бесконечным по Тарскому, если существует цепочка $\subset$-увеличение его подмножеств. Здесь каждый набор имеет новые элементы по сравнению со своим предшественником и в определении не говорится о росте ранга множества. Действительно, существует множество свойств, характеризующих бесконечность даже в классических теориях. ${\mathsf {ZF}}$ и эта теория не доказывает, что все неконечные множества бесконечны в смысле инъекционного существования, хотя это справедливо и при дальнейшем предположении счетного выбора. ${\mathsf {ZF}}$ без какого-либо выбора даже разрешает кардиналы исключать числа алефа , и тогда могут существовать множества, которые отрицают оба вышеуказанных свойства, т. е. они являются одновременно недедекиндово-бесконечными и неконечными (также называемыми дедекиндово-конечными бесконечными множествами).

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

Существуют также различные способы характеристики логически отрицательного понятия. Понятие несчетности в том смысле, что оно неисчислимо, также обсуждается ниже в сочетании с аксиомой возведения в степень. Еще одно понятие несчетности $X$ дается, когда можно произвести член в дополнение к любому из $X$счетные подмножества. Другие свойства конечности могут быть определены как отрицание таких свойств и так далее.

Характеристические функции

Разделение позволяет нам вырезать подмножества продуктов. $A\times C$, по крайней мере, когда они описаны ограниченным образом. Учитывая любой $B\subset A$, теперь можно задуматься о таких классах, как

$X_{B}:={\big \{}\langle x,y\rangle \in A\times \{0,1\}\mid (x\in B\land y=1)\lor (x\notin B\land y=0){\big \}}.$

С $\neg (0=1)$, надо

${\big (}a\in B\ \leftrightarrow \,\langle a,1\rangle \in X_{B}{\big )}\,\land \,{\big (}a\notin B\ \leftrightarrow \,\langle a,0\rangle \in X_{B}{\big )}$

и так

${\big (}a\in B\lor a\notin B{\big )}\ \leftrightarrow \ \exists !(y\in \{0,1\}).\langle a,y\rangle \in X_{B}$.

Но имейте в виду, что в отсутствие каких-либо неконструктивных аксиом $a\in B$вообще может быть неразрешимым , поскольку требуется явное доказательство того или иного дизъюнкта. Конструктивно, когда $\exists (y\in \{0,1\}).\langle x,y\rangle \in X_{B}$ не может быть свидетелем всего $x\in A$, или уникальность терминов $y$ связанный с каждым $x$невозможно доказать, то и нельзя судить о том, что постигнутая совокупность полностью функциональна. Показательный пример: классический вывод Шредера-Бернштейна основан на анализе случаев, но для того, чтобы составить функцию , конкретные случаи на самом деле должны быть конкретизированы, учитывая любые входные данные из предметной области. Установлено, что Шрёдер–Бернштейн не может иметь доказательства на основе ${\mathsf {IZF}}$ плюс конструктивные принципы. Итак, поскольку интуиционистский вывод не выходит за рамки того, что формализовано здесь, не существует общей конструкции биекции из двух инъекций в противоположных направлениях.

Но будучи совместимым с ${\mathsf {ZF}}$, разработка в этом разделе по-прежнему всегда разрешает "функцию на $\omega$» следует интерпретировать как законченный объект, который также не обязательно задан как закономерная последовательность. Приложения можно найти в общих моделях утверждений о вероятности, например, в утверждениях, включающих понятие «данности» бесконечной случайной последовательности подбрасываний монеты, даже если многие прогнозы также могут быть выражены через спреды .

Если действительно дана функция $\chi _{B}\colon A\to \{0,1\}$, это характеристическая функция, фактически определяющая принадлежность к некоторому отделяемому подмножеству $B\subset A$ и

$B=\{n\in \omega \mid \chi _{B}(n)=1\}.$

Согласно соглашению, съемное подмножество $B$, $\chi _{B}$ а также любой эквивалент формул $n\in B$ и $\chi _{B}(n)=1$ (с $n$ свободный) может называться разрешимым свойством или устанавливаться на $A$.

Можно назвать коллекцию $A$ доступен для поиска $\chi _{B}$ если существование действительно разрешимо,

$\exists (x\in A).\chi _{B}(x)=1\ \lor \ \forall (x\in A).\chi _{B}(x)=0.$

Теперь рассмотрим случай $A=\omega$. Если $\chi _{B}(0)=0$скажем, тогда диапазон $\{0\}\subset R\subset \{0,1\}$ из $\chi _{B}$представляет собой обитаемый, подсчитанный набор путем замены. Однако $R$ не обязательно снова должно быть разрешимым множеством, поскольку утверждение $R=\{0\}$ эквивалентно довольно сильному $\forall n.\chi _{B}(n)=0$. Более того, $R=\{0\}$ также эквивалентно $B=\{\}$ и поэтому можно высказывать неразрешимые утверждения о $B$ также при членстве в $B$разрешимо. Это также происходит классически в том смысле, что утверждения о $B$ может быть независимой , но тогда любая классическая теория, тем не менее, утверждает совместное утверждение. $B=\{\}\lor \neg (B=\{\})$. Рассмотрим набор $B$ всех индексов доказательств несогласованности рассматриваемой теории, и в этом случае универсально замкнутое утверждение $B=\{\}$является утверждением о непротиворечивости. С точки зрения арифметических принципов, предположение о разрешимости этого было бы $\Pi _{1}^{0}$- ${\mathrm {PEM} }$ или арифметика $\forall$- ${\mathrm {PEM} }$. Это и более сильное родственное ${\mathrm {LPO} }$, или арифметика $\exists$- ${\mathrm {PEM} }$, обсуждается ниже.

Свидетель разлучения

Если существует предикат $P$ который различает два термина $x$ и $y$ в смысле $P(x)\land \neg P(y)$, то тождество принципа неразличимого означает, что они не совпадают. Это понятие может быть выражено теоретически: $x,y\in A$ могут считаться обособленными, если существует подмножество $B\subset A$так, что один является членом, а другой нет. Ограниченное отделяемыми подмножествами, это можно кратко сформулировать посредством количественной оценки функций. $\chi _{B}\in 2^{A}$. Действительно, $x=y$ уже отвергается, как только установлено, что не все функции $f$ уважать $f(x)=f(y)$. В этом духе можно на любом наборе $A$ определить логически положительное отношение обособленности

$x\,\#_{A}\,y\,:=\,\exists (f\in {\mathbb {N} }^{A}).f(x)\neq f(y)$.

Поскольку натуральные числа дискретны, сказанное здесь проявляется в теореме

$\neg \neg (x\,\#_{A}\,y)\to \neg (x=y)$.

Вычислимые множества

Возвращаясь к большей общности, учитывая общий предикат $Q$ относительно чисел (скажем, определенных из предиката T Клини ), пусть снова

$B:=\{n\in \omega \mid Q(n)\}.$

Учитывая любое естественное $n\in \omega$, затем

${\big (}Q(n)\lor \neg Q(n){\big )}\leftrightarrow {\big (}n\in B\lor n\notin B{\big )}.$

В классической теории множеств $\forall (n\in \omega ).Q(n)\lor \neg Q(n)$ к ${\mathrm {PEM} }$и поэтому исключенное среднее также справедливо и для членства в подклассе. Если класс $B$ не имеет числового ограничения, затем последовательно перебирает натуральные числа $n$, и таким образом "перечислить" все числа в $B$ просто пропуская те, у которых есть $n\notin B$, классически всегда представляет собой возрастающую сюръективную последовательность $b\colon \omega \twoheadrightarrow B$. Там можно получить биективную функцию . Таким образом, класс функций в типичных классических теориях множеств, как доказано, богат, поскольку он также содержит объекты, которые, как мы знаем, находятся за пределами того, что мы знаем как эффективно вычислимые или программно перечисляемые на практике.

В теории вычислимости вычислимые множества представляют собой образы неубывающих полных функций в рекурсивном смысле на уровне $\Sigma _{1}^{0}\cap \Pi _{1}^{0}=\Delta _{1}^{0}$арифметической иерархии и не выше. Выбор предиката на этом уровне означает решение задачи по конечному нахождению сертификата , который либо подтверждает, либо отклоняет членство. Поскольку не всякий предикат $Q$ вычислимо разрешима, а также теория ${\mathsf {CZF}}$ в одиночку не будет утверждать (доказывать), что все неограниченные $B\subset \omega$ являются областью значений некоторой биективной функции с областью определения $\omega$. См. также схему Крипке. Обратите внимание, что ограниченное разделение, тем не менее, доказывает, что более сложные арифметические предикаты по-прежнему составляют множества, причем следующим уровнем являются вычислимо перечислимые предикаты на уровне $\Sigma _{1}^{0}$.

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

Критерии ограниченности

Любое подмножество $B\subset \omega$ вводит в $\omega$. Если $B$ разрешима и населён $y_{0}\in B$, последовательность

$q:={\big \{}\langle x,y\rangle \in \omega \times B\mid (x\in B\land y=x)\lor (x\notin B\land y=y_{0}){\big \}}$

то есть

$q(x):={\begin{cases}x&x\in B\\y_{0}&x\notin B\\\end{cases}}$

является сюръективным на $B$, что делает его счетным набором. Эта функция также имеет свойство $\forall (x\in B).q(x)=x$.

Теперь рассмотрим счетное множество $R\subset \omega$ограниченное . в смысле, определенном ранее Любая последовательность, принимающая значения в $R$затем также ограничивается численно и, в частности, в конечном итоге не превышает тождественную функцию своих входных индексов. Формально,

$\forall (r\colon \omega \to R).\exists (m\in \omega ).\forall (k\in \omega ).k>m\to r(k)<k$

Множество $I$ так что это слабое ограничивающее утверждение справедливо для всех последовательностей, принимающих значения в $I$(или эквивалентную формулировку этого свойства) называется псевдоограниченным . Целью этого свойства будет сохранение этого $I\subset \omega$ в конечном итоге исчерпывается, хотя теперь это выражается в терминах функционального пространства $I^{\omega }$ (что больше, чем $I$ в смысле $I$ всегда вводит в $I^{\omega }$). , Соответствующее понятие знакомое из теории топологического векторного пространства, формулируется в терминах отношений, стремящихся к нулю для всех последовательностей ( ${\tfrac {r(k)}{k}}$в приведенных выше обозначениях). Для разрешимого обитаемого множества справедливость псевдоограниченности вместе с определенной выше последовательностью подсчетов дает оценку для всех элементов множества. $I$.

Принцип, согласно которому любое обитаемое псевдоограниченное подмножество $\omega$ которое просто счетно (но не обязательно разрешимо), всегда также ограничено, называется $\mathrm {BD}$- ${\mathbb {N} }$. Этот принцип также в целом соблюдается во многих конструктивных концепциях, таких как марковская базовая теория. ${\mathsf {HA}}+{\mathrm {ECT} }_{0}+{\mathrm {MP} }$, которая представляет собой теорию, постулирующую исключительно закономерные последовательности с хорошими свойствами завершения поиска чисел. Однако, $\mathrm {BD}$- ${\mathbb {N} }$ не зависит от ${\mathsf {IZF}}$.

Функции выбора

Даже не классический ${\mathsf {ZF}}$доказывает, что каждое объединение счетного множества двухэлементных множеств снова счетно. , модели Действительно ${\mathsf {ZF}}$определены такие , которые отрицают счетность такого счетного объединения пар. Если предположить, что счетный выбор исключает эту модель как интерпретацию полученной теории. Этот принцип по-прежнему не зависит от ${\mathsf {ZF}}$ - Наивная стратегия доказательства этого утверждения терпит неудачу при учете бесконечного числа экзистенциальных реализаций .

Принцип выбора постулирует, что определенные выборы всегда могут быть сделаны совместным образом в том смысле, что они также проявляются в теории как единая функция множества. Как и в случае с любой независимой аксиомой, это расширяет возможности доказательства, одновременно ограничивая объем возможных (теоретико-модельных) интерпретаций (синтаксической) теории. Утверждение о существовании функции часто можно перевести на существование обратных функций, упорядочений и т. д. Более того, выбор подразумевает утверждения о мощностях различных множеств, например, они подразумевают или исключают счетность множеств. Добавление полного выбора ${\mathsf {ZF}}$ не доказывает ничего нового $\Pi _{4}^{1}$-теоремы , но она строго неконструктивна, как показано ниже. Развитие здесь происходит независимо от любого из вариантов, описанных далее.

• Аксиома счетного выбора ${\mathrm {AC} _{\omega }}$ (или ${\mathrm {CC} }$): Если $g\colon \omega \to z$, можно сформировать набор отношений «один ко многим» $\{\langle n,u\rangle \mid n\in \omega \land u\in g(n)\}$. Аксиома счетного выбора предполагает, что всякий раз, когда $\forall (n\in \omega ).\exists u.u\in g(n)$, можно сформировать функцию, сопоставляющую каждое число с уникальным значением. Существование таких последовательностей вообще не доказуемо на основе ${\mathsf {ZF}}$ и счетный выбор не $\Sigma _{4}^{1}$- консервативен в отношении этой теории. Счетный выбор в общих множествах также может быть дополнительно ослаблен. Одним из распространенных соображений является ограничение возможных мощностей диапазона $g$, давая слабый счетный выбор в счетные, конечные или даже просто бинарные множества ( ${\mathrm {AC} _{\omega ,2}}$). Можно рассмотреть вариант счетного выбора функций в $\omega$ (называется ${\mathrm {AC} _{\omega ,\omega }}$ или ${\mathrm {AC} _{00}}$), что подразумевается конструктивным тезисным принципом Чёрча , то есть постулированием того, что все полные арифметические отношения рекурсивны. ${\mathrm {CT} _{0}}$в арифметике можно понимать как форму аксиомы выбора. Другим средством ослабления исчисляемого выбора является ограничение используемых определений относительно их места в синтаксических иерархиях (скажем, $\Pi _{1}^{0}$- ${\mathrm {AC} _{\omega ,2}}$). Слабая лемма Кенига. ${\mathrm {WKL} }$, что нарушает строго рекурсивную математику, как обсуждается ниже, сильнее, чем $\Pi _{1}^{0}$- ${\mathrm {AC} _{\omega ,2}}$и сам по себе иногда рассматривается как форма исчисляемого выбора. При наличии слабой формы счетного выбора лемма становится эквивалентной неконструктивному принципу более логического варианта: ${\mathrm {LLPO} }$. Конструктивно для корректных чисел Коши требуется слабая форма выбора . Счетный выбор недействителен во внутренней логике общего топоса , который можно рассматривать как модели конструктивных теорий множеств.
• Аксиома зависимого выбора ${\mathrm {DC} }$: Счетный выбор подразумевается более общей аксиомой зависимого выбора, извлекающей последовательность в обитаемом пространстве. $z$, учитывая любое целое отношение $R\subset z\times z$. В теории множеств эта последовательность снова представляет собой бесконечное множество пар, подмножество $\omega \times z$. Таким образом, можно перейти от нескольких утверждений о существовании к функциональному существованию, которое само по себе предоставляет утверждения об уникальном существовании для каждого естественного. Соответствующая формулировка зависимого выбора принята в некоторых конструктивных концепциях, например, в некоторых школах, которые понимают бесконечные последовательности как продолжающиеся конструкции, а не как завершенные объекты. По крайней мере, те случаи кажутся благоприятными, когда при любом $x\in z$, существование следующего значения $\exists (y\in z).xRy$может быть проверено вычислимым способом. Соответствующая рекурсивная функция $\omega \to z$, если он существует, тогда концептуализируется как способный возвращать значение при бесконечном количестве потенциальных входных данных. $n\in \omega$, но их не обязательно оценивать все вместе сразу. Это также справедливо во многих моделях реализуемости . В условии формально аналогичной теоремы о рекурсии на каждом шаге уже дан уникальный выбор, и эта теорема позволяет объединить их в функцию от $\omega$. Так же и с ${\mathrm {DC} }$ можно рассматривать формы аксиомы с ограничениями на $R$. С помощью аксиомы ограниченного разделения в ${\mathsf {ECST}}$, этот принцип также эквивалентен схеме с двумя ограниченными переменными-предикатами: сохранение всех кванторов в пределах $z$, можно еще больше сузить эту область множества, используя унарный $\Delta _{0}$-переменная-предикат, при этом также используя любую 2-арную $\Delta _{0}$-предикат вместо набора отношений $R$.
• Релятивизированный зависимый выбор ${\mathrm {RDC} }$: В этой схеме используются только два общих класса вместо того, чтобы требовать $z$ и $R$быть наборами. Область определения функции выбора, которая существует, по-прежнему всего лишь $\omega$. Над ${\mathsf {ECST}}$, это подразумевает полную математическую индукцию, которая, в свою очередь, позволяет определить функцию на $\omega$через схему рекурсии. Когда ${\mathrm {RDC} }$ ограничивается $\Delta _{0}$-определений, оно по-прежнему подразумевает математическую индукцию для $\Sigma _{1}$-предикаты (с квантором существования над множествами), а также ${\mathrm {DC} }$. В ${\mathsf {ZF}}$, схема ${\mathrm {RDC} }$ эквивалентно ${\mathrm {DC} }$.
• $\Pi \Sigma$- $\mathrm {AC}$: Семейством множеств лучше управлять, если оно индексируется функцией. Множество $b$ является базовым, если все индексированные семейства множеств $i_{s}\colon b\to s$ над ним есть функция выбора $f_{s}$, то есть $\forall (x\in b).f_{s}(x)\in i_{s}(x)$. Коллекция наборов холдинга $\omega$ и его элементы и который замыкается путем взятия индексированных сумм и произведений (см. зависимый тип ), называется $\Pi \Sigma$-закрыто. Хотя аксиома, что все сводится к минимуму $\Pi \Sigma$-закрытый класс - это основа, требующая некоторой работы, чтобы сформулировать, это самый сильный принцип выбора по сравнению с ${\mathsf {CZF}}$ что справедливо в теоретической интерпретации типа ${\mathsf {ML_{1}V}}$.
• Аксиома выбора ${\mathrm {AC} }$: Это постулат функции «полного» выбора, касающийся областей, которые являются общими множествами. $\{z,\dots \}$содержащие обитаемые множества, кодомены которых заданы как их общий союз. Учитывая набор множеств, в каждом из которых логика позволяет сделать выбор, аксиома допускает, что существует функция множества, которая совместно фиксирует выбор во всех. Обычно он формулируется для всех множеств, но также изучался в классических формулировках для множеств только до любой конкретной мощности. Стандартным примером является выбор во всех населенных подмножествах реальности, что классически соответствует области ${\mathcal {P}}_{\mathbb {R} }\setminus 1$. Для этой коллекции не может быть единого рецепта выбора элементов, который доказуемо представляет собой функцию выбора на основе ${\mathsf {ZF}}$. Кроме того, если ограничиться борелевской алгеброй действительных чисел, ${\mathsf {ZF}}$само по себе не доказывает существование функции, выбирающей член из каждого непустого такого измеримого по Лебегу подмножества . (Набор ${\mathcal {B}}({\mathbb {R} })$ — σ-алгебра , порожденная интервалами $I:=\{(x,y\,]\mid x,y\in {\mathbb {R} }\}$. Он строго включает в себя эти интервалы в смысле $I\subsetneq {\mathcal {B}}({\mathbb {R} })\subsetneq {\mathcal {P}}_{\mathbb {R} }$, но в ${\mathsf {ZF}}$ также имеет только мощность самой реальности.) Поразительных утверждений о существовании, подразумеваемых аксиомой, предостаточно. ${\mathsf {ECST}}$ доказывает $\omega$существует, и тогда аксиома выбора также подразумевает зависимый выбор. Что особенно важно в данном контексте, это, кроме того, также подразумевает случаи ${\mathrm {PEM} }$по теореме Дьяконеску. Форум ${\mathsf {ECST}}$ или теории, расширяющие его, это означает, что полный выбор, по крайней мере, доказывает ${\mathrm {PEM} }$ для всех $\Delta _{0}$-формулы, неконструктивное следствие, неприемлемое, например, с точки зрения вычислимости. Обратите внимание, что конструктивно лемма Цорна не подразумевает выбора: когда членство в функциональных областях неразрешимо, экстремальная функция, предоставляемая этим принципом, не всегда доказуемо является функцией выбора во всей области.

Теорема Диаконеску

Чтобы подчеркнуть силу полного выбора и его связь с вопросами интенциональности , следует рассмотреть классы

$a=\{u\in \{0,1\}\mid (u=0)\lor P\}$

$b=\{u\in \{0,1\}\mid (u=1)\lor P\}$

из доказательства теоремы Дьяконеску . Они так же случайны, как и предложение $P$участвуют в их определении, и они не являются конечными. Тем не менее, эта установка влечет за собой несколько последствий. Возвращаясь к вводному разъяснению значения столь удобного обозначения классов, а также принципа дистрибутивности , $t\in a\leftrightarrow {\big (}t=0\lor (t=1\land P){\big )}$. Так что безоговорочно, $0\in a$ а также $1\in b$, и в частности они населены. Как $\neg (0=1)$ в любой модели арифметики Гейтинга, используя дизъюнктивный силлогизм как $0\in b$ и $1\in a$ каждый подразумевает $P$. Оба утверждения действительно эквивалентны предложению, как ясно $P\to (a=\{0,1\}\land b=\{0,1\})$. Последний также говорит о том, что обоснованность $P$ означает $a$ и $b$разделите все члены, а их два. Как $a$ являются $b$ тогда множества также $P\to (a=b\land \{a,b\}=\{a\})$по экстенсиональности. И наоборот, если предположить, что они равны, это означает $x\in a\leftrightarrow x\in b$ для любого $x$, проверяя все заявления о членстве. Таким образом, как утверждения о принадлежности, так и равенства оказываются эквивалентными $P$. Использование контрапозитивов приводит к более слабой эквивалентности дизъюнктов. $(P\lor \neg P)\leftrightarrow (a=b\lor \neg (a=b))$. Конечно, явно $\neg P\to (a=\{0\}\land b=\{1\})$и таким образом можно обнаружить, каким образом наборы могут оказаться разными. Поскольку функции сохраняют равенство по определению, $\neg {\big (}g(a)=g(b){\big )}\to \neg P$ действительно справедливо для любого $g$ с доменом $\{a,b\}$.

В дальнейшем предположим контекст, в котором $a,b$действительно установлено, что они являются множествами и, следовательно, субконечными множествами. Общая аксиома выбора утверждает существование функции $f\colon \{a,b\}\to a\cup b$ с $f(z)\in z$. Важно, чтобы элементы $a,b$ области определения функции отличаются от натуральных чисел $0,1$в том смысле, что о первом априори известно меньше. Образуя затем объединение двух классов, $u=0\lor u=1$является необходимым, но и достаточным условием. Таким образом $a\cup b=\{0,1\}$ и мы имеем дело с функциями $f$в набор двух различимых значений. С выбором приходит соединение $f(a)\in a\land f(b)\in b$ в кодомене функции, но возможные возвращаемые значения функции просто известно, что $0$ или $1$. Используя дистрибутивность, возникает список условий, еще одна дизъюнкция. Расширяя то, что тогда установлено, можно обнаружить, что либо оба $P$ а также равенство наборов или что возвращаемые значения различны и $P$может быть отклонено. Вывод состоит в том, что постулат выбора фактически подразумевает $P\lor \neg P$ всякий раз, когда аксиома разделения позволяет понять множество, используя неразрешимое предложение $P$.

Диаконеску

Таким образом, полный выбор неконструктивен в теории множеств, как это определено здесь. Проблема в том, что когда предложения являются частью понимания множества (например, когда $P$ используется для разделения и тем самым определения классов $a$ и $b$ от $\{0,1\}$), понятие их истинностных значений разветвляется на устоявшиеся термины теории. Равенство, определяемое установленной теоретической аксиомой экстенсиональности , которая сама по себе не связана с функциями, в свою очередь связывает знания о предложении с информацией о значениях функций. Подведем итоги последнего шага с точки зрения значений функций: с одной стороны, свидетельствование $f(a)=1$ подразумевает $P$ и $a=b$ и этот вывод независимо также относится и к свидетельствованию $f(b)=0$. С другой стороны, будучи свидетелем $f(a)=0\land f(b)=1$ подразумевает, что два аргумента функции не равны, и это исключает $P$. На самом деле комбинаций всего три, поскольку аксиома экстенсиональности в данной ситуации делает $f(a)=1\land f(b)=0$непоследовательный. Таким образом, если нужно сохранить конструктивное прочтение существования, в теории множеств может не быть принят полный выбор, поскольку простое утверждение о существовании функции не реализует конкретную функцию.

Чтобы лучше понять, почему нельзя ожидать предоставления окончательной (полной) функции выбора с доменом $\{a,b\}$, рассмотрите кандидатов наивных функций. Во-первых, необходимо провести анализ предметной области. Сюръекция $\{\langle 0,a\rangle ,\langle 1,b\rangle \}$ свидетели того, что $\{a,b\}$конечно индексируется. Было отмечено, что ее члены являются субконечными и также обитаемыми, поскольку независимо от $P$ это тот случай, что $0\in a$ и $1\in b$. Казалось бы, это так наивно, $f=\{\langle a,0\rangle ,\langle b,1\rangle \}$претендент на функцию выбора. Когда $P$можно отклонить, то это действительно единственный вариант. Но в случае доказуемости $P$, когда $\{a,b\}=\{a\}$, существует только одна возможная входная функция для функции выбора. Таким образом, в этой ситуации функция выбора явно будет иметь тип $f\colon \{a\}\to \{0,1\}$, например $f=\{\langle a,0\rangle \}$и это исключило бы первоначального претендента. Для общего $P$, область определения потенциальной функции выбора не конкретна, а зависит от $P$и не доказано, что конечный. При рассмотрении вышеизложенного функционального назначения $f(a)=0$, то ни одно безоговорочно заявляя $f(b)=1$ ни $f(b)=0$обязательно является последовательным. Определив $1$ с $\{0\}$, два кандидата, описанные выше, могут быть представлены одновременно через $f=\{\langle a,0\rangle ,\langle b,B_{\neg }\rangle \}$ (которое также не доказывается конечным) с субконечным «истинным значением $\neg P$"данный как $B_{\neg }:=\{u\in \{0\}\mid \neg P\}$. Как $(P\to (B_{\neg }=0))\land (\neg P\to (B_{\neg }=1))$, постулируя $P$, или $\neg P$или классический принцип $P\lor \neg P$ здесь действительно подразумевало бы, что $B_{\neg }$ является естественным, так что последнее множество $f$ представляет собой функцию выбора в $\{0,1\}$. И, как и в конструктивном случае, имея конкретную функцию выбора (множество, содержащее ровно одну или ровно две пары), можно фактически сделать вывод, $P$ или ли $\neg P$держится. И наоборот, третий и последний кандидат $f=\{\langle b,1\rangle \}$ может быть захвачен как часть $f=\{\langle a,B\rangle ,\langle b,1\rangle \}$, где $B:=\{u\in \{0\}\mid P\}$. Такой $B$уже рассматривалось в начале раздела об аксиоме разделения. Опять же, последнее $f$ вот классическая функция выбора в любом случае, где $P$функционирует как (потенциально неразрешимое) «предложение if». Конструктивно область применения и значения таких $P$-зависимые потенциальные функции недостаточно поняты, чтобы доказать, что они являются тотальным функциональным отношением в $\{0,1\}$.

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

Регулярность

Аксиома выбора допускает существование функции, связанной с каждым набором обитаемых элементов заданного размера. $s$, с помощью которого можно сразу подобрать уникальные элементы $t$. Аксиома регулярности гласит, что для любого обитаемого множества $s$ в универсальной коллекции существует элемент $t$ в $s$, который не имеет общих элементов с $s$. Эта формулировка не включает в себя функции или уникальные утверждения о существовании, а вместо этого напрямую гарантирует множества. $t\in s$с определенным свойством. Поскольку аксиома соотносит заявления о членстве разного ранга, она также в конечном итоге подразумевает, что ${\mathrm {PEM} }$:

В доказательстве из «Выбора» выше использовалось $1:=\{0\}$ и конкретный набор $\{a,b\}$. Доказательство в этом параграфе также предполагает, что Разделение применимо к $P$ и использует $b$, для которого $\{0\}\in b$по определению. Уже было разъяснено, что $P\leftrightarrow 0\in b$ и поэтому можно оказаться исключенным средним для $P$ в виде $0\in b\lor 0\notin b$. Теперь позвольте $t\in b$быть постулируемым членом со свойством пустого пересечения. Набор $b$ был определен как подмножество $\{0,1\}$ и так любой данный $t\in b$ выполняет дизъюнкция $t=0\lor t=1$. Левое предложение $t=0$ подразумевает $0\in b$, а для правильного предложения $t=1$ можно использовать специальный непересекающийся элемент $t$ выполняет $(t=\{0\})\leftrightarrow (0\notin b)$.

Требование, чтобы множество натуральных чисел было хорошо упорядочено по отношению к нему, стандартное отношение порядка налагает то же условие на обитаемое множество. $b\subset \omega$. Таким образом, принцип наименьшего числа имеет тот же неконструктивный смысл. Как и в случае с доказательством из «Выбора», объем предложений, для которых справедливы эти результаты, определяется аксиомой разделения.

Арифметика

Четыре аксиомы Пеано для $0$ и $S$, характеризующий множество $\omega$ как модель натуральных чисел в конструктивной теории множеств ${\mathsf {ECST}}$, обсуждались. Приказ " $<$"натуральных чисел определяется членством" $\in$" в этой модели фон Неймана и это множество дискретно, т.е. $\phi (n,m):=(n=m)$ разрешимо.

Как уже говорилось, индукция по арифметическим формулам является теоремой. Однако, если не предполагать полную математическую индукцию (или более сильные аксиомы, такие как полное разделение) в теории множеств, существует ловушка, связанная с существованием арифметических операций. Теория первого порядка арифметики Гейтинга ${\mathsf {HA}}$ имеет ту же сигнатуру и нелогические аксиомы, что и арифметика Пеано. ${\mathsf {PA}}$. Напротив, сигнатура теории множеств не содержит сложения». $+$"или умножение" $\times$". ${\mathsf {ECST}}$ на самом деле не включает примитивную рекурсию в $\omega$ для определения функций того, что будет $h\colon (x\times \omega )\to y$ (где " $\times$"здесь обозначает декартово произведение множества, не путать с приведенным выше умножением). Действительно, несмотря на наличие аксиомы замены, теория не доказывает существования множества, фиксирующего функцию сложения. $+\colon (\omega \times \omega )\to \omega$. В следующем разделе выясняется, какая аксиома теории множеств может быть утверждена для доказательства существования последних как функционального множества вместе с их желаемым отношением к нулю и преемнику.

Полученная модель арифметики выходит далеко за пределы предиката равенства.

${\mathsf {HA}}\vdash \forall n.\forall m.{\big (}\phi (n,m)\lor \neg \phi (n,m){\big )}$

для любой бескванторной формулы. Действительно, ${\mathsf {PA}}$ является $\Pi _{2}^{0}$-консервативный ${\mathsf {HA}}$ и исключение двойного отрицания возможно для любой формулы Харропа .

Арифметические функции из рекурсии

Делаем шаг за пределы ${\mathsf {ECST}}$, необходимо добавить аксиому, предоставляющую определение функций множества через функции множества итерационного шага: Для любого множества $y$, набор $z\in y$ и $f\colon y\to y$, также должна существовать функция $g\colon \omega \to y$ достигается за счет использования первого, а именно так, что $g(0)=z$ и $g(Sn)=f(g(n))$. Этот принцип итерации или рекурсии подобен теореме о трансфинитной рекурсии , за исключением того, что он ограничен функциями множества и конечными порядковыми аргументами, т.е. здесь нет пункта о предельных ординалах . Он функционирует как теоретико-множественный эквивалент объекта натуральных чисел в теории категорий . Это позволяет получить полную интерпретацию арифметики Гейтинга. ${\mathsf {HA}}$ в нашей теории множеств, включая функции сложения и умножения.

С этим, ${\mathbb {N} }$ и ${\mathbb {Z} }$обоснованы в смысле формулировки индуктивных подмножеств . Далее, арифметика рациональных чисел ${\mathbb {Q} }$ тогда также можно определить и доказать его свойства, такие как единственность и счетность.

Рекурсия из

Напомним, что $h\simeq y^{x}$ это сокращение от $\forall f.{\big (}f\in h\leftrightarrow f\in y^{x}{\big )}$, где $f\in y^{x}$является сокращением от предиката общей функции, предложения с точки зрения использования ограниченных кванторов. Если обе стороны являются множествами, то по экстенсиональности это также эквивалентно $h=y^{x}$. (Хотя и из-за небольшого злоупотребления формальными обозначениями, как в случае с символом « $\in$", символ " $=$" в любом случае также часто используется с классами.)

Теория множеств с ${\mathsf {HA}}$-модель, обеспечивающая принцип рекурсии, изложенный выше, также докажет, что для всех натуральных чисел $n$ и $m$, функциональные пространства

${\{0,1,\dots ,n-1\}}\to {\{0,1,\dots ,m-1\}}$

представляют собой наборы. Действительно, достаточно ограниченной рекурсии, т.е. принципа $\Delta _{0}$-определенные классы.

И наоборот, принцип рекурсии можно доказать на основе определения, включающего объединение рекурсивных функций на конечных областях. Для этого важен класс частичных функций на $\omega$ так, что все его члены имеют возвращаемые значения только до некоторого натурального числа, которое может быть выражено выражением $\cup _{n\in \omega }y^{\{0,1,\dots ,n-1\}}$. Существование этого набора становится доказуемым, если предположить, что отдельные функциональные пространства $y^{n}$все формы устанавливаются сами собой. С этой целью

Возведение в степень для конечных областей $\forall (n\in \omega ).\forall y.\ \ \exists h.h\simeq y^{n}$

Согласно этой аксиоме, любое такое пространство теперь представляет собой набор подмножеств $n\times y$и это строго слабее, чем полное разделение. Примечательно, что принятие этого принципа имеет подлинный теоретический оттенок, в отличие от прямого внедрения арифметических принципов в нашу теорию. И это скромный принцип, поскольку эти функциональные пространства являются ручными: если вместо этого предположить полную индукцию или полное возведение в степень, принимая $y$ для функциональных пространств $y^{n}$, или к n-кратным декартовым произведениям, доказуемо сохраняет счетность.

В ${\mathsf {ECTS}}$плюс конечное возведение в степень, принцип рекурсии является теоремой. Более того, теперь также можно доказать перечислимые формы принципа «ячейки» , например, что на множестве с конечной индексацией каждая автоинъекция также является сюръекцией. Как следствие, мощность конечных множеств, т. е. конечный ординал фон Неймана, доказуемо единственна. Дискретные множества с конечной индексацией — это всего лишь конечные множества. В частности, конечно индексированные подмножества $\omega$конечны. Факторы или бинарное объединение или декартово произведение двух множеств сохраняют конечность, субконечность и конечную индексацию.

Перечисленные до сих пор аксиомы теории множеств включают в себя арифметику первого порядка и достаточны в качестве формализованной основы для значительной части общей математики. Ограничение на конечные области снимается в строго более сильной аксиоме возведения в степень, приведенной ниже. Однако эта аксиома также не влечет за собой ни полную схему индукции для формул с несвязанными кванторами в области множеств, ни принцип зависимого выбора. Аналогично, существуют принципы Коллекции, которые конструктивно не подразумеваются Заменой, как обсуждается ниже. Следствием этого является то, что для некоторых утверждений более высокой сложности или косвенности, даже если конкретные представляющие интерес случаи вполне доказуемы, теория может не доказать универсальное замыкание. Более сильной, чем эта теория с конечным возведением в степень, является ${\mathsf {ECTS}}$плюс полная индукция. Это подразумевает принцип рекурсии даже для классов и такое, что $g$является уникальным. Уже этот принцип рекурсии, ограниченный $\Delta _{0}$ доказывает конечное возведение в степень, а также существование транзитивного замыкания для каждого множества относительно $\in$ (поскольку создание профсоюза $\Delta _{0}$). При этом более распространенные конструкции сохраняют счетность. Общие объединения над конечно индексированным множеством конечно индексированных множеств снова конечно индексируются, если, по крайней мере, предположить индукцию для $\Sigma _{1}$-предикаты (относительно языка теории множеств, и это тогда справедливо независимо от разрешимости их отношений равенства.)

Индукция без бесконечных множеств

Прежде чем обсуждать даже классически неисчисляемые множества, в этом последнем разделе мы делаем шаг назад, в контекст, более близкий к ${\mathsf {BCST}}$. Сложение чисел, рассматриваемое как отношение троек, представляет собой бесконечную коллекцию, как и совокупность самих натуральных чисел. Но обратите внимание, что схемы индукции могут быть приняты (для множеств, порядковых чисел или в сочетании с сортировкой натуральных чисел), даже не постулируя, что набор натуральных чисел существует как набор. Как уже отмечалось, арифметика Гейтинга ${\mathsf {HA}}$ такой двояко интерпретируется конструктивной теорией множеств, в которой постулируется, что все множества находятся в биекции с порядковым номером. — Предикат BIT это распространенное средство кодирования множеств в арифметике.

В этом параграфе перечислены несколько слабых принципов индукции натуральных чисел, изучаемых в теории доказательств арифметических теорий со сложением и умножением в их сигнатуре. Это структура, в которой эти принципы понимаются наиболее хорошо. Теории могут определяться посредством ограниченных формулировок или вариаций индукционных схем , которые, кроме того, могут допускать только предикаты ограниченной сложности. С точки зрения классической стороны первого порядка это приводит к теориям между арифметикой Робинсона ${\mathsf {Q}}$ и арифметика Пеано ${\mathsf {PA}}$: Теория ${\mathsf {Q}}$ не имеет индукции. ${\mathsf {PA}}$ имеет полную математическую индукцию для арифметических формул и имеет порядковый номер $\varepsilon _{0}$, что означает, что теория позволяет кодировать ординалы более слабых теорий как рекурсивное отношение только к натуральным числам. Теории могут также включать дополнительные символы для определенных функций. Многие из хорошо изученных арифметических теорий слабы в отношении доказательства полноты некоторых более быстро растущих функций . Некоторые из самых основных примеров арифметики включают арифметику элементарных функций. ${\mathsf {EFA}}$, который включает в себя индукцию для ограниченных арифметических формул, здесь имеется в виду с кванторами в диапазонах конечных чисел. Теория имеет теоретико-доказательный ординал (наименьший не доказанное рекурсивное упорядочение ) $\omega ^{3}$. $\Sigma _{1}^{0}$Схема -индукции для арифметических формул существования позволяет проводить индукцию для тех свойств натуральных чисел, проверка которых вычислима с помощью конечного поиска с неограниченным (любым, но конечным) временем выполнения. Схема также классически эквивалентна схеме $\Pi _{1}^{0}$-индукционная схема. Относительно слабая классическая арифметика первого порядка, использующая эту схему, обозначается ${\mathsf {I\Sigma }}_{1}$и доказывает сумму примитивно-рекурсивных функций. Теория ${\mathsf {I\Sigma }}_{1}$ является $\Pi _{2}^{0}$-консервативность по отношению к примитивно-рекурсивной арифметике ${\mathsf {PRA}}$. Обратите внимание, что $\Sigma _{1}^{0}$-индукция также является частью второго порядка. обратной математики базовой системы ${\mathsf {RCA}}_{0}$, другие его аксиомы ${\mathsf {Q}}$ плюс $\Delta _{1}^{0}$-понимание подмножеств натуральных чисел. Теория ${\mathsf {RCA}}_{0}$ является $\Pi _{1}^{1}$-консервативный ${\mathsf {I\Sigma }}_{1}$. Все последние упомянутые арифметические теории имеют порядковый номер. $\omega ^{\omega }$.

Отметим еще один шаг за пределы $\Sigma _{1}^{0}$-индукционная схема. Отсутствие более сильных схем индукции означает, например, что некоторые неограниченные версии принципа ячейки недоказуемы. Одно из относительно слабых утверждений — утверждение типа теоремы Рамсея, выраженное здесь следующим образом: для любого $m>0$ и кодирование карты-раскраски $f$, связывая каждый $n\in \omega$ с цветом $\{0,1,\dots ,m-1\}$, это не тот случай, когда для каждого цвета $c<m$ существует пороговый входной номер $n_{c}$ за пределами которого $c$больше никогда не является возвращаемым значением сопоставления. (В классическом контексте и в терминах множеств это утверждение о раскраске можно сформулировать положительно, как утверждая, что всегда существует хотя бы одно возвращаемое значение. $k$ такое, что, по сути, для некоторой неограниченной области $K\subset \omega$ он утверждает, что $\forall (n\in K).f(n)=k$. На словах, когда $f$ предоставляет бесконечные перечисляемые присваивания, каждое из которых относится к одному из $m$ различных возможных цветов, утверждается, что конкретный $k$ раскраска бесконечного числа чисел всегда существует и что таким образом набор можно указать, даже не проверяя свойства $f$. Если читать конструктивно, хотелось бы $k$Чтобы формально переформулировать такое отрицание (утверждение типа теоремы Рамсея в исходной формулировке выше) и доказать его, необходима более высокая косвенность, чем при индукции для простых экзистенциальных утверждений. А именно переформулировать проблему в терминах отрицания существования одного совместного порогового числа, зависящего от всех гипотетических $n_{c}$s, после чего функция все равно должна будет получить некоторое значение цвета. Более конкретно, сила требуемого ограничивающего принципа находится строго между схемой индукции в ${\mathsf {I\Sigma }}_{1}^{0}$ и ${\mathsf {I\Sigma }}_{2}^{0}$. Для свойств с точки зрения возвращаемых значений функций в конечных областях проверка методом грубой силы путем проверки всех возможных входных данных требует вычислительных затрат, которые больше для больших областей, но всегда конечны. Принятие индукционной схемы, как в ${\mathsf {I\Sigma }}_{2}^{0}$ подтверждает первый так называемый принцип бесконечной ячейки, который касается неограниченных областей и, следовательно, касается отображений с бесконечным количеством входных данных.

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

Возведение в степень

Классический ${\mathsf {ZFC}}$ без аксиомы Powerset имеет естественные модели в классах множеств наследственного размера меньше, чем некоторые несчетные кардиналы. В частности, это по-прежнему согласуется с тем, что все существующие множества (включая множества, содержащие вещественные числа) являются подсчетными , а там даже счетными. Такая теория по существу сводится к арифметике второго порядка . Все множества, являющиеся счетными, могут быть конструктивно непротиворечивы даже в нынешнем виде несчетных множеств.

Обсуждались возможные принципы выбора, уже была принята ослабленная форма схемы разделения и больше стандартных ${\mathsf {ZFC}}$аксиомы должны быть ослаблены для более предикативной и конструктивной теории. Первой из них является аксиома Powerset, принятая в виде пространства характеристических функций. Следующая аксиома ${\mathrm {Exp} }$ строго сильнее, чем его подвеска для конечных областей, обсуждавшихся выше:

Возведение в степень $\forall x.\forall y.\ \ \exists h.h\simeq y^{x}$

В формулировке здесь снова используются удобные обозначения функциональных пространств, как обсуждалось выше. На словах аксиома гласит, что даны два множества $x,y$, класс $y^{x}$всех функций, по сути, тоже множество. Это, безусловно, необходимо, например, для формализации карты объекта внутреннего hom-функтора типа ${\mathrm {hom} }({\mathbb {N} },-).$

Приняв такое утверждение о существовании, можно также определить количественную оценку. $\forall f$над элементами определенных классов (всего) функций теперь распространяются только по множествам. Рассмотрим набор пар $\langle a,b\rangle \in x\times x$ проверка отношения обособленности $\exists (f\in {\mathbb {N} }^{x}).f(a)\neq f(b)$. Через ограниченное разделение теперь это подмножество $x\times x$. Эти примеры показывают, что аксиома возведения в степень не только напрямую обогащает область множеств, но посредством разделения также позволяет получить еще больше множеств, что, кроме того, также усиливает другие аксиомы.

Примечательно, что эти ограниченные кванторы теперь распространяются на функциональные пространства, которые доказуемо неисчислимы и, следовательно, даже классически неисчислимы. Например, совокупность всех функций $f\colon \omega \to 2$ где $2:=SS0=\{0,1\}$, то есть набор $2^{\mathbb {N} }$точек, лежащих в основе пространства Кантора , несчетно в силу диагонального аргумента Кантора и в лучшем случае может считаться подсчетным множеством. В этой теории теперь можно также количественно оценивать подпространства таких пространств, как $2^{\mathbb {N} }$, что является понятием третьего порядка натуральных чисел. (В этом разделе и далее используется символ полукольца натуральных чисел в таких выражениях, как $y^{\mathbb {N} }$ используется или пишется $\omega \to y$, просто чтобы избежать смешения кардинального- с порядковым возведением в степень.) Грубо говоря, классически несчетные множества, такие как, например, эти функциональные пространства, как правило, не имеют вычислимо разрешимого равенства.

Подняв общий профсоюз над $x$-индексированное семейство $\{y_{i}\}_{i}$, а также зависимый или индексированный продукт, написанный $\Pi _{i\in x}\,y_{i}$, теперь является набором. Для постоянного $y_{i}$, это снова сводится к функциональному пространству $y^{x}$. И принимая общее объединение над самими функциональными пространствами, всякий раз, когда класс мощности $x$ это набор, то также надмножество $\cup _{s\subset x}y^{s}$ из $y^{x}$ теперь является набором, дающим возможность говорить о пространстве частичных функций на $x$.

Союзы и счетность

С помощью возведения в степень теория доказывает существование любой примитивно-рекурсивной функции в $x\times \omega \to y$, и в частности в несчетных функциональных пространствах из $\omega$. Действительно, используя функциональные пространства и конечные ординалы фон Неймана в качестве областей, мы можем моделировать ${\mathsf {HA}}$как обсуждалось, и, таким образом, кодируют порядковые номера в арифметике. Кроме того, можно получить порядковое число, возведенное в степень $\omega ^{\omega }$ как совокупность, которую можно охарактеризовать как $\cup _{n\in \omega }\omega ^{n}$, подсчитанный набор слов в бесконечном алфавите . Объединение всех конечных последовательностей над счетным множеством теперь является счетным множеством. Кроме того, для любого счетного семейства считающих функций вместе с их диапазонами теория доказывает, что объединение этих диапазонов счетно. Напротив, не предполагая счетного выбора, даже ${\mathsf {ZF}}$ согласовано с несчетным множеством ${\mathbb {R} }$ является объединением счетного множества счетных множеств.

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

Наконец, с возведением в степень любое конечно индексированное объединение семейства субконечно индексированных соотв. подсчетные множества сами по себе субконечно индексированы, соответственно. также счетно. Теория также доказывает совокупность всех счетных подмножеств любого множества. $x$быть самим набором. Что касается этого подмножества класса мощности ${\mathcal {P}}_{x}$, некоторые вопросы естественной мощности также классически могут быть решены только с помощью выбора, по крайней мере, для несчетных чисел. $x$.

Класс всех подмножеств набора

Учитывая последовательность наборов, можно определить новые такие последовательности, например, в $\langle a,b\rangle \mapsto \langle \langle \rangle ,\langle a\rangle ,\langle b\rangle ,\langle a,b\rangle \rangle$. Но примечательно, что в рамках математической теории множеств совокупность всех подмножеств множества определяется не восходящим построением из его составляющих, а посредством понимания всех множеств в области дискурса. Стандартная автономная характеристика класса мощности набора. $x$ предполагает неограниченную универсальную количественную оценку, а именно $\forall u.\left(u\in {\mathcal {P}}_{x}\leftrightarrow u\subset x\right)$, где $\subset$ ранее было определено также в терминах предиката членства $\in$. Здесь утверждение, выраженное как $\forall (u\in {\mathcal {P}}_{x}).Q(x)$ априори следует принять за $\forall u.{\big (}u\subset x\to Q(x){\big )}$и не эквивалентно ограниченному множеству высказыванию. Действительно, заявление $y={\mathcal {P}}_{x}$ сам по себе $\Pi _{1}$. Если ${\mathcal {P}}_{x}$ является набором, то определяющая количественная оценка даже варьируется в пределах ${\mathcal {P}}_{x}$, что делает аксиому powerset недопустимой .

Напомним, что член множества характеристических функций $2^{x}$ соответствует предикату, разрешимому на множестве $x$, что, таким образом, определяет отделяемое подмножество $s\subset x$. В свою очередь, класс ${\mathcal {D}}_{x}\subset {\mathcal {P}}_{x}$ всех отделяемых подмножеств $x$теперь тоже в комплекте, через замену. Однако, ${\mathcal {D}}_{x}$ может не обладать желаемыми свойствами, например, быть замкнутым при бесконечных операциях, таких как объединения над счетными бесконечными наборами индексов: для счетной последовательности $u_{n}\in {\mathcal {D}}_{x}$, подмножество $U:=\cup _{k\in \omega }u_{k}$ из $x$ проверка $(a\in U)\leftrightarrow \exists (m\in \omega ).a\in u_{m}$ для всех $a\in x$существует как набор. Но он может оказаться неотделимым и, следовательно, не обязательно сам по себе является доказуемо членом ${\mathcal {D}}_{x}$. Между тем, согласно классической логике, все подмножества множества $x$ являются тривиально отделяемыми, то есть ${\mathcal {D}}_{x}={\mathcal {P}}_{x}$ а потом ${\mathcal {D}}_{x}$конечно, содержит любое подмножество. Кроме того, в классической логике это означает, что возведение в степень превращает класс мощности в набор.

Перевод результатов математических теорий, основанных на теории множеств, таких как топология множества точек или теория меры, в конструктивную структуру — это тонкая процедура взад и вперед. Например, в то время как ${\mathcal {D}}_{x}$является полем множеств , для того чтобы оно образовало σ-алгебру по определению, также требуется упомянутая выше замкнутость относительно объединений. Но хотя область подмножеств может не проявлять конструктивного свойства замыкания, классическая мера $\mu$ является непрерывным снизу , и поэтому его значение в бесконечном объединении в любом случае может быть выражено без ссылки на этот набор как на вход функции, а именно как $\lim _{n\to \infty }$ растущей последовательности $\mu (\cup _{k\leq n}u_{k})$ значений функции в конечных объединениях.

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

Богатство полного степенного класса в теории без исключенного третьего лучше всего можно понять, рассматривая небольшие классически конечные множества. Для любого предложения $P$, рассмотрим подкласс $B:=\{x\in 1\mid P\}$ из $1$ (т.е. $\{0\}$ или $S0$). Это равно $B=0$ когда $P$ можно отклонить и оно равно $B=1$ (т.е. $B=S0$), когда $P$можно доказать. Но $P$может быть вообще неразрешимой. Рассмотрим три различных неразрешимых утверждения, ни одно из которых с доказанной точностью не подразумевает другое. Их можно использовать для определения трех подклассов синглтона. $1$, ни один из которых не является доказанно одинаковым. С этой точки зрения класс мощности ${\mathcal {P}}_{1}$ синглтона, обычно обозначаемого $\Omega$, называется истинностного значения алгеброй и не обязательно состоит только из двух элементов.

С возведением в степень, классом мощности синглтона, ${\mathcal {P}}_{1}$, будучи набором, уже подразумевает Powerset для наборов в целом. Доказательство проводится путем замены ассоциации $f\in {{\mathcal {P}}_{1}}^{x}$ к $\{z\in x\mid 0\in f(z)\}\in {\mathcal {P}}_{x}$и аргумент, почему охватываются все подмножества. Набор $2^{x}$ вводит в функциональное пространство ${{\mathcal {P}}_{1}}^{x}$ также.

Если теория подтвердится $B$ выше набора (например, ${\mathsf {IZF}}$ безусловно делает), то подмножество $b:=\{\langle 0,B\rangle \}$ из $1\times {\mathcal {P}}_{1}$ это функция $b\colon 1\to {\mathcal {P}}_{1}$ с ${\big (}b(0)=1{\big )}\leftrightarrow P$. Утверждать, что ${\mathcal {P}}_{1}=2$ состоит в том, чтобы утверждать, что исключенное среднее справедливо для $P$.

Было отмечено, что пустое множество $0$ и набор $1$ само по себе, конечно, представляет собой два подмножества $1$, значение $2\subset {\mathcal {P}}_{1}$. Также ли ${\mathcal {P}}_{1}\subset 2$ истинность теории зависит от простой дизъюнкции:

${\big (}\forall (x\in {\mathcal {P}}_{1}).(0\in x\lor 0\notin x){\big )}\to \,{\mathcal {P}}_{1}\subset 2$.

Итак, предполагая ${\mathrm {PEM} }$ для просто ограниченных формул предикативное разделение позволяет продемонстрировать, что степенной класс ${\mathcal {P}}_{1}$это набор. Итак, в этом контексте полный выбор также подтверждает Powerset. (В контексте ${\mathsf {IZF}}$, ограниченное исключенное среднее фактически уже превращает теорию множеств в классическую, как обсуждается ниже.)

Полное разделение эквивалентно простому предположению, что каждый отдельный подкласс $1$это набор. Если предположить полное разделение, то и полный выбор, и закономерность окажутся ${\mathrm {PEM} }$.

Предполагая ${\mathrm {PEM} }$ в этой теории индукция множества становится эквивалентной регулярности, а замена становится способной доказать полное разделение.

Обратите внимание, что кардинальные отношения, включающие несчетные множества, также неуловимы в ${\mathsf {ZFC}}$, где характеристика несчетности упрощается до $|\omega |<|x|$. Например, относительно несчетной степени $2^{|\omega |}$, от этой классической теории не зависит, все ли такие $x$ иметь $2^{|\omega |}\leq |x|$и это не доказывает, что $2^{|\omega |}<2^{|x|}$. См. гипотезу континуума и связанную с ней теорему Истона .

теории категорий

Таким образом, в этом контексте с возведением в степень арифметика первого порядка имеет модель, и все функциональные пространства между множествами существуют. Последние более доступны, чем классы, содержащие все подмножества множества, как в случае с экспоненциальными объектами, соответственно. подобъекты в теории категорий. С точки зрения теории категорий , теория ${\mathsf {BCST}}+{\mathrm {Exp} }$по существу соответствует конструктивно четкому декартову замкнутому Хейтинга пред- топу (всякий раз, когда принимается Бесконечность) с объектом натуральных чисел . Существование powerset — это то, что превратило бы претопос Хейтинга в элементарный топос . Каждый такой топос, который интерпретирует ${\mathsf {ZF}}$это, конечно, модель этих более слабых теорий, но были определены локально декартовы закрытые предлоги, которые, например, интерпретируют теории с возведением в степень, но отвергают полное разделение и набор степеней. Форма ${\mathrm {PEM} }$соответствует любому подобъекту, имеющему дополнение, и в этом случае мы называем топос логическим. Теорема Диаконеску в своей исходной топосной форме утверждает, что это справедливо тогда и только тогда, когда любой коэквалайзер двух непересекающихся мономорфизмов имеет сечение. Последнее является формулировкой выбора . Теорема Барра утверждает, что любой топос допускает сюръекцию из булева топоса на него, что относится к классическим утверждениям, доказуемым интуиционистски.

В теории типов выражение « $x\to y$" существует сам по себе и обозначает функциональные пространства - примитивное понятие. Эти типы (или, в теории множеств, классы или множества) естественным образом появляются, например, как тип карринговой биекции между $(z\times x)\to y$ и $z\to y^{x}$, дополнение . Типичная теория типов с возможностью общего программирования – и, конечно же, такая, которая может моделировать ${\mathsf {CZF}}$, которая считается конструктивной теорией множеств – будет иметь тип целых чисел и функциональных пространств, представляющих ${\mathbb {Z} }\to {\mathbb {Z} }$, и как таковые также включают неисчисляемые типы. Это просто означает или подразумевает, что среди функциональных членов $f\colon {\mathbb {Z} }\to ({\mathbb {Z} }\to {\mathbb {Z} })$ни одно из них не обладает свойством быть сюръективным.

Конструктивные теории множеств также изучаются в контексте аппликативных аксиом .

Metalogic

В то время как теория ${\mathsf {ECST}}+{\mathrm {Exp} }$ не превышает силу непротиворечивости арифметики Хейтинга, добавление исключенного среднего дает теорию, доказывающую те же теоремы, что и классическая ${\mathsf {ZF}}$минус Регулярность! Таким образом, добавление регулярности, а также либо ${\mathrm {PEM} }$ или полное разделение ${\mathsf {ECST}}+{\mathrm {Exp} }$ дает полную классику ${\mathsf {ZF}}$. Добавление полного выбора и полного разделения дает ${\mathsf {ZFC}}$минус Регулярность. Таким образом, это привело бы к созданию теории, превосходящей по силе типичную теорию типов .

Представленная теория не доказывает функциональное пространство типа ${\mathbb {N} }^{\mathbb {N} }$быть неисчислимым, в смысле инъекций из него. Без дальнейших аксиом интуиционистская математика имеет модели в виде рекурсивных функций, а также формы гипервычислений .

Анализ

В этом разделе сила ${\mathsf {ECST}}+{\mathrm {Exp} }$разрабатывается. Для контекста упоминаются возможные дополнительные принципы, которые не обязательно являются классическими, а также обычно не считаются конструктивными. Здесь уместно общее предупреждение: читая утверждения об эквивалентности предложений в вычислимом контексте, всегда следует помнить, какие принципы выбора , индукции и понимания молчаливо предполагаются. См. также соответствующий конструктивный анализ , осуществимый анализ и вычислительный анализ .

На данный момент теория доказывает единственность архимедовских с , дедекиндовых полных ( псевдо- ) упорядоченных полей эквивалентностью по единственному изоморфизму. Приставка «псевдо» здесь подчеркивает, что порядок в любом случае конструктивно не всегда будет разрешимым. Этот результат актуален, если предположить, что полные такие модели существуют в виде наборов.

Топология

Независимо от выбора модели характерный оттенок конструктивной теории чисел можно объяснить с помощью независимого утверждения. $P$. Рассмотрим контрпример к конструктивной доказуемости упорядоченности натуральных чисел, но теперь встроенных в действительные числа. Сказать

$M:=\{x\in {\mathbb {R} }\mid (x=0\land P)\lor (x=1)\}$.

Минимальное метрическое расстояние между некоторой точкой и таким подмножеством, которое можно выразить как $\rho (0,M)$например, может конструктивно не доказуемо существовать. В более общем смысле, это свойство местоположения подмножеств определяет хорошо разработанную теорию конструктивного метрического пространства.

меньше утверждений об арифметике действительных чисел Будь то действительные числа Коши или Дедекинда, среди прочего, также разрешимо по сравнению с классической теорией.

Последовательности Коши

Возведение в степень подразумевает принципы рекурсии и т. д. ${\mathsf {ECST}}+{\mathrm {Exp} }$, можно спокойно рассуждать о последовательностях $s\colon \omega \to {\mathbb {Q} }$, их свойства регулярности, такие как $|s_{n}-s_{m}|\leq {\tfrac {1}{n}}+{\tfrac {1}{m}}$, или о сокращении интервалов в $\omega \to ({\mathbb {Q} }\times {\mathbb {Q} })$. Это позволяет говорить о последовательностях Коши и их арифметике. Такой подход к анализу принят и в ${\mathsf {Z}}_{2}$.

Коши

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

Даже в сильной теории ${\mathsf {IZF}}$ с усиленной формой Коллекции действительные числа Коши ведут себя плохо, когда не принимают форму счетного выбора , и ${\mathrm {AC} _{\omega ,2}}$достаточно для большинства результатов. Речь идет о полноте классов эквивалентности таких последовательностей, эквивалентности всего множества числам Дедекинда, существовании модуля сходимости для всех последовательностей Коши и сохранении такого модуля при переходе к пределам. Альтернативный подход, который немного лучше, состоит в том, чтобы объединить набор действительных чисел Коши с выбором модуля, т.е. не только с действительными числами, но с набором пар или даже с фиксированным модулем, общим для всех действительных чисел.

Дедекинда

Как и в классической теории, дедекиндовы разрезы характеризуются с помощью подмножеств алгебраических структур, таких как ${\mathbb {Q} }$: Свойства населенности, численной ограниченности сверху, «закрытости вниз» и «открытости вверх» — все это ограниченные формулы по отношению к данному множеству, лежащему в основе алгебраической структуры. Стандартный пример разреза, первого компонента, действительно проявляющего эти свойства, — это представление ${\sqrt {2}}$ данный

${\big \langle }\{x\in {\mathbb {Q} }\mid x<0\lor x^{2}<2\},\,\{x\in {\mathbb {Q} }\mid 0<x\land 2<x^{2}\}{\big \rangle }\,\ \in \,\ {{\mathcal {P}}_{\mathbb {Q} }}\times {{\mathcal {P}}_{\mathbb {Q} }}$

(В зависимости от соглашения о сокращении, любая из двух частей или ни одна из них, как здесь, может использовать знак $\leq$.)

Теория, данная аксиомами, до сих пор подтверждает, что псевдоупорядоченное поле, которое также является архимедовым и дедекиндовым полным, если оно вообще существует, таким образом характеризуется однозначно, с точностью до изоморфизма. Однако существование именно функциональных пространств, таких как $\{0,1\}^{\mathbb {Q} }$ не предоставляет ${{\mathcal {P}}_{\mathbb {Q} }}$ быть множеством, и поэтому класс всех подмножеств этого ${\mathbb {Q} }$которые соответствуют названным свойствам. Для того чтобы класс дедекиндовых действительных чисел был набором, требуется аксиома существования набора подмножеств, и это обсуждается далее ниже в разделе, посвященном двоичному уточнению. В контексте без ${\mathrm {PEM} }$ или Powerset, предполагается, что счетный выбор в конечных множествах доказывает несчетность множества всех дедекиндовых действительных чисел.

Конструктивные школы

Большинство школ конструктивного анализа подтверждают некоторый выбор, а также $\mathrm {BD}$- ${\mathbb {N} }$, как определено во втором разделе, посвященном границам чисел. Вот некоторые другие положения, используемые в теориях конструктивного анализа, которые невозможно доказать, используя только базовую интуиционистскую логику:

• Что касается рекурсивной математики («русская» или «марковская» конструктивная основа со многими сокращениями, например ${\mathsf {RUSS}}$), первый имеет принцип Маркова ${\mathrm {MP} }$, которое представляет собой форму доказательства от противного, мотивированную вычислимым поиском (неограниченная емкость памяти). Это оказывает заметное влияние на утверждения о реальных числах, о которых говорится ниже. В этой школе присутствует даже антиклассический конструктивный принцип Церкви. ${\mathrm {CT} }$, обычно принимаемый для теоретико-числовых функций. Тезисный принцип Чёрча, выраженный на языке теории множеств и сформулированный для функций множеств, постулирует, что все они соответствуют вычислимым программам, которые в конечном итоге останавливаются при любом аргументе. В теории вычислимости натуральные числа, соответствующие индексам кодов вычислимых функций, которые являются тотальными, равны $\Pi _{2}^{0}$ в арифметической иерархии , что означает, что принадлежность к любому индексу подтверждается проверкой $\forall x\,\exists y$предложение. Это означает, что такой набор функций по-прежнему является всего лишь подклассом натуральных чисел и поэтому, если рассматривать его по отношению к некоторым классическим функциональным пространствам, концептуально мал. В этом смысле принятие ${\mathrm {CT} }$ постулат делает $\omega \to \omega$в «разреженное» множество, с точки зрения классической теории множеств. Счетность множеств можно постулировать и независимо.
• Итак, с другой стороны, со стороны брауэрианских интуиционистов ( ${\mathsf {INT}}$), существуют барная индукция , разрешимая теорема веера ${\mathrm {FAN} }_{\Delta }$ утверждая, что разрешимые полосы однородны, что является одним из самых слабых, часто обсуждаемых принципов, схема Крипке (со счетным выбором, превращающим все подклассы $\omega$ счетный), или даже антиклассический принцип непрерывности Брауэра, определяющий возвращаемые значения того, что устанавливается функцией на бесконечных последовательностях уже через только конечные начальные сегменты.

Некоторые законы обеих этих школ противоречат друг другу. ${\mathrm {WLPO} }$, так что принятие всех принципов любой школы опровергает теоремы классического анализа. ${\mathrm {CT} }_{0}$ все еще соответствует некоторому выбору, но противоречит классической ${\mathrm {WKL} }$ и ${\mathrm {LLPO} }$, объяснено ниже. Независимость правила посылок от предпосылок существования множеств до конца не понята, но как принцип теории чисел она в некоторых концепциях противоречит аксиомам русской школы. Примечательно, ${\mathrm {CT} }_{0}$ также противоречит ${\mathrm {FAN} }_{\Delta }$То есть конструктивные школы также не могут быть полностью объединены. Некоторые принципы не могут быть конструктивно объединены до такой степени, что вместе они предполагают формы ${\mathrm {PEM} }$ - например ${\mathrm {MP} }$плюс счетность всех подмножеств натуральных чисел. Эти комбинации, естественно, также не согласуются с дальнейшими антиклассическими принципами.

Неразложимость

Обозначим класс всех множеств через ${\mathcal {V}}$. Разрешимость принадлежности к классу $R$ может быть выражено как членство в $R\cup ({\mathcal {V}}\setminus R)$. Отметим также, что по определению два экстремальных класса ${\mathcal {V}}$ и $\{\}$тривиально разрешимы. Членство в этих двух эквивалентно тривиальным утверждениям $x=x$ соотв. $\neg (x=x)$.

Позвонить в класс $R$ неразложимый или связный, если для любого предиката $\chi$,

${\big (}\forall (x\in R).\chi (x)\lor \neg \chi (x){\big )}\to {\Big (}{\big (}\forall (x\in R).\chi (x){\big )}\lor {\big (}\forall (x\in R).\neg \chi (x){\big )}{\Big )}$

Это означает, что единственные свойства, разрешимые на $R$являются тривиальными свойствами. Это хорошо изучено в интуиционистском анализе.

Так называемая схема неразложимости. ${\mathrm {UZ} }$ (Unzerlegbarkeit) для теории множеств — это возможный принцип, который утверждает, что весь класс ${\mathcal {V}}$является неразложимым. Говоря в более широком смысле, ${\mathrm {UZ} }$постулирует, что два тривиальных класса — единственные классы, разрешимые относительно класса всех множеств. В качестве простого мотивирующего предиката рассмотрим членство $x\in 1$ в первом нетривиальном классе, то есть свойство $x=\{\}$быть пустым. Это свойство нетривиально, поскольку оно разделяет некоторые множества: пустое множество является членом $1$по определению, хотя доказано, что множество множеств не являются членами $1$. Но, используя разделение, можно, конечно, также определить различные множества, для которых пустота вообще неразрешима в конструктивной теории, т. е. принадлежность к $1\cup ({\mathcal {V}}\setminus 1)$доказуемо не для всех множеств. Таким образом, здесь свойство пустоты не разделяет заданную теоретическую область дискурса на две разрешимые части. Для любого такого нетривиального свойства противоположность ${\mathrm {UZ} }$ говорит, что оно не может быть разрешимо во всех множествах.

${\mathrm {UZ} }$ подразумевается принципом единообразия ${\mathrm {UP} }$, что соответствует ${\mathsf {CZF}}$ и обсуждается ниже.

Неконструктивные принципы

Конечно ${\mathrm {PEM} }$ и многие принципы, определяющие промежуточную логику, неконструктивны. ${\mathrm {PEM} }$ и ${\mathrm {WPEM} }$, который ${\mathrm {PEM} }$для только что отрицаемых предложений можно представить как правила Де Моргана . Более конкретно, этот раздел будет посвящен утверждениям в терминах предикатов - особенно более слабым, выраженным в терминах нескольких кванторов над множествами поверх разрешимых предикатов над числами. Возвращаясь к разделу о характеристических функциях, можно назвать коллекцию $A$ доступен для поиска, если он доступен для поиска по всем его отделяемым подмножествам, что само по себе соответствует $\{0,1\}^{A}$. Это форма $\exists$- ${\mathrm {PEM} }$ для $A$. Обратите внимание, что в контексте возведения в степень такие предложения о множествах теперь привязаны к множествам.

Особую ценность при изучении конструктивного анализа представляют неконструктивные утверждения, обычно формулируемые в терминах совокупности всех бинарных последовательностей и характеристических функций. $f$ в арифметической области $A=\omega$хорошо изучены. Здесь $f({\underline {\mathrm {n} }})=0$ является разрешимым предложением для каждой цифры ${\mathrm {n} }$, но, как было показано ранее, количественные утверждения с точки зрения $f$может и не быть. Как известно из теоремы о неполноте и ее вариаций, уже в арифметике первого порядка примерные функции на ${\mathbb {N} }$ можно охарактеризовать так, что если ${\mathsf {PA}}$ является последовательным, конкурирующим $\exists$- ${\mathrm {PEM} }$ каждый из дизъюнктов низкой сложности ${\mathsf {PA}}$- недоказуемый (даже если ${\mathsf {PA}}$ аксиоматически доказывает их дизъюнкция.)

В более общем плане арифметика $\exists$- ${\mathrm {PEM} }$Наиболее известное неконструктивное, по существу логическое утверждение носит название ограниченного принципа всеведения. ${\mathrm {LPO} }$. В конструктивной теории множеств ${\mathsf {CZF}}$ представленное ниже, это подразумевает ${\mathrm {BD} }$- ${\mathbb {N} }$, ${\mathrm {MP} }$, $\Pi _{1}^{0}$-версия теоремы веера, но и ${\mathrm {WKL} }$обсуждается ниже. Вспомните примеры известных предложений, которые можно записать в $\Pi _{1}^{0}$-мода, то есть типа Гольдбаха: гипотеза Гольдбаха , последняя теорема Ферма , а также гипотеза Римана среди них . Предполагая релятивизированный зависимый выбор ${\mathrm {RDP} }$ и классический ${\mathrm {LPO} }$ над ${\mathsf {CZF}}$ не позволяет доказать более $\Pi _{0}^{2}$-заявления. ${\mathrm {LPO} }$ постулирует дизъюнктивное свойство, как и более слабое утверждение о разрешимости для постоянных функций ( $\Pi _{1}^{0}$-предложения) ${\mathrm {WLPO} }$, арифметика $\forall$- ${\mathrm {PEM} }$. Эти два связаны таким же образом, как и ${\mathrm {PEM} }$ против ${\mathrm {WPEM} }$ и они существенно отличаются ${\mathrm {MP} }$. ${\mathrm {WLPO} }$ в свою очередь подразумевает так называемую «меньшую» версию ${\mathrm {LLPO} }$. Это (арифметика) $\exists$-версия неконструктивного правила Де Моргана для отрицательного союза. Существуют, например, модели сильной теории множеств. ${\mathsf {IZF}}$ которые разделяют такие утверждения в том смысле, что они могут подтвердить достоверность ${\mathrm {LLPO} }$ но отвергнуть ${\mathrm {WLPO} }$.

Дизъюнктивные принципы о $\Pi _{1}^{0}$-предложения обычно намекают на эквивалентные формулировки, определяющие обособленность в анализе в контексте с мягким выбором или ${\mathrm {MP} }$. Претензия, высказанная ${\mathrm {LPO} }$перевод в действительные числа эквивалентен утверждению, что равенство или раздельность любых двух действительных чисел разрешимы (фактически это решает трихотомию). Тогда это также эквивалентно утверждению, что каждое реальное либо рационально, либо иррационально - без требования или построения свидетеля для любого из дизъюнктов. Аналогичным образом, утверждение, высказанное ${\mathrm {LLPO} }$ для действительных чисел эквивалентно упорядочиванию $\leq$любых двух вещественных чисел разрешима (дихотомия). Тогда это также эквивалентно утверждению, что если произведение двух действительных чисел равно нулю, то любое из вещественных чисел равно нулю - опять же без свидетеля. В самом деле, тогда каждая формулировка трех принципов всеведения эквивалентна теоремам обособленности, равенства или порядка двух вещественных чисел. Еще больше можно сказать о последовательностях Коши, дополненных модулем сходимости.

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

Бесконечные деревья

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

$T\,\subset \,\bigcup _{n\in \omega }\{0,1\}^{\{0,1,\dots ,n-1\}}$,

с разрешимой принадлежностью, и тогда доказано, что эти деревья содержат элементы произвольного большого конечного размера. Так называемая слабая лемма Кёнига. ${\mathrm {WKL} }$ утверждает: для такого $T$, всегда существует бесконечный путь в $\omega \to \{0,1\}$, т.е. бесконечная последовательность, все ее начальные сегменты являются частью дерева. В обратной математике арифметическая подсистема второго порядка ${\mathsf {RCA}}_{0}$ не доказывает ${\mathrm {WKL} }$. Чтобы понять это, заметим, что существуют вычислимые деревья $K$для которого не существует вычислимого такого пути через него. Чтобы доказать это, нужно перечислить частично вычислимые последовательности, а затем диагонализировать все полные вычислимые последовательности в одну частичную вычислимую последовательность. $d$. Затем можно выкатить определенное дерево $K$, который точно совместим с все еще возможными значениями $d$ всюду, что по построению несовместимо ни с одним полным вычислимым путем.

В ${\mathsf {CZF}}$, принцип ${\mathrm {WKL} }$ подразумевает ${\mathrm {LLPO} }$ и $\Pi _{1}^{0}$- ${\mathrm {AC} }_{\omega ,2}$, очень скромная форма счетного выбора, представленная выше. Первые два эквивалентны, если предположить, что принцип выбора уже применяется в более консервативном арифметическом контексте. ${\mathrm {WKL} }$также эквивалентна теореме Брауэра о неподвижной точке и другим теоремам, касающимся значений непрерывных функций в действительных числах. Теорема о фиксированной точке, в свою очередь, подразумевает теорему о промежуточном значении , но всегда помните, что эти утверждения могут зависеть от формулировки, поскольку классические теоремы о закодированных действительных числах могут переводиться в разные варианты, когда они выражены в конструктивном контексте.

The ${\mathrm {WKL} }$и некоторые его варианты относятся к бесконечным графам, поэтому его противоположности дают условие конечности. Опять же для подключения к анализу, по классической теории арифметики. ${\mathsf {RCA}}_{0}$, претензия ${\mathrm {WKL} }$ например, эквивалентно борелевской компактности относительно конечных подпокрытий действительного единичного интервала. ${\mathrm {FAN} }_{\Delta }$- это тесно связанное утверждение о существовании, включающее конечные последовательности в бесконечном контексте. Над ${\mathsf {RCA}}_{0}$, они фактически эквивалентны. В ${\mathsf {CZF}}$ они различны, но, снова предположив некоторый выбор, вот тогда ${\mathrm {WKL} }$ подразумевает ${\mathrm {FAN} }_{\Delta }$.

Индукция

Математическая индукция

Было замечено, что на общепринятом языке принципы индукции можно прочитать $\mathrm {Ind} _{A}\to \omega \subset A$, с предшествующим $\mathrm {Ind} _{A}$ определяется, как указано выше, и с $\omega \subset A$ значение $\forall (n\in \omega ).n\in A$ где набор $\omega$всегда обозначает стандартную модель натуральных чисел. Благодаря сильной аксиоме Бесконечности и предикативному Разделению справедливость индукции для ограниченных множеством или $\Delta _{0}$-определения уже установлены и тщательно обсуждены. Для тех предикатов, включающих только кванторы над $\omega$, это подтверждает индукцию в смысле теории арифметики первого порядка. В контексте теории множеств, где $\omega$ является множеством, этот принцип индукции можно использовать для доказательства предикативно определенных подклассов $\omega$ быть набором $\omega$сам. Так называемая схема полной математической индукции теперь постулирует равенство множеств $\omega$всем его индуктивным подклассам. Как и в классической теории, это подразумевается и при переходе к непредикативной схеме полного разделения. Как указано в разделе «Выбор», подобные принципы индукции также подразумеваются различными формами принципов выбора.

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

Схема аксиом полной математической индукции : для любого предиката $\phi$ на $\omega$, ${\Big (}\phi (0)\ \land \ \forall (k\in \omega ).{\big (}\phi (k)\to \phi (Sk){\big )}{\Big )}\to \forall (n\in \omega ).\phi (n)$

Формулы предикатов, используемые в схеме, следует понимать как формулы теории множеств первого порядка. Ноль $0$ обозначает множество $\{\}$ как указано выше, и набор $Sn$ обозначает последующий набор $n\in \omega$, с $n\in Sn$. Согласно Аксиоме Бесконечности, приведенной выше, он снова является членом $\omega$. Помните, что в отличие от арифметической теории, натуральные числа здесь являются не абстрактными элементами в области дискурса, а элементами модели. Как было отмечено в предыдущих обсуждениях, при принятии ${\mathsf {ECST}}$, даже для всех предикативно определенных множеств равенство такому конечному ординалу фон Неймана не обязательно разрешимо.

Установить индукцию

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

Схема аксиом индукции множества : для любого предиката $\phi$, ${\Big (}\forall x.\,{\big (}\forall (y\in x).\ \phi (y){\big )}\to \phi (x){\Big )}\to \forall z.\phi (z)$

Здесь $\forall (z\in \{\}).\phi (z)$ выполняется тривиально, и поэтому это относится к «нижнему случаю» $\phi (\{\})$в стандартных рамках. Это (как и индукция натуральных чисел) снова может быть ограничено только формулами ограниченного множества, и в этом случае арифметика не затрагивается.

В ${\mathsf {ECST}}$, аксиома доказывает индукцию в транзитивных множествах и, в частности, также для транзитивных множеств транзитивных множеств. Последнее тогда является адекватным определением ординалов и даже $\Delta _{0}$-формулировка. Индукция множеств, в свою очередь, обеспечивает порядковую арифметику в этом смысле. Кроме того, он позволяет определять функции класса с помощью трансфинитной рекурсии . Изучение различных принципов, которые дают определения множеств посредством индукции, то есть индуктивных определений, является основной темой в контексте конструктивной теории множеств и ее сравнительно слабых сторон . Это справедливо и для их аналогов в теории типов. Замена не требуется для доказательства индукции по множеству натуральных чисел из индукции множеств, но эта аксиома необходима для их арифметики, моделируемой в рамках теории множеств.

Аксиома регулярности — это единственное утверждение с квантором универсальности над множествами, а не схема. Как показано, это подразумевает ${\mathrm {PEM} }$, и поэтому неконструктивно. Теперь о $\phi$ считается отрицанием некоторого предиката $\neg S$ и писать $\Sigma$ для класса $\{y\mid S(y)\}$, индукция читает

$\forall (x\in \Sigma ).\neg (x\cap \Sigma =\{\})\,\,\leftrightarrow \,\,\Sigma =\{\}$

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

Metalogic

Сформулированную выше теорию можно выразить как ${\mathsf {CZF}}$с его набором аксиом, отброшенных в пользу более слабых аксиом замены и возведения в степень. Это доказывает, что действительные числа Коши являются множеством, а не классом вещественных чисел Дедекинда.

Сам ординал назовем трихотомическим, если иррефлексивное отношение принадлежности $\in$«среди своих членов является трихотомическим . Как и аксиома регулярности, индукция множеств ограничивает возможные модели» $\in$Но конструктивная теория здесь не доказывает трихотомию для всех ординалов, в то время как трихотомические ординалы не очень хорошо ведут себя по отношению к понятию преемника и классифицировать.

Дополнительная сила теории доказательств, достигаемая с помощью индукции в конструктивном контексте, значительна, даже если отказаться от регулярности в контексте ${\mathsf {ZF}}$не снижает теоретическую силу доказательства. Даже без возведения в степень настоящая теория с индукцией множеств имеет ту же теоретическую силу доказательства, что и ${\mathsf {CZF}}$и доказывает рекурсивность тех же функций. с точки зрения теории доказательств В частности, его большой счетный ординал - это ординал Бахмана – Ховарда . Это также ординал классической или интуиционистской теории множеств Крипке – Платека . Это согласуется даже с ${\mathsf {IZF}}$предположить, что класс трихотомических ординалов образует множество. Современная теория, дополненная этим постулатом существования порядкового множества, доказывает непротиворечивость ${\mathsf {CZF}}$.

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

Отношение к ZF

Теория также представляет собой изложение теории множеств Цермело – Френкеля. ${\mathsf {ZF}}$в том смысле, что присутствуют варианты всех его восьми аксиом. Экстенсиональность, Спаривание, Союз и Замена действительно идентичны. Разделение принимается в слабой предикативной форме, тогда как Бесконечность утверждается в сильной формулировке. Как и в классической формулировке, эта аксиома разделения и существование любого множества уже доказывают аксиому пустого множества. Возведение в степень для конечных областей и полная математическая индукция также подразумеваются их более сильными принятыми вариантами. Без принципа исключенного третьего теория в своей классической форме лишена полного разделения, набора сил, а также регулярности. Принятие ${\mathrm {PEM} }$ теперь точно ведет к классической теории.

Ниже представлены различные прочтения формальной теории. Позволять $\mathrm {CH}$ обозначают гипотезу континуума и $B:=\{z\in 1\mid \mathrm {CH} \}$ так что $0\in B\leftrightarrow \mathrm {CH}$. Затем $b:=B\cup \{1\}$ населён $1$ и любое множество, которое установлено как член $b$ либо равно $0$ или $1$. Индукция включена $\omega$ подразумевает, что нельзя последовательно отрицать, что $b$имеет некоторый член с наименьшим натуральным числом. Можно показать, что значение такого члена не зависит от таких теорий, как ${\mathsf {ZFC}}$. Тем не менее, любая классическая теория множеств, такая как ${\mathsf {ZFC}}$ также доказывает, что существует такое число .

Сильная коллекция

Обсудив все ослабленные формы аксиом классической теории множеств, замену и возведение в степень можно дополнительно усилить, не теряя теоретической интерпретации типов, и таким образом, чтобы не выходить за рамки ${\mathsf {ZF}}$.

Итак, во-первых, можно поразмышлять о силе аксиомы замены , в том числе и в контексте классической теории множеств. Для любого набора $y$ и любые натуральные $n$, существует произведение $y^{n}$ рекурсивно заданный $y^{n-1}\times y$, которые имеют все более глубокий ранг . Индукция несвязанных предикатов доказывает, что эти множества существуют для всех бесконечно многих натуральных чисел. Замена для $n\mapsto y^{n}$«Более того, теперь утверждается, что этот бесконечный класс продуктов можно превратить в бесконечное множество, $\{p\mid \exists (n\in \omega ).p=y^{n}\}$. Это также не является подмножеством какого-либо ранее установленного набора.

Выйдя за рамки аксиом, также встречающихся в типизированном подходе Майхилла, рассмотрим обсуждаемую конструктивную теорию с возведением в степень и индукцией, но теперь усиленную схемой набора . В ${\mathsf {ZF}}$это эквивалентно замене, если не отбрасывается аксиома набора мощности. В текущем контексте представленная сильная аксиома заменяет замену, поскольку не требуется, чтобы определение бинарного отношения было функциональным, но, возможно, многозначным.

Схема аксиом сильной коллекции: для любого предиката. $\phi$, $\forall a.\ \ {\Big (}\forall (x\in a).\exists y.\phi (x,y){\Big )}\to \exists b.{\Big (}\forall (x\in a).\exists (y\in b).\phi (x,y)\ \land \ \forall (y\in b).\exists (x\in a).\phi (x,y){\Big )}$

Другими словами, для каждого тотального отношения существует набор образов. $b$так что отношение является полным в обоих направлениях. Выражение этого через необработанную формулировку первого порядка приводит к несколько повторяющемуся формату. Антецедент утверждает, что рассматривается отношение $\phi$ между сетами $x$ и $y$ которые являются общими для определенного набора доменов $a$, то есть, $\phi$ имеет хотя бы одно «значение изображения» $y$ для каждого элемента $x$в домене. Это более общее явление, чем условие обитания. $x\in y$ в наборе аксиом теоретического выбора, но также более общем, чем условие Замены, которое требует уникального существования $\exists !y$. В консеквенте, во-первых, аксиомы утверждают, что тогда существует множество $b$ который содержит хотя бы одно значение «изображения» $y$ под $\phi$, для каждого элемента домена. Во-вторых, в этой формулировке аксиомы, кроме того, утверждается, что только такие образы $y$ являются элементами этого нового набора кодоменов $b$. Это гарантия того, что $b$ не выходит за пределы кодомена $\phi$и, таким образом, аксиома также выражает некоторую силу, подобную процедуре разделения. Этот принцип можно использовать при конструктивном исследовании больших множеств, выходящих за рамки повседневной необходимости анализа.

Metalogic

Эта теория без ${\mathrm {PEM} }$, без неограниченного разделения и без «наивного» силового множества, обладает различными приятными свойствами. Например, в отличие от ${\mathsf {CZF}}$ со схемой коллекции подмножеств, приведенной ниже, он имеет свойство существования .

-

Бинарное уточнение

Так называемая аксиома бинарного уточнения гласит, что для любого $a$ существует набор ${\mathcal {B}}_{a}\subset {\mathcal {P}}_{a}$ такая, что для любого покрытия $a=x\cup y$, набор ${\mathcal {B}}_{a}$ содержит два подмножества $c\subset x$ и $d\subset y$ которые также выполняют эту работу по прикрытию, $a=c\cup d$. Это самая слабая форма аксиомы набора степеней, лежащая в основе некоторых важных математических доказательств. Полнота ниже для отношений между множеством $a$ и конечное $\{0,1\}$, подразумевает, что это действительно возможно.

Сделав еще шаг назад, ${\mathsf {ECST}}$Плюс рекурсия и плюс двоичное уточнение уже доказывают, что существует архимедово, дедекиндово полное псевдоупорядоченное поле. Эта теория множеств также доказывает, что класс левых дедекиндовых разрезов является множеством, не требующим индукции или сбора. Более того, это доказывает, что функциональные пространства, разбитые на дискретные множества, являются множествами (там, например, $\omega \to \omega$), не предполагая ${\mathrm {Exp} }$. Уже над слабой теорией ${\mathsf {BCST}}$ (то есть без бесконечности) доказывает ли бинарное уточнение, что функциональные пространства, разбитые на дискретные множества, являются множествами и, следовательно, например, существование всех характеристических функциональных пространств $\{0,1\}^{a}$.

Коллекция подмножеств

Теория, известная как ${\mathsf {CZF}}$принимает аксиомы предыдущих разделов плюс более сильную форму возведения в степень. Это происходит путем принятия следующей альтернативы возведению в степень, которую снова можно рассматривать как конструктивную версию аксиомы набора степеней :

Схема аксиом коллекции подмножеств: для любого предиката. $\phi$, $\forall a.\forall b.\ \ \exists u.\forall z.{\big (}\forall (x\in a).\exists (y\in b).\phi (x,y,z){\big )}\to \exists (v\in u).{\big (}\forall (x\in a).\exists (y\in v).\phi (x,y,z)\;\land \;\forall (y\in v).\exists (x\in a).\phi (x,y,z){\big )}$

Альтернатива, не являющаяся схемой, подробно описана ниже.

Полнота

Для данного $a$ и $b$, позволять ${\mathcal {R}}_{ab}$ быть классом всех полных отношений между $a$ и $b$. Этот класс задается как

$r\in {\mathcal {R}}_{ab}\leftrightarrow {\Big (}{\big (}\forall (x\in a).\exists (y\in b).\langle x,y\rangle \in r{\big )}\,\land \,{\big (}\forall (p\in r).\exists (x\in a).\exists (y\in b).p=\langle x,y\rangle {\big )}{\Big )}$

В отличие от определения функции, в ней нет уникального квантора существования. $\exists !(y\in b)$. Класс ${\mathcal {R}}_{ab}$ представляет собой пространство «неоднозначных функций» или « многозначных функций » из $a$ к $b$, а как набор отдельных пар с правой проекцией в $b$. Во втором пункте говорится, что речь идет только об этих отношениях, а не о тех, которые тотальны по отношению к другим. $a$ но и расширить свою сферу деятельности за пределы $a$.

Никто не постулирует ${\mathcal {R}}_{ab}$ быть множеством, поскольку при Замене можно использовать эту совокупность отношений между множеством $a$ и конечное $b=\{0,1\}$, то есть «двузначные функции на $a$", чтобы извлечь набор ${\mathcal {P}}_{a}$всех его подмножеств. Другими словами ${\mathcal {R}}_{ab}$ быть набором означало бы аксиому Powerset.

Над ${\mathsf {ECTS}}+{\text{Strong Collection}}$, существует единственная, несколько более ясная альтернативная аксиома схеме коллекции подмножеств . Он постулирует существование достаточно большого множества ${\mathcal {S}}_{ab}$ совокупных отношений между $a$ и $b$.

Аксиома полноты: $\forall a.\forall b.\ \exists {\mathcal {S}}_{ab}.\,({\mathcal {S}}_{ab}\subset {\mathcal {R}}_{ab})\,\land \,\forall (r\in {\mathcal {R}}_{ab}).\exists (s\in {\mathcal {S}}_{ab}).s\subset r$

Это говорит о том, что для любых двух множеств $a$ и $b$, существует набор ${\mathcal {S}}_{ab}\subset {\mathcal {R}}_{ab}$ которое среди своих членов находится в еще тотальном отношении $s\in {\mathcal {S}}_{ab}$ для любого данного полного отношения $r\in {\mathcal {R}}_{ab}$.

На заданном домене $a$, функции представляют собой в точности самые разреженные полные отношения, а именно однозначнозначные. Следовательно, из аксиомы следует, что существует множество, в котором находятся все функции. Таким образом, Полнота подразумевает Возведение в степень. Это далее подразумевает бинарное уточнение, уже более ${\mathsf {BCST}}$.

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

Металогика CZF

${\mathsf {CZF}}$ обладает свойством числового существования и свойством дизъюнктивности , но есть уступки: ${\mathsf {CZF}}$отсутствует свойство существования из-за схемы коллекции подмножеств или аксиомы полноты. Схема также может быть препятствием для моделей реализуемости. Свойство существования не является недостатком, когда вместо него принимается более слабое возведение в степень или более сильная, но непредикативная аксиома Powerset. Последнее вообще лишено конструктивной интерпретации.

Недоказуемые утверждения

Теория согласуется с некоторыми антиклассическими утверждениями, но сама по себе не доказывает ничего, что не было бы доказуемо. ${\mathsf {ZF}}$. Некоторые известные утверждения, не подтвержденные ни теорией (ни ${\mathsf {IZF}}$, если уж на то пошло) являются частью принципов, перечисленных выше, в разделах о конструктивных школах анализа, о конструкции Коши и о неконструктивных принципах. Нижеследующее касается установленных теоретических концепций:

Ограниченное понятие транзитивного множества транзитивных множеств — хороший способ определения ординалов и возможность индукции по ординалам. Но примечательно, что это определение включает в себя некоторые $\Delta _{0}$-подмножества в ${\mathsf {CZF}}$. Итак, если предположить, что членство $0$ разрешимо во всех последующих ординалах $S\alpha$ доказывает ${\mathrm {PEM} }$ для ограниченных формул в ${\mathsf {CZF}}$. Кроме того, в этой теории невозможно вывести ни линейность ординалов . , ни существование степенных множеств конечных множеств, поскольку предположение любого из них подразумевает степенное множество То обстоятельство, что ординалы ведут себя лучше в классическом, чем в конструктивном контексте, проявляется в различных постулатах теории существования больших множеств.

Рассмотрим функции, областью определения которых является $\omega$ или несколько $n\in \omega$. Это последовательности, а их диапазоны представляют собой наборы. Обозначим через $C$ класс, характеризуемый как наименьший кодомен, такой, что диапазоны вышеупомянутых функций в $C$ также сами являются членами $C$. В ${\mathsf {ZF}}$, это набор $H_{\aleph _{1}}$ наследственно счетных множеств и имеет порядковый ранг не более $\omega _{2}$. В ${\mathsf {ZF}}$, он несчетен (так как содержит также все счетные ординалы, мощность которых обозначается $\aleph _{1}$), но его мощность не обязательно равна мощности ${\mathbb {R} }$. Тем временем, ${\mathsf {CZF}}$ не доказывает $C$ даже представляет собой множество, даже если счетный выбор предполагается .

Наконец, теория не доказывает, что все функциональные пространства образованы из множеств в конструируемой вселенной. $L$ установлены внутри $L$, и это справедливо даже при использовании Powerset вместо более слабой аксиомы возведения в степень. Итак, это конкретное утверждение, предотвращающее ${\mathsf {CZF}}$ от доказательства класса $L$ быть образцом ${\mathsf {CZF}}$.

Порядковый анализ

принимая ${\mathsf {CZF}}$ и отказ от индукции множеств дает теорию, консервативную по ${\mathsf {HA}}$ для арифметических утверждений в том смысле, что он доказывает одни и те же арифметические утверждения для своих ${\mathsf {HA}}$-модель $\omega$. Добавление только математической индукции дает теорию с теоретико-доказательным порядковым номером. $\varphi (\varepsilon _{0},0)$, которая является первой общей неподвижной точкой функций Веблена $\varphi _{\beta }$ для $\beta <\varepsilon _{0}$. Это тот же порядковый номер, что и для ${\mathsf {ML_{1}}}$ и находится ниже ординала Фефермана – Шютте. $\Gamma _{0}$. Демонстрируя типовую теоретическую модель, полную теорию ${\mathsf {CZF}}$ выходит за рамки $\Gamma _{0}$, его порядковый номер по-прежнему остается скромным порядковым номером Бахмана – Говарда. Если предположить, что класс трихотомических ординалов представляет собой множество, это повышает теоретическую силу доказательства ${\mathsf {CZF}}$ (но не из ${\mathsf {IZF}}$).

Будучи связанной с индуктивными определениями или барной индукцией , аксиома регулярного расширения ${\mathrm {REA} }$ повышает теоретическую силу доказательства ${\mathsf {CZF}}$. Эта аксиома большого множества, допускающая существование определенных хороших надмножеств для каждого множества, доказывается ${\mathsf {ZFC}}$.

Модели

Категория множеств и функций ${\mathsf {CZF}}+{\mathrm {REA} }$ это $\Pi W$-претопос. Не углубляясь в теорию топоса , некоторые расширили такие $\Pi W$-претопы содержат модели ${\mathsf {CZF}}+{\mathrm {REA} }$. Эффективный топос содержит модель этого ${\mathsf {CZF}}+{\mathrm {REA} }$ на основе карт, характеризующихся некоторыми хорошими свойствами счетности.

Разделение, излишне сформулированное в классическом контексте, конструктивно не подразумевается Заменой. До сих пор дискуссия сводилась только к предикативно обоснованному ограниченному разделению. Обратите внимание, что полное разделение (вместе с ${\mathrm {RDC} }$, ${\mathrm {MP} }$ а также ${\mathrm {IP} }$ для множеств) подтверждается в некоторых эффективных топосных моделях, а это означает, что аксиома не портит краеугольные камни школы ограничительной рекурсии.

С этим связаны теоретические интерпретации типов. В 1977 году Аксель показал, что ${\mathsf {CZF}}$ все еще можно интерпретировать в теории типов Мартина-Лёфа , используя подход «предложения как типы» . Более конкретно, здесь используется одна вселенная и $W$-типы, обеспечивающие то, что сейчас рассматривается как стандартная модель ${\mathsf {CZF}}$ в ${\mathsf {ML_{1}V}}$. Это делается через образы ее функций и имеет достаточно прямое конструктивное и предикативное обоснование, сохраняя при этом язык теории множеств. Грубо говоря, есть два «больших» типа. $U,V$, все наборы даются через любые $f\colon A\to V$ на некоторых $A\colon U$и членство в $x$ в наборе определено, что оно выполняется, когда $\exists (a\colon A).f(a)=x$. Наоборот, ${\mathsf {CZF}}$ интерпретирует ${\mathsf {ML_{1}V}}$. Все утверждения, подтвержденные в счетной модели теории множеств, могут быть точно доказаны с помощью ${\mathsf {CZF}}$ плюс принцип выбора $\Pi \Sigma$- $\mathrm {AC}$, указано далее выше. Как уже отмечалось, такие теории, как ${\mathsf {CZF}}$, а также вместе с выбором обладают свойством существования для широкого класса множеств в общей математике. Теории типа Мартина-Лёфа с дополнительными принципами индукции подтверждают соответствующие аксиомы теории множеств.

корректности и полноте Теоремы о ${\mathsf {CZF}}$, относительно реализуемости , установлены.

Разрыв с ZF

Можно, конечно, добавить тезис Чёрча.

Можно постулировать счетность всех множеств. Это уже справедливо для теоретико-типовой интерпретации и модели эффективного топоса. По бесконечности и возведению в степень, $\omega \to \omega$ является несчетным множеством, а класс ${\mathcal {P}}_{\omega }$ или даже ${\mathcal {P}}_{1}$тогда доказано, что это не множество, согласно диагональному аргументу Кантора . Таким образом, эта теория затем логически отвергает Powerset и, конечно же, ${\mathrm {PEM} }$. Субсчетность также противоречит различным аксиомам больших множеств . (С другой стороны, также используя ${\mathsf {CZF}}$, некоторые такие аксиомы предполагают непротиворечивость таких теорий, как ${\mathsf {ZF}}$ и сильнее.)

По правилу вывода ${\mathsf {CZF}}$ замкнуто согласно общему единообразию Трульстры для обоих $z=\omega$ и $z=\{0,1\}$. Ее можно принять как антиклассическую схему аксиом, принцип единообразия, который можно обозначить как ${\mathrm {UP} }$,

$\forall z.{\big (}\forall x.\exists (y\in z).\phi (x,y){\big )}\to \exists (y\in z).\forall x.\phi (x,y)$

Это также несовместимо с аксиомой powerset. Этот принцип также часто формулируется для $z=\omega$. Теперь о двоичном наборе меток $z=\{0,1\}$, ${\mathrm {UP} }$ подразумевает схему неразложимости ${\mathrm {UZ} }$, как указано.

В 1989 году Ингрид Линдстрём показала, что необоснованные множества также можно интерпретировать в теории типов Мартина-Лёфа, которые получаются заменой индукции множеств в ${\mathsf {CZF}}$ с антифундаментальной аксиомой Акселя . Полученная теория ${\mathsf {CZFA}}$ можно изучить, также добавив обратно $\omega$-индукционная схема или релятивизированный зависимый выбор , а также утверждение, что каждое множество является членом транзитивного множества .

Intuitionistic Zermelo–Fraenkel

The theory ${\mathsf {IZF}}$ is ${\mathsf {CZF}}$ adopting both the standard Separation as well as Power set and, as in ${\mathsf {ZF}}$, one conventionally formulates the theory with Collection below. As such, ${\mathsf {IZF}}$ can be seen as the most straight forward variant of ${\mathsf {ZF}}$ without PEM. So as noted, in ${\mathsf {IZF}}$, in place of Replacement, one may use the

Axiom schema of collection: For any predicate $\phi$, $\forall z.{\big (}\forall (x\in z).\exists y.\phi (x,y){\big )}\to \exists w.\forall (x\in z).\exists (y\in w).\phi (x,y)$

While the axiom of replacement requires the relation ϕ to be functional over the set z (as in, for every x in z there is associated exactly one y), the Axiom of Collection does not. It merely requires there be associated at least one y, and it asserts the existence of a set which collects at least one such y for each such x. In classical ${\mathsf {ZFC}}$, the Collection schema implies the Axiom schema of replacement. When making use of Powerset (and only then), they can be shown to be classically equivalent.

While ${\mathsf {IZF}}$ is based on intuitionistic rather than classical logic, it is considered impredicative. It allows formation of sets via a power set operation and using the general Axiom of Separation with any proposition, including ones which contain quantifiers which are not bounded. Thus new sets can be formed in terms of the universe of all sets, distancing the theory from the bottom-up constructive perspective. So it is even easier to define sets $\{x\in B\mid Q(x)\}$ with undecidable membership, namely by making use of undecidable predicates defined on a set. The power set axiom further implies the existence of a set of truth values. In the presence of excluded middle, this set has two elements. In the absence of it, the set of truth values is also considered impredicative. The axioms of ${\mathsf {IZF}}$ are strong enough so that full PEM is already implied by PEM for bounded formulas. See also the previous discussion in the section on the Exponentiation axiom. And by the discussion about Separation, it is thus already implied by the particular formula $\forall x.{\big (}0\in x\lor 0\notin x{\big )}$, the principle that knowledge of membership of $0$ shall always be decidable, no matter the set.

Metalogic

As implied above, the subcountability property cannot be adopted for all sets, given the theory proves ${\mathcal {P}}_{\omega }$ to be a set. The theory has many of the nice numerical existence properties and is e.g. consistent with Church's thesis principle as well as with $\omega \to \omega$ being subcountable. It also has the disjunctive property.

${\mathsf {IZF}}$ with Replacement instead of Collection has the general existence property, even when adopting relativized dependent choice on top of it all. But just ${\mathsf {IZF}}$ as formulated does not. The combination of schemas including full separation spoils it.

Even without PEM, the proof theoretic strength of ${\mathsf {IZF}}$ equals that of ${\mathsf {ZF}}$. And ${\mathsf {HA}}$ proves them equiconsistent and they prove the same $\Pi _{1}^{0}$-sentences.

Intuitionistic Z

Again on the weaker end, as with its historical counterpart Zermelo set theory, one may denote by ${\mathsf {IZ}}$ the intuitionistic theory set up like ${\mathsf {IZF}}$ but without Replacement, Collection or Induction.

Intuitionistic KP

Let us mention another very weak theory that has been investigated, namely Intuitionistic (or constructive) Kripke–Platek set theory ${\mathsf {IKP}}$. It has not only Separation but also Collection restricted to $\Delta _{0}$-formulas, i.e. it is similar to ${\mathsf {BCST}}$ but with Induction instead of full Replacement. The theory does not fit into the hierarchy as presented above, simply because it has Axiom schema of Set Induction from the start. This enables theorems involving the class of ordinals. The theory has the disjunction property. Of course, weaker versions of ${\mathsf {IKP}}$ are obtained by restricting the induction schema to narrower classes of formulas, say $\Sigma _{1}$. The theory is especially weak when studied without Infinity.

Sorted theories

Constructive set theory

As he presented it, Myhill's system ${\mathsf {CST}}$ is a theory using constructive first-order logic with identity and two more sorts beyond sets, namely natural numbers and functions. Its axioms are:

• The usual Axiom of Extensionality for sets, as well as one for functions, and the usual Axiom of union.
• The Axiom of restricted, or predicative, separation, which is a weakened form of the Separation axiom from classical set theory, requiring that any quantifications be bounded to another set, as discussed.
• A form of the Axiom of Infinity asserting that the collection of natural numbers (for which he introduces a constant $\omega$) is in fact a set.
• The axiom of Exponentiation, asserting that for any two sets, there is a third set which contains all (and only) the functions whose domain is the first set, and whose range is the second set. This is a greatly weakened form of the Axiom of power set in classical set theory, to which Myhill, among others, objected on the grounds of its impredicativity.

And furthermore:

• The usual Peano axioms for natural numbers.
• Axioms asserting that the domain and range of a function are both sets. Additionally, an Axiom of non-choice asserts the existence of a choice function in cases where the choice is already made. Together these act like the usual Replacement axiom in classical set theory.

One can roughly identify the strength of this theory with a constructive subtheories of ${\mathsf {ZF}}$ when comparing with the previous sections.

And finally the theory adopts

• An Axiom of dependent choice, which is much weaker than the usual Axiom of choice.

Bishop style set theory

Set theory in the flavor of Errett Bishop's constructivist school mirrors that of Myhill, but is set up in a way that sets come equipped with relations that govern their discreteness. Commonly, Dependent Choice is adopted.

A lot of analysis and module theory has been developed in this context.

Category theories

Not all formal logic theories of sets need to axiomize the binary membership predicate "$\in$" directly. A theory like the Elementary Theory of the Categories Of Set (${\mathsf {ETCS}}$), e.g. capturing pairs of composable mappings between objects, can also be expressed with a constructive background logic. Category theory can be set up as a theory of arrows and objects, although first-order axiomatizations only in terms of arrows are possible.

Beyond that, topoi also have internal languages that can be intuitionistic themselves and capture a notion of sets.

Good models of constructive set theories in category theory are the pretoposes mentioned in the Exponentiation section. For some good set theory, this may require enough projectives, an axiom about surjective "presentations" of set, implying Countable and Dependent Choice.

See also

• Axiom schema of predicative separation
• Constructive mathematics
• Constructive analysis
• Constructive Church's thesis rule and principle
• Computable set
• Diaconescu's theorem
• Disjunction and existence properties
• Epsilon-induction
• Hereditarily finite set
• Heyting arithmetic
• Impredicativity
• Intuitionistic type theory
• Law of excluded middle
• Ordinal analysis
• Set theory
• Subcountability

Further reading

• Troelstra, Anne; van Dalen, Dirk (1988). Constructivism in Mathematics, Vol. 2. Studies in Logic and the Foundations of Mathematics. p. 619. ISBN 978-0-444-70358-3.
• Aczel, P. and Rathjen, M. (2001). Notes on constructive set theory. Technical Report 40, 2000/2001. Mittag-Leffler Institute, Sweden.

External links

• Crosilla, Laura (13 February 2019). "Set Theory: Constructive and Intuitionistic ZF". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
• Van den Berg, Benno (7 September 2012). "Constructive set theory – an overview" (PDF). Slides from Heyting dag, Amsterdam