Введение

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

Введение

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

Логические предпосылки

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

Порядок против разъединений

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

Трихотомия

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

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

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

Вариации

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

Инвертируемость

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

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

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

Модули

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

Границы и верховенство

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

Официальное удостоверение епископа

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

Вариации

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

Кодирование

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

Реали Коши

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

Дедекинды реальные

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

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

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

Недопустимость

Напомним, что предзаказ на кардиналах "" в теории множеств является основным понятием, определяемым существованием инъекции. В результате, конструктивная теория кардинального порядка может существенно отличаться от классической. Здесь множества, такие как или некоторые модели вещественных чисел, могут считаться счетными. Тем не менее, диагональный аргумент Кантора, доказывающий несчетность множеств мощностей, например, и обычных функциональных пространств, например, интуиционистски верен. Предполагая или, альтернативно, аксиому счетного выбора, модели всегда несчетны также и в конструктивном контексте. Один из вариантов диагонального аргумента, релевантный для данного контекста, может быть сформулирован следующим образом, доказанный с использованием счетного выбора и для вещественных чисел, представленных как последовательности рациональных чисел: Для любой пары вещественных чисел и любой последовательности вещественных чисел существует вещественное число с и Представления вещественных чисел с использованием явных модулей позволяют рассматривать их отдельно. По словам Канамори, "исторически сложилось заблуждение, связывающее диагонализацию с неконструктивностью", и конструктивный компонент диагонального аргумента уже присутствовал в работах Кантора.

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

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

Принципы

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

Антиклассические школы

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

Теоремы

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

Теорема промежуточных значений

Для простого примера рассмотрим теорему о промежуточном значении (IVT). В классическом анализе IVT утверждает, что для любой непрерывной функции f, отображающей замкнутый интервал [a, b] на действительную прямую R, если f(a) отрицательна, а f(b) положительна, то в интервале существует действительное число c, такое что f(c) равна точно нулю. В конструктивном анализе это не всегда верно, поскольку конструктивная интерпретация квантора существования ("существует") требует возможности построить это действительное число c (в том смысле, что его можно приблизить к любой желаемой точности рациональным числом). Но если f колеблется вблизи нуля на некотором участке своей области определения, то это не всегда возможно. Однако конструктивный анализ предоставляет несколько альтернативных формулировок IVT, все из которых эквивалентны обычной форме в классическом анализе, но не в конструктивном. Например, при тех же условиях на f, что и в классической теореме, для любого натурального числа n (каким бы большим оно ни было), существует (то есть мы можем построить) действительное число cn в интервале, такое что абсолютная величина f(cn) меньше 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] был последовательно компактным в конструктивном анализе, то классическая теорема о промежуточных значениях следовала бы из первой конструктивной версии, приведённой в примере: можно было бы найти c как точку накопления бесконечной последовательности (cn)n∈N.