Конструктивный анализ

В математике конструктивный анализ — это математический анализ , выполняемый в соответствии с некоторыми принципами конструктивной математики .

Название предмета контрастирует с классическим анализом , который в этом контексте означает анализ, выполненный в соответствии с более общими принципами классической математики. Однако существуют различные школы мысли и множество различных формализаций конструктивного анализа. ^[1] Будь то классический или конструктивный в некотором роде, любой такой каркас анализа аксиоматизирует действительную числовую линию некоторыми средствами, набором, расширяющим рациональные числа , и с отношением обособленности , определяемым из асимметричной порядковой структуры. Центральное место занимает предикат положительности, здесь обозначаемый , который управляет равенством нулю . Члены набора обычно называются просто действительными числами . Хотя этот термин, таким образом, перегружен в предмете, все каркасы разделяют широкое общее ядро ​​результатов, которые также являются теоремами классического анализа.${\displaystyle х>0}$${\displaystyle x\cong 0}$

Конструктивные рамки для его формулировки являются расширениями арифметики Гейтинга по типам, включая , конструктивную арифметику второго порядка или достаточно сильные топосные , типные или конструктивные теории множеств, такие как , конструктивный аналог . Конечно, можно также изучить и прямую аксиоматизацию .${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {ZF}}}$

Базовая логика конструктивного анализа — интуиционистская логика , что означает, что принцип исключенного третьего не предполагается автоматически для каждого предложения . Если предложение доказуемо, это в точности означает, что утверждение о несуществовании, будучи доказуемым, было бы абсурдным, и поэтому последнее также не может быть доказуемым в последовательной теории. Утверждение о существовании с двойным отрицанием является логически отрицательным утверждением и подразумевается, но, как правило, не эквивалентно самому утверждению о существовании. Многие из сложностей конструктивного анализа можно сформулировать в терминах слабости предложений логически отрицательной формы , которая, как правило, слабее, чем . В свою очередь, также импликация, как правило, не может быть обращена.${\displaystyle {\mathrm {PEM}}}$${\displaystyle \neg \neg \exists x.\theta (x)}$${\displaystyle \neg \exists x.\theta (x)}$${\displaystyle \neg \neg \phi }$${\displaystyle \фи}$${\displaystyle {\big (}\exists x.\theta (x){\big )}\to \neg \forall x.\neg \theta (x)}$

Хотя конструктивная теория доказывает меньше теорем, чем ее классический аналог в ее классическом представлении, она может демонстрировать привлекательные металогические свойства. Например, если теория демонстрирует свойство дизъюнкции , то если она доказывает дизъюнкцию , то также или . Уже в классической арифметике это нарушается для самых основных предложений о последовательностях чисел - как показано далее.${\displaystyle {\mathsf {T}}}$${\displaystyle {\mathsf {T}}\vdash \phi \lor \psi }$${\displaystyle {\mathsf {T}}\vdash \phi }$${\displaystyle {\mathsf {T}}\vdash \psi }$

