WikiDer > Конструктивизм (философия математики)

Constructivism (philosophy of mathematics)

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

Есть много форм конструктивизма.^[1] К ним относится программа интуиционизм основан Брауэр, то финитизм из Гильберта и Бернейс, конструктивная рекурсивная математика Шанин и Марков, и Епископпрограмма конструктивный анализ. Конструктивизм также включает изучение конструктивные теории множеств Такие как CZF и изучение теория топоса.

Конструктивизм часто отождествляют с интуиционизмом, хотя интуиционизм - лишь одна из конструктивистских программ. Интуиционизм утверждает, что основы математики лежат в интуиции отдельного математика, что делает математику внутренне субъективной деятельностью.^[2] Другие формы конструктивизма не основаны на этой интуитивной точке зрения и совместимы с объективной точкой зрения на математику.

Конструктивная математика

В конструктивной математике много интуиционистская логика, что по сути классическая логика без закон исключенного среднего. Этот закон гласит, что для любого предложения либо это предложение истинно, либо его отрицание. Это не означает, что полностью отрицается закон исключенного третьего; особые случаи закона будут доказуемы. Просто общий закон не рассматривается как аксиома. В закон непротиворечия (в котором говорится, что противоречащие друг другу утверждения не могут быть правдой одновременно) по-прежнему в силе.

Например, в Арифметика Гейтинга, можно доказать, что для любого предложения п который не содержит кванторы, ${displaystyle forall x, y, z, ldots в mathbb {N}: pvee, например, p}$ это теорема (где Икс, у, z ... являются свободные переменные в предложении п). В этом смысле предложения, ограниченные конечный до сих пор считаются истинными или ложными, как в классической математике, но это двухвалентность не распространяется на предложения, относящиеся к бесконечный коллекции.

Фактически, L.E.J. Брауэр, основатель интуиционистской школы, рассматривал закон исключенного третьего как абстрагированный от конечного опыта, а затем примененный к бесконечному без оправдание. Например, Гипотеза Гольдбаха - это утверждение, что каждое четное число (больше 2) является суммой двух простые числа. Для любого конкретного четного числа можно проверить, является ли оно суммой двух простых чисел (например, с помощью исчерпывающего поиска), поэтому любое из них является либо суммой двух простых чисел, либо нет. И до сих пор каждое из протестированных таким образом было фактически суммой двух простых чисел.

Но нет никаких известных доказательств того, что все они таковы, или какого-либо известного доказательства того, что не все из них таковы. Таким образом, по мнению Брауэра, мы не имеем права утверждать, что «либо гипотеза Гольдбаха верна, либо нет». И хотя гипотеза может быть однажды решена, аргумент применим к аналогичным нерешенным проблемам; для Брауэра закон исключенного среднего был равносилен предположению, что каждый математическая проблема имеет решение.

За исключением аксиомы закона исключенного третьего, оставшиеся логическая система имеет свойство существования в этой классической логике нет: всякий раз ${displaystyle существует _ {xin X} P (x)}$ доказано конструктивно, то на самом деле ${displaystyle P (a)}$ доказано конструктивно (по крайней мере) для одного конкретного ${displaystyle ain X}$ , часто вызывается свидетелем. Таким образом, доказательство существования математического объекта связано с возможностью его построения.

Пример из реального анализа

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

В конструктивной математике один из способов построить действительное число - это функция ƒ который принимает положительное целое число ${displaystyle n}$ и выводит рациональную ƒ(п) вместе с функцией грамм который принимает положительное целое число п и выводит положительное целое число грамм(п) такие, что

{displaystyle forall n forall i, jgeq g (n) quad | f (i) -f (j) | leq {1 over n}}

так что как п увеличивается, значения ƒ(п) становятся все ближе и ближе друг к другу. Мы можем использовать ƒ и грамм вместе, чтобы вычислить как можно ближе рациональное приближение к действительному числу, которое они представляют.

Согласно этому определению, простое представление действительного числа е является:

{displaystyle f (n) = sum _ {i = 0} ^ {n} {1 over i!}, quad g (n) = n.}

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

{displaystyle forall n: существует m: forall i, jgeq m: | f (i) -f (j) | leq {1 over n}}

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

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

Мощность

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

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

Тем не менее, можно было ожидать, что, поскольку Т является частичной функцией натуральных чисел на действительные числа, поэтому действительные числа равны не более чем счетный. И поскольку каждое натуральное число может быть тривиально представлены как действительные числа, поэтому действительные числа не менее чем счетный. Поэтому они точно счетный. Однако это рассуждение не является конструктивным, так как оно все еще не строит требуемую биекцию. Классическая теорема, доказывающая существование биекции в таких обстоятельствах, а именно Теорема Кантора – Бернштейна – Шредера., неконструктивен. Недавно было показано, что Теорема Кантора – Бернштейна – Шредера. подразумевает закон исключенного среднего, поэтому конструктивного доказательства теоремы быть не может.^[3]

