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

Axiomatic set theories based on the principles of mathematical constructivism

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

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

Введение

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

Предварительные сведения об использовании интуиционистской логики

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

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

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

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

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

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

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

Металоджик

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Модели

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

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

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

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

Обозначение

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

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

Язык

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

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

Переменные

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

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

Классы

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

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

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

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

Подкласс называется отделяемым от, если релятивизированный предикат принадлежности разрешим, т.е. если выполняется. Он также называется разрешимым, если суперкласс ясен из контекста - часто это множество натуральных чисел. ${\displaystyle A\subset B}$ ${\displaystyle B}$ ${\displaystyle \forall (x\in B).x\in A\lor x\notin A}$

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

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

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

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

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

Подтеории ZF

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

Равенство

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

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

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

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

Альтернативные подходы

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

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

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

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

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

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

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

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

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

говоря, что для любого множества существует по крайней мере одно множество , которое содержит все элементы , из элементов . Минимальным таким множеством является объединение . ${\displaystyle x}$ ${\displaystyle u}$ ${\displaystyle z}$ ${\displaystyle x}$ ${\displaystyle y}$

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

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

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

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

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

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

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

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

БКСТ

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

Разделение

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

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

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

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

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

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

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

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

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

Следующее справедливо для любого отношения . Оно дает чисто логическое условие, при котором два термина и не могут быть связаны друг с другом. ${\displaystyle E}$ ${\displaystyle s}$ ${\displaystyle y}$ ${\displaystyle E}$

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

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

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

Для любого и частный случай в приведенной выше формуле дает ${\displaystyle E}$ ${\displaystyle y}$ ${\displaystyle s=y}$

${\displaystyle \neg {\big (}\forall x.xEy\leftrightarrow \neg xEx{\big )}}$

Это уже подразумевает, что подкласс универсального класса также является правильным. Но даже без Регулярности последовательно, чтобы был правильный класс синглтонов, каждый из которых содержит в точности себя. ${\displaystyle \{x\mid x\notin x\}}$ ${\displaystyle {\mathsf {ZF}}}$

В качестве отступления, в теории со стратификацией , такой как Intuitionistic New Foundations , синтаксическое выражение может быть запрещено в Separation. В свою очередь, приведенное выше доказательство отрицания существования универсального множества не может быть выполнено в этой теории. ${\displaystyle x\in x}$

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

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

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

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

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

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

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

Замена

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

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

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

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

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

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

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

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

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

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

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

ЕКСТ

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

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

${\displaystyle {\big (}\exists z.z\in A{\big )}\land \forall (x\in A).\exists (s\in A).x\in s}$.

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

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

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

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

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

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

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

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

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

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

Более слабые формулировки бесконечности

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

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

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

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

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

Принимая Аксиому Бесконечности, ограниченная множеством квантификация, допустимая в предикатах, используемых в -Разделение, затем явно допускает численно неограниченные квантификаторы - два значения "ограниченный" не следует путать. Имея под рукой, назовите класс чисел ограниченным, если выполняется следующее утверждение о существовании ${\displaystyle \Delta _{0}}$ ${\displaystyle \omega }$ ${\displaystyle I\subset \omega }$

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

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

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

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

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

Умеренная индукция в ECST

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

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

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

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

Функции

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

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

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

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

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

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

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

Всего функциональных отношений

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

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

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

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

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

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

Конечность

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

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

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

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

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

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

Характерные функции

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

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

Так как , один имеет ${\displaystyle \neg (0=1)}$

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

и так

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

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

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

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

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

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

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

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

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

Свидетель разлуки

Тождество неразличимых , которое в контексте первого порядка является принципом более высокого порядка, утверждает, что равенство двух терминов и требует, чтобы все предикаты были согласны с ними. И поэтому, если существует предикат , который различает два термина и в том смысле, что , то принцип подразумевает, что два термина не совпадают. Форма этого может быть выражена теоретически множеством: может считаться раздельным, если существует подмножество, такое, что одно является членом, а другое — нет. Ограниченное отделяемыми подмножествами, это также может быть сформулировано кратко с использованием характеристических функций . Действительно, последнее фактически не зависит от того, является ли область значений двоичным множеством: Равенство отвергается, т.е. доказывается, как только устанавливается, что не все функции на validate , логически отрицательное условие. ${\displaystyle x=y}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle P(x)\land \neg P(y)}$ ${\displaystyle x,y\in A}$ ${\displaystyle B\subset A}$ ${\displaystyle \chi _{B}\in \{0,1\}^{A}}$ ${\displaystyle x\neq y}$ ${\displaystyle f}$ ${\displaystyle A}$ ${\displaystyle f(x)=f(y)}$