Распространенная стратегия формализации действительных чисел заключается в терминах последовательностей или рациональных чисел, и поэтому мы приводим мотивацию и примеры в их терминах. Итак, чтобы определить термины, рассмотрим разрешимый предикат на натуральных числах, который в конструктивном просторечии означает доказуемость, и пусть будет характеристической функцией, определенной как точно равная, где является истинным. Связанная последовательность является монотонной, со значениями, не строго растущими между границами и . Здесь, ради демонстрации, определяя экстенсиональное равенство нулевой последовательности , следует, что . Обратите внимание, что символ " " здесь используется в нескольких контекстах. Для любой теории, охватывающей арифметику, существует много еще нерешенных и даже доказанно независимых таких утверждений . Два примера - гипотеза Гольдбаха и предложение Россера теории. ${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$${\displaystyle \forall n.{\big (}Q(n)\lor \neg Q(n){\big )}}$${\displaystyle \chi _{Q}\colon {\mathbb {N} }\to \{0,1\}}$${\displaystyle 0}$${\displaystyle Q}$${\displaystyle q_{n}\,:=\,{\textstyle \sum }_{k=0}^{n}\chi _{Q}(n)/2^{n+1}}$${\displaystyle 0}$${\displaystyle 1}$${\displaystyle (q\cong _{\mathrm {ext} }0)\,:=\,\forall n.q_{n}=0}$${\displaystyle q\cong _{\mathrm {ext}}0\leftrightarrow \forall nQ(n)}$${\displaystyle 0}$${\displaystyle \forall nQ(n)}$${\displaystyle \Пи _{1}^{0}}$

Рассмотрим любую теорию с кванторами, ранжирующими примитивно рекурсивные , рационально-значные последовательности. Уже минимальная логика доказывает непротиворечивость утверждения для любого предложения, и что отрицание исключенного среднего для любого данного предложения было бы абсурдным. Это также означает, что не существует последовательной теории (даже если она антиклассическая), отвергающей дизъюнкцию исключенного среднего для любого данного предложения. Действительно, она утверждает, что${\displaystyle {\mathsf {T}}}$

${\displaystyle {\mathsf {T}}\,\,\,\vdash \,\,\,\forall (x\in {\mathbb {Q} }^{\mathbb {N} }).\,\neg \neg {\big (}(x\cong _{\mathrm {ext} }0)\lor \neg (x\cong _{\mathrm {ext} }0){\big )}}$

Эта теорема логически эквивалентна утверждению о несуществовании последовательности, для которой исключенная средняя дизъюнкция о равенстве нулю была бы опровержимой. Никакая последовательность с этой отвергнутой дизъюнкцией не может быть представлена. Предположим, что рассматриваемые теории последовательны и арифметически обоснованы. Теперь теоремы Гёделя означают, что существует явная последовательность , такая, которая для любой фиксированной точности доказывает, что нулевая последовательность является хорошим приближением к , но также можно металогически установить, что также как и . ^[2] Здесь это предложение снова равнозначно предложению универсально квантифицированной формы. Тривиально${\displaystyle g\in {\mathbb {Q} }^{\mathbb {N} }}$${\displaystyle {\mathsf {T}}}$${\displaystyle г}$${\displaystyle {\mathsf {T}}\,\nvdash \,(g\cong _{\mathrm {ext} }0)}$${\displaystyle {\mathsf {T}}\,\nvdash \,\neg (g\cong _{\mathrm {ext} }0)}$${\displaystyle g\cong _ {\ mathrm {ext} }0}$

${\displaystyle {\mathsf {T}}+{\mathrm {PEM} }\,\,\,\vdash \,\,\,\forall (x\in {\mathbb {Q} }^{\mathbb {N} }).\,(x\cong _{\mathrm {ext} }0)\lor \neg (x\cong _{\mathrm {ext} }0)}$

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

Теория действительного замкнутого поля может быть аксиоматизирована таким образом, что все нелогические аксиомы соответствуют конструктивным принципам. Это касается коммутативного кольца с постулатами для предиката положительности , с положительной единицей и неположительным нулем, т.е. и . В любом таком кольце можно определить , что составляет строгий полный порядок в его конструктивной формулировке (также называемый линейным порядком или, чтобы быть точным в контексте, псевдопорядком ) . Как обычно, определяется как .${\displaystyle х>0}$${\displaystyle 1>0}$${\displaystyle \отрицательный (0>0)}$${\displaystyle y>x\,:=\,(yx>0)}$${\displaystyle х<0}$${\displaystyle 0>х}$

Эта теория первого порядка актуальна, поскольку структуры, обсуждаемые ниже, являются ее моделями. ^[3] Однако этот раздел, таким образом, не касается аспектов, родственных топологии , и соответствующие арифметические подструктуры в нем не определяются .

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

В интуитонистической логике дизъюнктивный силлогизм в форме вообще действительно идет только в -направлении. В псевдопорядке, один имеет${\displaystyle (\phi \lor \psi)\to (\neg \phi \to \psi)}$${\displaystyle \to}$

${\displaystyle \neg (x>0\lor 0>x)\to x\cong 0}$

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

${\displaystyle (x>0\lor 0>x)\lor x\cong 0}$

См. аналитический${\displaystyle {\mathrm {LPO} }}$ . Другие дизъюнкции, однако, подразумеваются на основе других результатов положительности, например . Аналогично, асимметричный порядок в теории должен удовлетворять слабому свойству линейности для всех , связанному с локализацией действительных чисел.${\displaystyle (x+y>0)\to (x>0\lor y>0)}$${\displaystyle (y>x)\to (y>t\or t>x)}$${\displaystyle т}$

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

В контексте анализа вспомогательный логически положительный предикат

${\displaystyle x\#y\,:=\,(x>y\lor y>x)}$

может быть независимо определена и составляет отношение обособленности . С ней заменитель принципов выше дает плотность

${\displaystyle \neg (x\#0)\leftrightarrow (x\cong 0)}$

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

${\displaystyle \neg \neg (x\cong y)\leftrightarrow (x\cong y)}$

Неуловимая трихотомическая дизъюнкция сама по себе читается так:

${\displaystyle (x\#0)\lor \neg (x\#0)}$

Важно, что доказательство дизъюнкции несет положительную информацию${\displaystyle x\#y}$ , в обоих смыслах этого слова. Через это также следует, что . На словах: Демонстрация того, что число каким-то образом отличается от нуля, также является демонстрацией того, что это число не равно нулю. Но конструктивно из этого не следует, что дважды отрицательное утверждение будет подразумевать . Следовательно, многие классически эквивалентные утверждения разветвляются на отдельные утверждения. Например, для фиксированного многочлена и фиксированного утверждение о том, что '-й коэффициент отличается от нуля, сильнее, чем просто утверждение о том, что он не равен нулю. Демонстрация первого объясняет, как и ноль связаны, относительно предиката упорядочивания на действительных числах, в то время как демонстрация второго показывает, как отрицание таких условий будет подразумевать противоречие. В свою очередь, тогда также существует сильное и более свободное понятие, например, быть многочленом третьего порядка.${\displaystyle (\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )}$${\displaystyle x\#0\to \neg (x\cong 0)}$${\displaystyle \neg (x\cong 0)}$${\displaystyle x\#0}$${\displaystyle p\in {\mathbb {R} }[x]}$${\displaystyle k\in {\mathbb {N} }}$${\displaystyle к}$${\displaystyle а_{к}}$${\displaystyle p}$${\displaystyle а_{к}}$

Таким образом, исключенное среднее для априори сильнее, чем для . Однако см. обсуждение возможных дальнейших аксиоматических принципов относительно силы " " ниже.${\displaystyle x\#0}$${\displaystyle x\cong 0}$${\displaystyle \конг}$

Наконец, отношение может быть определено или доказано эквивалентным логически отрицательному утверждению , и тогда определяется как . Разрешимость позитивности может быть выражена таким образом как , что, как отмечено, не будет доказуемо в общем случае. Но также не будет доказана и дизъюнкция тотальности , см. также аналитическое .${\displaystyle 0\geq x}$${\displaystyle \neg (x>0)}$${\displaystyle x\leq 0}$${\displaystyle 0\geq x}$${\displaystyle x>0\lor 0\geq x}$${\displaystyle x\geq 0\lor 0\geq x}$${\displaystyle {\mathrm {LLPO} }}$

Согласно закону Де Моргана , соединение таких утверждений также становится отрицанием их отдельности, и поэтому

${\displaystyle (x\geq y\land y\geq x)\leftrightarrow (x\cong y)}$

Дизъюнкция подразумевает , но другое направление также не доказуемо в общем случае. В конструктивном вещественном замкнутом поле отношение " " является отрицанием и не эквивалентно дизъюнкции в общем случае .${\displaystyle x>y\lor x\cong y}$${\displaystyle x\geq y}$${\displaystyle \geq }$

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

В коммутативном кольце действительных чисел доказуемо необратимый элемент равен нулю. Эта и самая базовая структура локальности абстрагируется в теории полей Гейтинга .

Обычный подход заключается в идентификации действительных чисел с помощью неизменяемых последовательностей в . Постоянные последовательности соответствуют рациональным числам. Алгебраические операции, такие как сложение и умножение, могут быть определены покомпонентно вместе с систематической переиндексацией для ускорения. Определение в терминах последовательностей, кроме того, позволяет определить строгий порядок " ", удовлетворяющий желаемым аксиомам. Другие отношения, обсуждавшиеся выше, затем могут быть определены в его терминах. В частности, любое число, кроме , т. е . , в конечном итоге имеет индекс, за пределами которого все его элементы обратимы. ^[4] Различные импликации между отношениями, а также между последовательностями с различными свойствами, затем могут быть доказаны.${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$${\displaystyle >}$${\displaystyle x}$${\displaystyle 0}$${\displaystyle x\#0}$

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

Модуль сходимости часто используется в конструктивном изучении последовательностей Коши действительных чисел, то есть требуется ассоциация любого с соответствующим индексом (за пределами которого последовательности ближе, чем ) в форме явной, строго возрастающей функции . Такой модуль можно рассматривать для последовательности действительных чисел, но его также можно рассматривать для всех действительных чисел, и в этом случае мы фактически имеем дело с последовательностью пар.${\displaystyle \varepsilon >0}$${\displaystyle \varepsilon }$${\displaystyle \varepsilon \mapsto N(\varepsilon )}$

При наличии такой модели можно определить больше теоретико-множественных понятий. Для любого подмножества действительных чисел можно говорить о верхней границе , отрицательно характеризуемой с помощью . Можно говорить о наименьших верхних границах относительно " ". Супремум — это верхняя граница, заданная через последовательность действительных чисел, положительно характеризуемая с помощью " ". Если подмножество с верхней границей ведет себя хорошо относительно " " (обсуждается ниже), оно имеет супремум.${\displaystyle b}$${\displaystyle x\leq b}$${\displaystyle \leq }$${\displaystyle <}$${\displaystyle <}$

Одна формализация конструктивного анализа, моделирующая свойства порядка, описанные выше, доказывает теоремы для последовательностей рациональных чисел, удовлетворяющих условию регулярности . Альтернативой является использование более тесного вместо , и в последнем случае должны использоваться ненулевые индексы. Никакие два рациональных элемента в регулярной последовательности не находятся дальше друг от друга, и поэтому можно вычислить натуральные числа, превосходящие любое действительное число. Для регулярных последовательностей определяется логически положительное свойство слабой положительности как , где отношение в правой части выражается через рациональные числа. Формально положительное действительное число в этом языке является регулярной последовательностью вместе с естественной свидетельствующей положительностью. Кроме того, , что логически эквивалентно отрицанию . Это доказуемо транзитивно и, в свою очередь, является отношением эквивалентности . С помощью этого предиката регулярные последовательности в полосе считаются эквивалентными нулевой последовательности. Такие определения, конечно, совместимы с классическими исследованиями, и их вариации также были хорошо изучены ранее. Можно иметь как . Также может быть определено из числового свойства неотрицательности, как для всех , но затем показано, что оно эквивалентно логическому отрицанию первого. ^{[5] [6]}${\displaystyle x}$${\displaystyle |x_{n}-x_{m}|\leq {\tfrac {1}{n}}+{\tfrac {1}{m}}}$${\displaystyle 2^{-n}}$${\displaystyle {\tfrac {1}{n}}}$${\displaystyle {\tfrac {3}{2}}}$${\displaystyle x>0\,:=\,\exists n.x_{n}>{\tfrac {1}{n}}}$${\displaystyle x\cong y\,:=\,\forall n.|x_{n}-y_{n}|\leq {\tfrac {2}{n}}}$${\displaystyle \neg \exists n.|x_{n}-y_{n}|>{\tfrac {2}{n}}}$${\displaystyle |x_{n}|\leq {\tfrac {2}{n}}}$${\displaystyle y>x}$${\displaystyle (y-x)>0}$${\displaystyle x\geq 0}$${\displaystyle x_{n}\geq -{\tfrac {1}{n}}}$${\displaystyle n}$

Вышеприведенное определение использует общую границу . Другие формализации напрямую принимают в качестве определения, что для любой фиксированной границы числа и должны в конечном итоге быть по крайней мере так же близки. Экспоненциально падающие границы также используются, также скажем, в условии действительного числа , и аналогично для равенства двух таких действительных чисел. И также последовательности рациональных чисел могут потребоваться для переноса модуля сходимости. Свойства положительности могут быть определены как в конечном итоге навсегда разделенные некоторым рациональным числом.${\displaystyle x\cong y}$${\displaystyle {\tfrac {2}{n}}}$${\displaystyle {\tfrac {2}{N}}}$${\displaystyle x}$${\displaystyle y}$${\displaystyle 2^{-n}}$${\displaystyle \forall n.|x_{n}-x_{n+1}|<2^{-n}}$

Выбор функции или более строгие принципы помогают таким структурам.${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$

Стоит отметить, что последовательности в можно закодировать довольно компактно, поскольку каждая из них может быть сопоставлена ​​уникальному подклассу . Последовательность рациональных чисел можно закодировать как набор четверок . В свою очередь, это можно закодировать как уникальные натуральные числа с использованием фундаментальной теоремы арифметики . Существуют также более экономичные функции спаривания или теги кодирования расширений или метаданные. Для примера, использующего эту кодировку, последовательность , или , может использоваться для вычисления числа Эйлера , и с помощью приведенной выше кодировки она отображается на подкласс . Хотя этот пример, явная последовательность сумм, изначально является полной рекурсивной функцией , кодировка также означает, что эти объекты находятся в области действия квантификаторов в арифметике второго порядка.${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$${\displaystyle {\mathbb {N} }}$${\displaystyle i\mapsto {\tfrac {n_{i}}{d_{i}}}(-1)^{s_{i}}}$${\displaystyle \langle i,n_{i},d_{i},s_{i}\rangle \in {\mathbb {N} }^{4}}$${\displaystyle 2^{i}\cdot 3^{n_{i}}\cdot 5^{d_{i}}\cdot 7^{s_{i}}}$${\displaystyle i\mapsto {\textstyle \sum }_{k=0}^{i}{\tfrac {1}{k}}}$${\displaystyle 1,2,{\tfrac {5}{2}},{\tfrac {8}{3}},\dots }$${\displaystyle \{15,90,24300,6561000,\dots \}}$${\displaystyle {\mathbb {N} }}$

В некоторых рамках анализа название действительных чисел дается таким хорошо ведущим себя последовательностям или рациональным числам, а такие отношения называются равенством или действительными числами . Обратите внимание, однако, что существуют свойства, которые позволяют различать два -связанных действительных числа.${\displaystyle x\cong y}$${\displaystyle \cong }$

Напротив, в теории множеств, которая моделирует натуральные числа и подтверждает существование даже классически несчетных функциональных пространств (и, конечно, скажем, или даже ), числа, эквивалентные относительно " " в , могут быть собраны в набор, и тогда это называется действительным числом Коши . На этом языке регулярные рациональные последовательности деградируют до простого представителя действительного числа Коши. Равенство этих действительных чисел затем задается равенством множеств, которое регулируется теоретико-множественной аксиомой экстенсиональности . Результатом является то, что теория множеств докажет свойства для действительных чисел, т. е. для этого класса множеств, выраженных с помощью логического равенства. Конструктивные действительные числа при наличии соответствующих аксиом выбора будут полными по Коши, но не будут автоматически полными по порядку. ^[7]${\displaystyle {\mathbb {N} }}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {ZFC}}}$${\displaystyle \cong }$${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$

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

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

Напомним, что предпорядок кардиналов " " в теории множеств является основным понятием, определяемым как существование инъекции . В результате конструктивная теория кардинального порядка может существенно расходиться с классической. Здесь множества, такие как или некоторые модели вещественных чисел, можно считать подсчетными .${\displaystyle \leq }$${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$

Тем не менее, диагональная конструкция Кантора, доказывающая несчетность множеств типа и простых функциональных пространств типа, является интуиционистски обоснованной. Предполагая или, в качестве альтернативы, аксиому счетного выбора , модели всегда несчетны также и над конструктивной структурой. ^[8] Один из вариантов диагональной конструкции, релевантный для настоящего контекста, может быть сформулирован следующим образом, доказанным с использованием счетного выбора и для вещественных чисел как последовательностей рациональных чисел: ^[9]${\displaystyle {\mathcal {P}}{\mathbb {N} }}$${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathbb {R} }}$

Для любых двух пар действительных чисел и любой последовательности действительных чисел существует действительное число с и .${\displaystyle a<b}$${\displaystyle x_{n}}$${\displaystyle z}$${\displaystyle a<z<b}$${\displaystyle \forall (n\in {\mathbb {N} }).x_{n}\,\#\,z}$

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

По словам Канамори , «историческое искажение было увековечено, что связывает диагонализацию с неконструктивностью», а конструктивный компонент диагонального аргумента уже появился в работе Кантора. ^[10]

Все эти соображения могут быть также рассмотрены в топосе или соответствующей теории зависимого типа.

В практической математике аксиома зависимого выбора принята в различных школах.

Принцип Маркова принят в русской школе рекурсивной математики. Этот принцип усиливает влияние доказанного отрицания строгого равенства. Так называемая аналитическая форма его допускает или . Могут быть сформулированы более слабые формы.${\displaystyle \neg (x\leq 0)\to x>0}$${\displaystyle \neg (x\cong 0)\to x\#0}$

Брауэровская школа рассуждает в терминах спредов и принимает классически обоснованную индукцию бара .

Благодаря необязательному принятию дополнительных последовательных аксиом отрицание разрешимости может быть доказуемо. Например, равенство нулю отвергается как разрешимое при принятии принципов непрерывности Брауэра или тезиса Чёрча в рекурсивной математике. ^[11] Слабый принцип непрерывности, а также даже опровергают . Существование последовательности Шпеккера доказано из . Такие явления также встречаются в топосах реализуемости . Примечательно, что существуют две антиклассические школы как несовместимые друг с другом. В этой статье обсуждаются принципы, совместимые с классической теорией, и выбор делается явно.${\displaystyle {\mathrm {CT} _{0}}}$${\displaystyle x\geq 0\lor 0\geq x}$${\displaystyle {\mathrm {CT} _{0}}}$

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

В качестве простого примера рассмотрим теорему о промежуточном значении (IVT). В классическом анализе IVT подразумевает, что для любой непрерывной функции f из замкнутого интервала [ a , b ] до действительной прямой R , если f ( a ) отрицательно , а f ( b ) положительно , то существует действительное число c в интервале, такое, что f ( c ) равно нулю . В конструктивном анализе это не выполняется, поскольку конструктивная интерпретация экзистенциальной квантификации («существует») требует, чтобы можно было построить действительное число c (в том смысле, что его можно приблизить с любой желаемой точностью рациональным числом ). Но если f колеблется около нуля во время растяжения вдоль своей области определения, то это не обязательно может быть сделано.

Однако конструктивный анализ предоставляет несколько альтернативных формулировок IVT, все из которых эквивалентны обычной форме в классическом анализе, но не в конструктивном анализе. Например, при тех же условиях на f , что и в классической теореме, при любом натуральном числе n (независимо от того, насколько оно велико), существует (то есть мы можем построить) действительное число c _n в интервале такое, что абсолютное значение f ( c _n ) меньше 1/ n . То есть мы можем подобраться к нулю так близко, как нам хочется, даже если мы не можем построить c, которое даст нам точно ноль.

В качестве альтернативы мы можем сохранить тот же вывод, что и в классическом IVT — единственное c , такое что f ( c ) равно нулю, — при этом усилив условия на f . Мы требуем, чтобы f была локально ненулевой , то есть для любой точки x в интервале [ a , b ] и любого натурального числа m существует (мы можем построить) действительное число y в интервале такое, что | y - x | < 1/ m и | f ( y )| > 0. В этом случае можно построить желаемое число c . Это сложное условие, но есть несколько других условий, которые его подразумевают и которые обычно выполняются; например, каждая аналитическая функция локально ненулевая (предполагая, что она уже удовлетворяет f ( a ) < 0 и f ( b ) > 0).

Чтобы рассмотреть этот пример по-другому, обратите внимание, что согласно классической логике , если локально ненулевое условие не выполняется, то оно должно не выполняться в некоторой конкретной точке x ; и тогда f ( x ) будет равно 0, так что IVT автоматически действителен. Таким образом, в классическом анализе, который использует классическую логику, для доказательства полного IVT достаточно доказать конструктивную версию. С этой точки зрения полный IVT не выполняется в конструктивном анализе просто потому, что конструктивный анализ не принимает классическую логику. Наоборот, можно утверждать, что истинным значением IVT, даже в классической математике, является конструктивная версия, включающая локально ненулевое условие, с полным IVT, следующим за «чистой логикой» впоследствии. Некоторые логики, признавая, что классическая математика верна, все же считают, что конструктивный подход дает лучшее понимание истинного значения теорем, во многом таким образом.

Другое различие между классическим и конструктивным анализом заключается в том, что конструктивный анализ не доказывает принцип наименьшей верхней границы , т. е. что любое подмножество действительной прямой R будет иметь наименьшую верхнюю границу (или супремум), возможно бесконечную. Однако, как и в случае с теоремой о промежуточном значении, альтернативная версия выживает; в конструктивном анализе любое локализованное подмножество действительной прямой имеет супремум. (Здесь подмножество S из R локализовано , если, когда x < y — действительные числа, либо существует элемент s из S такой, что x < s , либо y — верхняя граница S .) Опять же, это классически эквивалентно полному принципу наименьшей верхней границы, поскольку каждое множество локализовано в классической математике. И снова, хотя определение локализованного множества является сложным , тем не менее ему удовлетворяют многие обычно изучаемые множества, включая все интервалы и все компактные множества .

Тесно связано с этим, в конструктивной математике, меньшее количество характеристик компактных пространств конструктивно допустимы — или с другой точки зрения, есть несколько различных концепций, которые классически эквивалентны, но не конструктивно эквивалентны. Действительно, если бы интервал [ a , b ] был последовательно компактен в конструктивном анализе, то классический IVT следовал бы из первой конструктивной версии в примере; можно было бы найти c как точку кластера бесконечной последовательности ( c _n ) _{n ∈ N.}

• Вычислимая аналитика
• Конструктивный нестандартный анализ
• Гейтинговое поле
• Неразложимость (конструктивная математика)
• Псевдо-порядок

• Бишоп, Эрретт (1967). Основы конструктивного анализа . ISBN 4-87187-714-0.
• Бриджер, Марк (2007). Реальный анализ: конструктивный подход . Hoboken: Wiley. ISBN 0-471-79230-6.