Аксиома выбора

Статус аксиома выбора в конструктивной математике осложняется разными подходами разных конструктивистских программ. Одно банальное значение слова «конструктивный», неформально используемое математиками, - это «доказуемо в Теория множеств ZF без аксиомы выбора ». Однако сторонники более ограниченных форм конструктивной математики утверждали бы, что ZF сама по себе не является конструктивной системой.

В интуиционистских теориях теория типов (особенно в арифметике высшего типа) разрешены многие формы аксиомы выбора. Например, аксиома AC₁₁ можно перефразировать, чтобы сказать, что для любого отношения р на множестве действительных чисел, если вы доказали, что для каждого действительного числа Икс есть реальное число у такой, что р(Икс,у), то действительно существует функция F такой, что р(Икс,F(Икс)) выполняется для всех действительных чисел. Аналогичные принципы выбора приняты для всех конечных типов. Мотивацией для принятия этих, казалось бы, неконструктивных принципов является интуиционистское понимание доказательства того, что «для каждого действительного числа Икс есть реальное число у такой, что р(Икс,у) выполняется ". Толкование BHK, само это доказательство является, по сути, функцией F это желательно. Принципы выбора, которые принимают интуиционисты, не подразумевают закон исключенного среднего.

Однако в некоторых системах аксиом для конструктивной теории множеств выбранная аксиома действительно подразумевает закон исключенного третьего (при наличии других аксиом), как показано Теорема Диаконеску-Гудмана-Майхилла. Некоторые конструктивные теории множеств включают более слабые формы аксиомы выбора, такие как аксиома зависимого выбора в теории множеств Майхилла.

Теория меры

Классический теория меры принципиально неконструктивен, поскольку классическое определение Мера Лебега не описывает способ вычисления меры набора или интеграла функции. На самом деле, если рассматривать функцию как правило, которое «вводит действительное число и выводит действительное число», тогда не может быть никакого алгоритма для вычисления интеграла функции, поскольку любой алгоритм мог бы вызывать только конечное число значений функции за раз, и конечного числа значений недостаточно для вычисления интеграла с любой нетривиальной точностью. Решение этой загадки, впервые представленное в книге Бишопа 1967 года, состоит в том, чтобы рассматривать только функции, которые записаны как поточечный предел непрерывных функций (с известным модулем непрерывности), с информацией о скорости сходимости. Преимущество конструктивизации теории меры состоит в том, что если можно доказать, что множество конструктивно имеет полную меру, то существует алгоритм для нахождения точки в этом множестве (снова см. Книгу Бишопа). Например, этот подход можно использовать для построения действительного числа, которое нормальный на каждую базу.^{[нужна цитата]}

Место конструктивизма в математике

Традиционно некоторые математики относились к математическому конструктивизму с подозрением, если не антагонизмом, в основном из-за ограничений, которые, по их мнению, он создавал для конструктивного анализа. Дэвид Гильберт в 1928 году, когда он писал в Grundlagen der Mathematik«Принятие принципа исключенного третьего из математика было бы тем же самым, что, скажем, запретить астроному или боксеру пользоваться телескопом кулаками».^[4]

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

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

Физик Ли Смолин пишет в Три пути к квантовой гравитации эта теория топоса является «правильной формой логики для космологии» (стр. 30) и «В своих первых формах она называлась« интуиционистской логикой »(стр. 31). "В такой логике утверждения, которые наблюдатель может сделать о Вселенной, делятся по крайней мере на три группы: те, которые мы можем судить как истинные, те, которые мы можем судить как ложные, и те, истину которых мы не можем определить на настоящее время »(стр. 28).

Математики, внесшие большой вклад в конструктивизм

Леопольд Кронекер (старый конструктивизм, полуинтуиционизм)
Л. Э. Дж. Брауэр (основатель интуиционизма)
Марков А.А. (праотец русской школы конструктивизма)
Аренд Хейтинг (формализованная интуиционистская логика и теории)
Пер Мартин-Лёф (основоположник теорий конструктивного типа)
Эрретт Бишоп (продвигал версию конструктивизма, утверждавшую, что она совместима с классической математикой)
Пол Лоренцен (разработан конструктивный анализ)

ветви

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

Примечания

^ Troelstra 1977a: 974
^ Троельстра 1977b: 1
^ Прадич, Пьер; Браун, Чад Э. (19 апреля 2019 г.). «Кантор-Бернштейн подразумевает исключенное среднее». arXiv:1904.09193 [math.LO].
^ Стэнфордская энциклопедия философии: Конструктивная математика.

внешняя ссылка

[1] Troelstra 1977a: 974

[2] Троельстра 1977b: 1

[3] Прадич, Пьер; Браун, Чад Э. (19 апреля 2019 г.). «Кантор-Бернштейн подразумевает исключенное среднее». arXiv:1904.09193 [math.LO].

[4] Стэнфордская энциклопедия философии: Конструктивная математика.

[1]

[2]

[3]

[4]

Navigation