Войти
В философии математики конструктивизм утверждает, что это необходимо найти (или «построить») математический объект, чтобы доказать, что он существует. В классической математике можно доказать существование математического объекта, не «обнаруживая» этот объект явно, допуская его несуществование и затем выводя противоречие из этого предположения. Это доказательство от противного конструктивно некорректно. Конструктивная точка зрения включает верификационную интерпретацию квантора существования , что противоречит его классической интерпретации.
Есть много форм конструктивизма. К ним относятся программа интуиционизма, основанная Брауэром, финитизм Гильберта и Бернейс, конструктивная рекурсивная математика Шанина и Маркова и программа Бишопа конструктивного анализа . Конструктивизм также включает изучение теорий конструктивных множеств, таких как CZF, и изучение теории топосов.
. Конструктивизм часто отождествляется с интуиционизмом, хотя интуиционизм - лишь одна из конструктивистских программ.. Интуиционизм утверждает, что основы математики лежат в интуиции отдельного математика, что делает математику внутренне субъективной деятельностью. Другие формы конструктивизма не основаны на этой интуитивной точке зрения и совместимы с объективной точкой зрения на математику.
Конструктивная математика во многом использует интуиционистская логика, которая по сути является классической логикой без закона исключенного третьего. Этот закон гласит, что для любого предложения либо это утверждение истинно, либо его отрицание. Это не означает, что полностью отрицается закон исключенного третьего; особые случаи закона будут доказуемы. Просто общий закон не рассматривается как аксиома . Закон непротиворечивости (который гласит, что противоречащие друг другу утверждения не могут одновременно быть правдой) по-прежнему действует.
Например, в арифметике Гейтинга можно доказать, что для любого предложения p, не содержащего кванторов, 
Фактически, L.E.J. Брауэр, основатель школы интуиционизма, рассматривал закон исключенного третьего как абстрагированный от конечного опыта, а затем примененный к бесконечному без оправдания. Например, гипотеза Гольдбаха - это утверждение, что каждое четное число (больше 2) является суммой двух простых чисел. Для любого конкретного четного числа можно проверить, является ли оно суммой двух простых чисел (например, с помощью исчерпывающего поиска), поэтому любое из них является либо суммой двух простых чисел, либо нет. И до сих пор каждое из протестированных таким образом было фактически суммой двух простых чисел.
Но нет ни известных доказательств того, что все они таковы, ни какого-либо известного доказательства того, что не все из них таковы. Таким образом, по мнению Брауэра, мы не имеем права утверждать, что «либо гипотеза Гольдбаха верна, либо нет». И хотя однажды гипотеза может быть решена, аргумент применим к аналогичным нерешенным проблемам; для Брауэра закон исключенного третьего был равносилен предположению, что каждая математическая проблема имеет решение.
За исключением аксиомы закона исключенного третьего, оставшаяся логическая система имеет свойство существования, которого нет в классической логике: всякий раз, когда 
В классическом реальном анализе один из способов определить действительное число - это класс эквивалентности из последовательностей Коши из рациональных чисел.
В конструктивной математике одним из способов построения действительного числа является функция ƒ, которая принимает положительное целое число 
так, чтобы как n увеличивается, значения ƒ (n) становятся все ближе друг к другу. Мы можем использовать ƒ и g вместе, чтобы вычислить как можно более точное рациональное приближение к действительному числу, которое они представляют.
Согласно этому определению, простое представление действительного числа e :
Это определение соответствует классическому определению с использованием Коши последовательности, за исключением конструктивного поворота: для классической последовательности Коши требуется, чтобы для любого заданного расстояния существовал (в классическом смысле) член в последовательности, после которого все элементы находятся ближе друг к другу чем это расстояние. В конструктивной версии требуется, чтобы для любого заданного расстояния можно было фактически указать точку в последовательности, где это происходит (эта требуемая спецификация часто называется модулем сходимости ). Фактически, стандартная конструктивная интерпретация математического утверждения
в точности существует функции, вычисляющей модуль сходимости. Таким образом, различие между двумя определениями действительных чисел можно рассматривать как различие в интерпретации утверждения «для всех... существует...»
Тогда возникает вопрос о том, какой вид из функции из счетного набора в счетный набор, такой как f и g выше, могут быть фактически созданы. По этому поводу расходятся разные версии конструктивизма. Конструкции могут быть определены в широком смысле, как последовательности свободного выбора, что является интуиционистским взглядом, или в узком смысле, как алгоритмы (или, более технически, вычислимые функции ), или даже оставить неопределенными. Если, например, взять алгоритмическое представление, то построенные здесь действительные числа по сути представляют собой то, что классически можно было бы назвать вычислимыми числами.
. Принятие алгоритмической интерпретации, приведенной выше, казалось бы противоречивым. с классическими представлениями о мощности. Путем перечисления алгоритмов мы можем классически показать, что вычислимые числа являются счетными. И все же диагональный аргумент Кантора показывает, что действительные числа имеют более высокую мощность. Более того, диагональный аргумент кажется вполне конструктивным. Отождествлять действительные числа с вычислимыми числами было бы противоречием.
И на самом деле диагональный аргумент Кантора является конструктивным в том смысле, что при взаимно однозначном соотношении между действительными числами и натуральными числами создается неподходящее действительное число, и тем самым доказывает противоречие. Мы действительно можем перечислить алгоритмы для построения функции T, относительно которой мы изначально предполагаем, что это функция от натуральных чисел на вещественных чисел. Но для каждого алгоритма может существовать или не соответствовать действительное число, поскольку алгоритм может не удовлетворять ограничениям или даже не завершаться (T - частичная функция ), поэтому это не может произвести требуемую биекцию. Короче говоря, тот, кто придерживается точки зрения, что действительные числа (индивидуально) эффективно вычислимые, интерпретирует результат Кантора как показывающий, что действительные числа (в совокупности) не рекурсивно перечислимы.
Тем не менее, можно ожидать, что, поскольку T является частичным функция натуральных чисел на действительные числа, поэтому действительные числа не более чем счетные. И поскольку каждое натуральное число может быть тривиально представлено как действительное число, поэтому действительные числа не менее чем счетные. Следовательно, они точно счетны. Однако это рассуждение неконструктивно, так как оно все еще не строит требуемую биекцию. Классическая теорема, доказывающая существование биекции в таких обстоятельствах, а именно теорема Кантора – Бернштейна – Шредера, неконструктивна. Недавно было показано, что теорема Кантора – Бернштейна – Шредера влечет за собой закон исключенного третьего, следовательно, не может быть конструктивного доказательства теоремы.
Статус аксиомы выбора в конструктивной математике усложняется различными подходами различных конструктивистских программ. Одно тривиальное значение слова «конструктивный», неформально используемое математиками, - «доказуемо в теории множеств ZF без аксиомы выбора». Однако сторонники более ограниченных форм конструктивной математики будут утверждать, что ZF сама по себе не является конструктивной системой.
В интуиционистских теориях теории типов (особенно в арифметике более высокого типа) допускаются многие формы аксиомы выбора. Например, аксиому AC 11 можно перефразировать, чтобы сказать, что для любого отношения R на множестве действительных чисел, если вы доказали, что для каждого действительного числа x существует действительное число y такое, что R ( x, y), то на самом деле существует функция F такая, что R (x, F (x)) выполняется для всех действительных чисел. Аналогичные принципы выбора приняты для всех конечных типов. Мотивом принятия этих, казалось бы, неконструктивных принципов является интуиционистское понимание доказательства того, что «для каждого действительного числа x существует действительное число y такое, что выполняется R (x, y)». Согласно интерпретации BHK, это доказательство само по себе является желаемой функцией F. Принципы выбора, которые принимают интуиционисты, не подразумевают закон исключенного третьего.
. Однако в некоторых системах аксиом для конструктивной теории множеств аксиома выбора действительно подразумевает закон исключенного третьего (при наличии другого аксиомы), как показывает теорема Диаконеску-Гудмана-Майхилла. Некоторые конструктивные теории множеств включают более слабые формы аксиомы выбора, такие как аксиома зависимого выбора в теории множеств Майхилла.
Классическая теория меры принципиально неконструктивна, поскольку классическое определение меры Лебега не описывает никаких способов вычисления мера множества или интеграл функции. На самом деле, если рассматривать функцию как правило, которое «вводит действительное число и выводит действительное число», тогда не может быть никакого алгоритма для вычисления интеграла функции, поскольку любой алгоритм мог бы вызывать только конечное число значений функции за раз, и конечного числа значений недостаточно для вычисления интеграла с любой нетривиальной точностью. Решение этой загадки, впервые представленное в книге Бишопа 1967 года, состоит в том, чтобы рассматривать только функции, которые записаны как поточечный предел непрерывных функций (с известным модулем непрерывности), с информацией о скорости сходимости. Преимущество конструктивизации теории меры состоит в том, что если можно доказать, что набор конструктивно имеет полную меру, то существует алгоритм для нахождения точки в этом наборе (снова см. Книгу Бишопа). Например, этот подход можно использовать для построения действительного числа, которое нормально для каждого основания.
Традиционно некоторые математики подозрительно, если не антагонистично, по отношению к математическому конструктивизму, в основном из-за ограничений, которые, по их мнению, он создает для конструктивного анализа. Эти взгляды были решительно выражены Дэвидом Гильбертом в 1928 году, когда он написал в Grundlagen der Mathematik : «Использование принципа исключенного среднего из математика было бы то же самое, скажем, как запрет на использование телескопа астрономом или боксером кулаками ".
Эрретт Бишоп в своей работе 1967 года Основы конструктивного анализа попытался развеять эти страхи за счет развития традиционного анализа в конструктивных рамках.
Хотя большинство математиков не принимают тезис конструктивистов о том, что только математика, основанная на конструктивных методах, является правильной, конструктивные методы вызывают все больший интерес по неидеологическим причинам. Например, конструктивные доказательства в анализе могут гарантировать, что работа в рамках ограничений конструктивных методов может упростить поиск свидетелей теорий, чем использование классических методов. Приложения для конструктивной математики также были найдены в типизированных лямбда-исчислениях, теории топосов и категориальной логике, которые являются известными предметами фундаментальной математики и информатики.. В алгебре для таких объектов, как topoi и алгебры Хопфа, структура поддерживает внутренний язык, который является конструктивной теорией; работа в рамках ограничений этого языка часто бывает более интуитивной и гибкой, чем работа извне с помощью таких средств, как рассуждения о множестве возможных конкретных алгебр и их гомоморфизмах.
Физик Ли Смолин пишет в Три пути к квантовой гравитации эта теория топоса является «правильной формой логики для космологии» (стр. 30) и «В своих первых формах она называлась« интуиционистской логикой »(стр. 31). "В такой логике утверждения, которые наблюдатель может сделать о Вселенной, делятся по крайней мере на три группы: те, которые мы можем судить как истинные, те, которые мы можем судить как ложные, и те, истину которых мы не можем определить на настоящее время »(стр. 28).
