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

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

Введение

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

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

Логические предварительные сведения

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

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

Неразрешимые предикаты

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

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

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

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

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

даже если эти утверждения о дизъюнкции не несут никакой информации. В отсутствие дальнейших аксиом, нарушающих металогические свойства, вместо этого конструктивный вывод обычно отражает доказуемость. Запретные утверждения, которые не должны быть разрешимы (если цель состоит в том, чтобы соблюсти интерпретацию доказуемости конструктивных утверждений), могут быть разработаны для определений пользовательской эквивалентности». $\cong$» а также в формализациях, приведенных ниже. Что касается импликаций дизъюнкций еще не доказанных или опровергнутых утверждений, говорят о слабых брауэровских контрпримерах .

Порядок против дизъюнкций

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

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

Как объяснялось, различные предикаты не будут разрешимы в конструктивной формулировке, например, сформированной из теоретико-порядковых отношений. Сюда входит " $\cong$", что будет эквивалентно отрицанию. Важнейшие дизъюнкции теперь обсуждаются подробно.

Трихотомия

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

$\neg (x>0\lor 0>x)\to x\cong 0$

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

$(x>0\lor 0>x)\lor x\cong 0$

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

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

Отделение

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

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

может быть определено независимо и представляет собой отношение обособленности . При этом замена вышеприведенных принципов дает герметичность.

$\neg (x\#0)\leftrightarrow (x\cong 0)$

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

$\neg \neg (x\cong y)\leftrightarrow (x\cong y)$

Само неуловимое трихотомическое расхождение тогда читается

$(x\#0)\lor \neg (x\#0)$

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

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

Нестрогий частичный порядок

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

Согласно действующему закону Де Моргана , соединение таких высказываний также рассматривается как отрицание обособленности, и, таким образом,

$(x\geq y\land y\geq x)\leftrightarrow (x\cong y)$

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

Вариации

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

Обратимость

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

Формализация

Рациональные последовательности

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

Модули

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

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

Границы и супремы

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

Формализация епископа

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

Вариации

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

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

Кодирование

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

Теория множеств

Реалы Коши

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

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

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

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

Интервальная арифметика

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

Несчетность

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

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

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

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

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

Теория категорий и типов

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

Принципы

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

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

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

Антиклассические

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

Теоремы

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

Теорема

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

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

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

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

наименьшей верхней границы

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

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

См. также

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

Дальнейшее чтение

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