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

Математический анализ

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

Введение

Название предмета контрастирует с классическим анализом , который в данном контексте означает анализ, проводимый в соответствии с более общими принципами классической математики . Однако существуют различные школы мысли и множество различных формализаций конструктивного анализа. ^[1] Любая такая система анализа, будь то классическая или конструктивная в некотором роде, каким-то образом аксиоматизирует линию действительных чисел , набор, расширяющий рациональные числа и с отношением обособленности , определяемым из асимметричной структуры порядка. В центре внимания находится предикат положительности, обозначаемый здесь , который управляет равенством нулю . Членами коллекции обычно называют просто действительные числа . Хотя этот термин, таким образом, перегружен в данном предмете, все концепции имеют общее ядро ​​результатов, которые также являются теоремами классического анализа. ${\displaystyle x>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 \phi }$ ${\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 n.Q(n)}$ ${\displaystyle 0}$ ${\displaystyle \forall n.Q(n)}$ ${\displaystyle \Pi _{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 g}$ ${\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 \cong }$

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

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

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

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

Трихотомия

В интуиционистской логике дизъюнктивный силлогизм в форме обычно идет только в -направлении. В псевдопорядке имеется ${\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\lor t>x)}$ ${\displaystyle t}$

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

Апартность

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

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

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

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

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

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

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

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

Наконец, отношение может быть определено логически отрицательным утверждением или доказать его эквивалентность , а затем определяется как . Разрешимость положительности, таким образом, может быть выражена как , что, как уже отмечалось, в общем случае не доказуемо. Но не будет и тотальной дизъюнкции , см. также аналитическую . ${\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 {\mathrm {PEM} }}$

Несчетность

Напомним, что предпорядок кардиналов " " в теории множеств является основным понятием, определяемым как существование инъекции . В результате конструктивная теория кардинального порядка может существенно расходиться с классической. Здесь множества, подобные некоторым моделям действительных чисел, можно считать подсчетными . ${\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 в интервале такое, что | у - х | < 1/ м и | ж ( у )| > 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} .

Смотрите также

• Математический портал

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

Рекомендации

1. Троелстра А.С., ван Дален Д., Конструктивизм в математике: введение 1 ; Исследования по логике и основам математики; Спрингер, 1988 г.;
2. Смит, Питер (2007). Введение в теоремы Гёделя. Кембридж, Великобритания: Издательство Кембриджского университета. ISBN 978-0-521-67453-9. МР  2384958.
3. Эрик Палмгрен, Интуиционистская аксиоматизация реальных закрытых полей , Mathematical Logic Quarterly, том 48, выпуск 2, страницы: 163-320, февраль 2002 г.
4. Бриджес Д., Исихара Х., Ратьен М., Швихтенберг Х. (редакторы), Справочник по конструктивной математике ; Исследования по логике и основам математики; (2023) стр. 201-207.
5. Эрретт Бишоп, Основы конструктивного анализа , июль 1967 г.
6. Столценберг, Габриэль (1970). «Обзор: Эрретт Бишоп, Основы конструктивного анализа». Бык. амер. Математика. Соц. 76 (2): 301–323. дои : 10.1090/s0002-9904-1970-12455-7 .
7. Роберт С. Любарский, О полноте Коши конструктивных вещественных чисел Коши, июль 2015 г.
8. Бауэр, А., Хэнсон, Дж. А. «Счетные реалы», 2022 г.
9. См., например, теорему 1 у Бишопа, 1967, с. 25
10. Акихиро Канамори , «Математическое развитие теории множеств от Кантора до Коэна», Бюллетень символической логики / Том 2 / Выпуск 01 / Март 1996 г., стр. 1-71
11. Динер, Ханнес (2020). «Конструктивная обратная математика». arXiv : 1804.05495 ​​[math.LO].

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

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