На любом множестве можно определить логически положительное отношение обособленности ${\displaystyle A}$

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

Поскольку натуральные числа дискретны, для этих функций отрицательное условие эквивалентно (слабому) двойному отрицанию этого отношения. Опять же, на словах, равенство и подразумевает, что никакая окраска не может их различить - и поэтому, чтобы исключить первое, т.е. доказать , нужно просто исключить второе, т.е. просто доказать . ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle f\in {\mathbb {N} }^{A}}$ ${\displaystyle x\neq y}$ ${\displaystyle \neg \neg (x\,\#_{A}\,y)}$

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

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

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

При наличии любого натурального , тогда ${\displaystyle n\in \omega }$

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

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

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

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

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

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

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

то есть

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

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

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

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

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

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

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

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

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

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

Теорема Дьяконеску

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

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

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

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

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

Анализ теоремы Диаконеску

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

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

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

Регулярность подразумевает PEM

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

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

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

Арифметика

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Союзы и исчисляемость

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Теоретико-категориальные и типологические понятия

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

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

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

Металоджик

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

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

Анализ

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

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

Топология

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

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

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

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

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

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

Коши реалы

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

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

К Дедекиндовым реалам

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

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

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

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

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

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

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

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

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

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

Назовите класс неразложимым или связным, если для любого предиката ${\displaystyle R}$ ${\displaystyle \chi }$

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

Это выражает, что единственные свойства, которые разрешимы, — это тривиальные свойства. Это хорошо изучено в интуиционистском анализе. ${\displaystyle R}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Индукция

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

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

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

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

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

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

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

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

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

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

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

Металоджик

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

Назовем сам ординал трихотомическим, если нерефлексивное отношение принадлежности " " среди его членов является трихотомическим . Подобно аксиоме регулярности, индукция множеств ограничивает возможные модели " " и, следовательно, теорию множеств, что было мотивацией принципа в 20-х годах. Но конструктивная теория здесь не доказывает трихотомию для всех ординалов, в то время как трихотомические ординалы плохо ведут себя по отношению к понятию преемника и ранга. ${\displaystyle \in }$ ${\displaystyle \in }$

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

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

Отношение к ZF

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

The following highlights the different readings of a formal theory. Let ${\displaystyle \mathrm {CH} }$ denote the continuum hypothesis and ${\displaystyle B:=\{z\in 1\mid \mathrm {CH} \}}$ so that ${\displaystyle 0\in B\leftrightarrow \mathrm {CH} }$. Then ${\displaystyle b:=B\cup \{1\}}$ is inhabited by ${\displaystyle 1}$ and any set that is established to be a member of ${\displaystyle b}$ either equals ${\displaystyle 0}$ or ${\displaystyle 1}$. Induction on ${\displaystyle \omega }$ implies that it cannot consistently be negated that ${\displaystyle b}$ has some least natural number member. The value of such a member can be shown to be independent of theories such as ${\displaystyle {\mathsf {ZFC}}}$. Nonetheless, any classical set theory like ${\displaystyle {\mathsf {ZFC}}}$ also proves there exists such a number.

Strong Collection

Having discussed all the weakened forms of the classical set theory axioms, Replacement and Exponentiation can be further strengthened without losing a type theoretical interpretation, and in a way that is not going beyond ${\displaystyle {\mathsf {ZF}}}$.

So firstly, one may reflect upon the strength of the axiom of replacement, also in the context of the classical set theory. For any set ${\displaystyle y}$ and any natural ${\displaystyle n}$, there exists the product ${\displaystyle y^{n}}$ recursively given by ${\displaystyle y^{n-1}\times y}$, which have ever deeper rank. Induction for unbound predicates proves that these sets exist for all of the infinitely many naturals. Replacement "for ${\displaystyle n\mapsto y^{n}}$" now moreover states that this infinite class of products can be turned into the infinite set, ${\displaystyle \{p\mid \exists (n\in \omega ).p=y^{n}\}}$. This is also not a subset of any previously established set.

Going beyond those axioms also seen in Myhill's typed approach, consider the discussed constructive theory with Exponentiation and Induction, but now strengthened by the collection schema. In ${\displaystyle {\mathsf {ZF}}}$ it is equivalent to Replacement, unless the powerset axiom is dropped. In the current context the strong axiom presented supersedes Replacement, due to not requiring the binary relation definition to be functional, but possibly multi-valued.

In words, for every total relation, there exists an image set ${\displaystyle b}$ such that the relation is total in both directions. Expressing this via a raw first-order formulation leads to a somewhat repetitive format. The antecedent states that one considers relation ${\displaystyle \phi }$ between sets ${\displaystyle x}$ and ${\displaystyle y}$ that are total over a certain domain set ${\displaystyle a}$, that is, ${\displaystyle \phi }$ has at least one "image value" ${\displaystyle y}$ for every element ${\displaystyle x}$ in the domain. This is more general than an inhabitance condition ${\displaystyle x\in y}$ in a set theoretical choice axiom, but also more general than the condition of Replacement, which demands unique existence ${\displaystyle \exists !y}$. In the consequent, firstly, the axioms states that then there exists a set ${\displaystyle b}$ which contains at least one "image" value ${\displaystyle y}$ under ${\displaystyle \phi }$, for every element of the domain. Secondly, in this axioms formulation it then moreover states that only such images ${\displaystyle y}$ are elements of that new codomain set ${\displaystyle b}$. It is guaranteeing that ${\displaystyle b}$ does not overshoot the codomain of ${\displaystyle \phi }$ and thus the axiom is also expressing some power akin to a Separation procedure. The principle may be used in the constructive study of larger sets beyond the everyday need of analysis.

Metalogic

This theory without ${\displaystyle {\mathrm {PEM} }}$, without unbounded separation and without "naive" Power set enjoys various nice properties. For example, as opposed to ${\displaystyle {\mathsf {CZF}}}$ with its subset collection schema below, it has the existence property.

Constructive Zermelo–Fraenkel

Binary refinement

The so called binary refinement axiom says that for any ${\displaystyle a}$ there exists a set ${\displaystyle {\mathcal {B}}_{a}\subset {\mathcal {P}}_{a}}$ such that for any covering ${\displaystyle a=x\cup y}$, the set ${\displaystyle {\mathcal {B}}_{a}}$ holds two subsets ${\displaystyle c\subset x}$ and ${\displaystyle d\subset y}$ that also do this covering job, ${\displaystyle a=c\cup d}$. It is a weakest form of the powerset axiom and at the core of some important mathematical proofs. Fullness below, for relations between the set ${\displaystyle a}$ and the finite ${\displaystyle \{0,1\}}$, implies that this is indeed possible.

Taking another step back, ${\displaystyle {\mathsf {ECST}}}$ plus Recursion and plus Binary refinement already proves that there exists an Archimedean, Dedekind complete pseudo-ordered field. That set theory also proves that the class of left Dedekind cuts is a set, not requiring Induction or Collection. And it moreover proves that function spaces into discrete sets are sets (there e.g. ${\displaystyle \omega \to \omega }$), without assuming ${\displaystyle {\mathrm {Exp} }}$. Already over the weak theory ${\displaystyle {\mathsf {BCST}}}$ (which is to say without Infinity) does binary refinement prove that function spaces into discrete sets are sets, and therefore e.g. the existence of all characteristic function spaces ${\displaystyle \{0,1\}^{a}}$.

Subset Collection

The theory known as ${\displaystyle {\mathsf {CZF}}}$ adopts the axioms of the previous sections plus a stronger form of Exponentiation. It is by adopting the following alternative to Exponentiation, which can again be seen as a constructive version of the Power set axiom:

An alternative that is not a schema is elaborated on below.

Fullness

For given ${\displaystyle a}$ and ${\displaystyle b}$, let ${\displaystyle {\mathcal {R}}_{ab}}$ be the class of all total relations between ${\displaystyle a}$ and ${\displaystyle b}$. This class is given as

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

As opposed to the function definition, there is no unique existence quantifier in ${\displaystyle \exists !(y\in b)}$. The class ${\displaystyle {\mathcal {R}}_{ab}}$ represents the space of "non-unique-valued functions" or "multivalued functions" from ${\displaystyle a}$ to ${\displaystyle b}$, but as set of individual pairs with right projection in ${\displaystyle b}$. The second clause says that one is concerned with only these relations, not those which are total on ${\displaystyle a}$ but also extend their domain beyond ${\displaystyle a}$.

One does not postulate ${\displaystyle {\mathcal {R}}_{ab}}$ to be a set, since with Replacement one can use this collection of relations between a set ${\displaystyle a}$ and the finite ${\displaystyle b=\{0,1\}}$, i.e. the "bi-valued functions on ${\displaystyle a}$", to extract the set ${\displaystyle {\mathcal {P}}_{a}}$ of all its subsets. In other words ${\displaystyle {\mathcal {R}}_{ab}}$ being a set would imply the Powerset axiom.

Over ${\displaystyle {\mathsf {ECTS}}+{\text{Strong Collection}}}$, there is a single, somewhat clearer alternative axiom to the Subset Collection schema. It postulates the existence of a sufficiently large set ${\displaystyle {\mathcal {S}}_{ab}}$ of total relations between ${\displaystyle a}$ and ${\displaystyle b}$.

This says that for any two sets ${\displaystyle a}$ and ${\displaystyle b}$, there exists a set ${\displaystyle {\mathcal {S}}_{ab}\subset {\mathcal {R}}_{ab}}$ which among its members inhabits a still total relation ${\displaystyle s\in {\mathcal {S}}_{ab}}$ for any given total relation ${\displaystyle r\in {\mathcal {R}}_{ab}}$.

On a given domain ${\displaystyle a}$, the functions are exactly the sparsest total relations, namely the unique valued ones. Therefore, the axiom implies that there is a set such that all functions are in it. In this way, Fullness implies Exponentiation. It further implies binary refinement, already over ${\displaystyle {\mathsf {BCST}}}$.

The Fullness axiom, as well as dependent choice, is in turn also implied by the so-called Presentation Axiom about sections, which can also be formulated category theoretically.

Metalogic of CZF

${\displaystyle {\mathsf {CZF}}}$ has the numerical existence property and the disjunctive property, but there are concessions: ${\displaystyle {\mathsf {CZF}}}$ lacks the existence property due to the Subset Collection Schema or Fullness axiom. The schema can also be an obstacle for realizability models. The existence property is not lacking when the weaker Exponentiation or the stronger but impredicative Powerset axiom axiom is adopted instead. The latter is in general lacking a constructive interpretation.

Unprovable claims

The theory is consistent with some anti-classical assertions, but on its own proves nothing not provable in ${\displaystyle {\mathsf {ZF}}}$. Some prominent statements not proven by the theory (nor by ${\displaystyle {\mathsf {IZF}}}$, for that matter) are part of the principles listed above, in the sections on constructive schools in analysis, on the Cauchy construction and on non-constructive principles. What follows concerns set theoretical concepts:

The bounded notion of a transitive set of transitive sets is a good way to define ordinals and enables induction on ordinals. But notably, this definition includes some ${\displaystyle \Delta _{0}}$-subsets in ${\displaystyle {\mathsf {CZF}}}$. So assuming that the membership of ${\displaystyle 0}$ is decidable in all successor ordinals ${\displaystyle S\alpha }$ proves ${\displaystyle {\mathrm {PEM} }}$ for bounded formulas in ${\displaystyle {\mathsf {CZF}}}$. Also, neither linearity of ordinals, nor existence of power sets of finite sets are derivable in this theory, as assuming either implies Power set. The circumstance that ordinals are better behaved in the classical than in the constructive context manifests in a different theory of large set existence postulates.

Consider the functions the domain of which is ${\displaystyle \omega }$ or some ${\displaystyle n\in \omega }$. These are sequences and their ranges are counted sets. Denote by ${\displaystyle C}$ the class characterized as the smallest codomain such that the ranges of the aforementioned functions into ${\displaystyle C}$ are also itself members of ${\displaystyle C}$. In ${\displaystyle {\mathsf {ZF}}}$, this is the set ${\displaystyle H_{\aleph _{1}}}$ of hereditarily countable sets and has ordinal rank at most ${\displaystyle \omega _{2}}$. In ${\displaystyle {\mathsf {ZF}}}$, it is uncountable (as it also contains all countable ordinals, the cardinality of which is denoted ${\displaystyle \aleph _{1}}$) but its cardinality is not necessarily that of ${\displaystyle {\mathbb {R} }}$. Meanwhile, ${\displaystyle {\mathsf {CZF}}}$ does not prove ${\displaystyle C}$ even constitutes a set, even when countable choice is assumed.

Finally, the theory does not prove that all function spaces formed from sets in the constructible universe ${\displaystyle L}$ are sets inside ${\displaystyle L}$, and this holds even when assuming Powerset instead of the weaker Exponentiation axiom. So this is a particular statement preventing ${\displaystyle {\mathsf {CZF}}}$ from proving the class ${\displaystyle L}$ to be a model of ${\displaystyle {\mathsf {CZF}}}$.

Ordinal analysis

Taking ${\displaystyle {\mathsf {CZF}}}$ and dropping set induction gives a theory that is conservative over ${\displaystyle {\mathsf {HA}}}$ for arithmetic statements, in that sense that it proves the same arithmetical statements for its ${\displaystyle {\mathsf {HA}}}$-model ${\displaystyle \omega }$. Adding back just mathematical induction gives a theory with proof theoretic ordinal ${\displaystyle \varphi (\varepsilon _{0},0)}$, which is the first common fixed point of the Veblen functions ${\displaystyle \varphi _{\beta }}$ for ${\displaystyle \beta <\varepsilon _{0}}$. This is the same ordinal as for ${\displaystyle {\mathsf {ML_{1}}}}$ and is below the Feferman–Schütte ordinal ${\displaystyle \Gamma _{0}}$. Exhibiting a type theoretical model, the full theory ${\displaystyle {\mathsf {CZF}}}$ goes beyond ${\displaystyle \Gamma _{0}}$, its ordinal still being the modest Bachmann–Howard ordinal. Assuming the class of trichotomous ordinals is a set raises the proof theoretical strength of ${\displaystyle {\mathsf {CZF}}}$ (but not of ${\displaystyle {\mathsf {IZF}}}$).

Being related to inductive definitions or bar induction, the regular extension axiom ${\displaystyle {\mathrm {REA} }}$ raises the proof theoretical strength of ${\displaystyle {\mathsf {CZF}}}$. This large set axiom, granting the existence of certain nice supersets for every set, is proven by ${\displaystyle {\mathsf {ZFC}}}$.

Models

The category of sets and functions of ${\displaystyle {\mathsf {CZF}}+{\mathrm {REA} }}$ is a ${\displaystyle \Pi W}$-pretopos. Without diverging into topos theory, certain extended such ${\displaystyle \Pi W}$-pretopoi contain models of ${\displaystyle {\mathsf {CZF}}+{\mathrm {REA} }}$. The effective topos contains a model of this ${\displaystyle {\mathsf {CZF}}+{\mathrm {REA} }}$ based on maps characterized by certain good subcountability properties.

Separation, stated redundantly in a classical context, is constructively not implied by Replacement. The discussion so far only committed to the predicatively justified bounded Separation. Note that full Separation (together with ${\displaystyle {\mathrm {RDC} }}$, ${\displaystyle {\mathrm {MP} }}$ and also ${\displaystyle {\mathrm {IP} }}$ for sets) is validated in some effective topos models, meaning the axiom does not spoil cornerstones of the restrictive recursive school.

Related are type theoretical interpretations. In 1977 Aczel showed that ${\displaystyle {\mathsf {CZF}}}$ can still be interpreted in Martin-Löf type theory,^[26] using the propositions-as-types approach. More specifically, this uses one universe and ${\displaystyle W}$-types, providing what is now seen a standard model of ${\displaystyle {\mathsf {CZF}}}$ in ${\displaystyle {\mathsf {ML_{1}V}}}$.^[27]This is done in terms of the images of its functions and has a fairly direct constructive and predicative justification, while retaining the language of set theory. Roughly, there are two "big" types ${\displaystyle U,V}$, the sets are all given through any ${\displaystyle f\colon A\to V}$ on some ${\displaystyle A\colon U}$, and membership of a ${\displaystyle x}$ in the set is defined to hold when ${\displaystyle \exists (a\colon A).f(a)=x}$. Conversely, ${\displaystyle {\mathsf {CZF}}}$ interprets ${\displaystyle {\mathsf {ML_{1}V}}}$. All statements validated in the subcountable model of the set theory can be proven exactly via ${\displaystyle {\mathsf {CZF}}}$ plus the choice principle ${\displaystyle \Pi \Sigma }$- ${\displaystyle \mathrm {AC} }$, stated further above. As noted, theories like ${\displaystyle {\mathsf {CZF}}}$, and also together with choice, have the existence property for a broad class of sets in common mathematics. Martin-Löf type theories with additional induction principles validate corresponding set theoretical axioms.

Soundness and Completeness theorems of ${\displaystyle {\mathsf {CZF}}}$, with respect to realizability, have been established.

Breaking with ZF

One may of course add a Church's thesis.

One may postulate the subcountability of all sets. This already holds true in the type theoretical interpretation and the model in the effective topos. By Infinity and Exponentiation, ${\displaystyle \omega \to \omega }$ is an uncountable set, while the class ${\displaystyle {\mathcal {P}}_{\omega }}$ or even ${\displaystyle {\mathcal {P}}_{1}}$ is then provenly not a set, by Cantor's diagonal argument. So this theory then logically rejects Powerset and of course ${\displaystyle {\mathrm {PEM} }}$. Subcountability is also in contradiction with various large set axioms. (On the other hand, also using ${\displaystyle {\mathsf {CZF}}}$, some such axioms imply the consistency of theories such as ${\displaystyle {\mathsf {ZF}}}$ and stronger.)

As a rule of inference, ${\displaystyle {\mathsf {CZF}}}$ is closed under Troelstra's general uniformity for both ${\displaystyle z=\omega }$ and ${\displaystyle z=\{0,1\}}$. One may adopt it as an anti-classical axiom schema, the uniformity principle which may be denoted ${\displaystyle {\mathrm {UP} }}$,

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

This also is incompatible with the powerset axiom. The principle is also often formulated for ${\displaystyle z=\omega }$. Now for a binary set of labels ${\displaystyle z=\{0,1\}}$, ${\displaystyle {\mathrm {UP} }}$ implies the indecomposability schema ${\displaystyle {\mathrm {UZ} }}$, as noted.

In 1989 Ingrid Lindström showed that non-well-founded sets can also be interpreted in Martin-Löf type theory, which are obtained by replacing Set Induction in ${\displaystyle {\mathsf {CZF}}}$ with Aczel's anti-foundation axiom.^[28] The resulting theory ${\displaystyle {\mathsf {CZFA}}}$ may be studied by also adding back the ${\displaystyle \omega }$-induction schema or relativized dependent choice, as well as the assertion that every set is member of a transitive set.

Intuitionistic Zermelo–Fraenkel

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

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 ${\displaystyle {\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 ${\displaystyle {\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 ${\displaystyle \{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 ${\displaystyle {\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 ${\displaystyle \forall x.{\big (}0\in x\lor 0\notin x{\big )}}$, the principle that knowledge of membership of ${\displaystyle 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 ${\displaystyle {\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 ${\displaystyle \omega \to \omega }$ being subcountable. It also has the disjunctive property.

${\displaystyle {\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 ${\displaystyle {\mathsf {IZF}}}$ as formulated does not. The combination of schemas including full separation spoils it.

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

Intuitionistic Z

Again on the weaker end, as with its historical counterpart Zermelo set theory, one may denote by ${\displaystyle {\mathsf {IZ}}}$ the intuitionistic theory set up like ${\displaystyle {\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 ${\displaystyle {\mathsf {IKP}}}$. It has not only Separation but also Collection restricted to ${\displaystyle \Delta _{0}}$-formulas, i.e. it is similar to ${\displaystyle {\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 ${\displaystyle {\mathsf {IKP}}}$ are obtained by restricting the induction schema to narrower classes of formulas, say ${\displaystyle \Sigma _{1}}$. The theory is especially weak when studied without Infinity.

Sorted theories

Constructive set theory

As he presented it, Myhill's system ${\displaystyle {\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 ${\displaystyle \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 ${\displaystyle {\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 " ${\displaystyle \in }$" directly. A theory like the Elementary Theory of the Categories Of Set ( ${\displaystyle {\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

References

1. Feferman, Solomon (1998), In the Light of Logic, New York: Oxford University Press, pp. 280–283, 293–294, ISBN 0-195-08030-0
2. Troelstra, A. S., van Dalen D., Constructivism in mathematics: an introduction 1; Studies in Logic and the Foundations of Mathematics; Springer, 1988;
3. Bridges D., Ishihara H., Rathjen M., Schwichtenberg H. (Editors), Handbook of Constructive Mathematics; Studies in Logic and the Foundations of Mathematics; (2023) pp. 20-56
4. Myhill, "Some properties of Intuitionistic Zermelo-Fraenkel set theory", Proceedings of the 1971 Cambridge Summer School in Mathematical Logic (Lecture Notes in Mathematics 337) (1973) pp. 206-231
5. Crosilla, Laura; Set Theory: Constructive and Intuitionistic ZF; Stanford Encyclopedia of Philosophy; 2009
6. Peter Aczel and Michael Rathjen, Notes on Constructive Set Theory, Reports Institut Mittag-Leffler, Mathematical Logic - 2000/2001, No. 40
7. John L. Bell, Intuitionistic Set Theorys, 2018
8. Jeon, Hanul (2022), "Constructive Ackermann's interpretation", Annals of Pure and Applied Logic, 173 (5): 103086, arXiv:2010.04270, doi:10.1016/j.apal.2021.103086, S2CID 222271938
9. Shapiro, S., McCarty, C. & Rathjen, M., Intuitionistic sets and numbers: small set theory and Heyting arithmetic, https://doi.org/10.1007/s00153-024-00935-4, Arch. Math. Logic (2024)
10. Gambino, N. (2005). "Presheaf models for constructive set theories" (PDF). In Laura Crosilla and Peter Schuster (ed.). From Sets and Types to Topology and Analysis (PDF). pp. 62–96. doi:10.1093/acprof:oso/9780198566519.003.0004. ISBN 9780198566519.
11. Scott, D. S. (1985). Category-theoretic models for Intuitionistic Set Theory. Manuscript slides of a talk given at Carnegie-Mellon University
12. Benno van den Berg, Predicative topos theory and models for constructive set theory, Netherlands University, PhD thesis, 2006
13. Jech, Thomas (2003), Set Theory, Springer Monographs in Mathematics (Third Millennium ed.), Berlin, New York: Springer-Verlag, p. 642, ISBN 978-3-540-44085-7, Zbl 1007.03002
14. Gert Smolka, Set Theory in Type Theory, Lecture Notes, Saarland University, Jan. 2015
15. Gert Smolka and Kathrin Stark, Hereditarily Finite Sets in Constructive Type Theory, Proc. of ITP 2016, Nancy, France, Springer LNCS, May 2015
16. Diener, Hannes (2020). "Constructive Reverse Mathematics". arXiv:1804.05495 [math.LO].
17. Sørenson, Morten; Urzyczyn, Paweł (1998), Lectures on the Curry-Howard Isomorphism, CiteSeerX 10.1.1.17.7385, p. 239
18. Smith, Peter (2007). An introduction to Gödel's Theorems (PDF). Cambridge, U.K.: Cambridge University Press. ISBN 978-0-521-67453-9. MR 2384958., p. 297
19. Pradic, Pierre; Brown, Chad E. (2019). "Cantor-Bernstein implies Excluded Middle". arXiv:1904.09193 [math.LO].
20. Michael Rathjen, Choice principles in constructive and classical set theories, Cambridge University Press: 31 March 2017
21. Gitman, Victoria (2011), What is the theory ZFC without power set, arXiv:1110.2430
22. Shulman, Michael (2019), "Comparing material and structural set theories", Annals of Pure and Applied Logic, 170 (4): 465-504, arXiv:1808.05204, doi:10.1016/j.apal.2018.11.002
23. Errett Bishop, Foundations of Constructive Analysis, July 1967
24. Robert S. Lubarsky, On the Cauchy Completeness of the Constructive Cauchy Reals, July 2015
25. Matthew Ralph John Hendtlass, Constructing fixed points and economic equilibria, PhD Thesis, University of Leeds, April 2013
26. Aczel, Peter: 1978. The type theoretic interpretation of constructive set theory. In: A. MacIntyre et al. (eds.), Logic Colloquium '77, Amsterdam: North-Holland, 55–66.
27. Rathjen, M. (2004), "Predicativity, Circularity, and Anti-Foundation" (PDF), in Link, Godehard (ed.), One Hundred Years of Russell ́s Paradox: Mathematics, Logic, Philosophy, Walter de Gruyter, ISBN 978-3-11-019968-0
28. Lindström, Ingrid: 1989. A construction of non-well-founded sets within Martin-Löf type theory. Journal of Symbolic Logic 54: 57–64.

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