Конструктивизм (философия математики) - Constructivism (philosophy of mathematics)

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

Есть много форм конструктивизма. Они включают в себя программу интуитивизма основанную Брауэра , в Финитизм из Гильберта и Бернайсом , по конструктивным рекурсивные математики из Шанина и Маркова , и епископ программы «s в конструктивном анализе . Конструктивизм также включает изучение конструктивных теорий множеств, таких как CZF, и изучение теории топосов .

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

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

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

Например, в арифметике Гейтинга можно доказать, что любое предложение p , не содержащее кванторов , является теоремой (где x , y , z ... - свободные переменные в предложении p ). В этом смысле предложения, ограниченные конечным , по-прежнему считаются либо истинными, либо ложными, как и в классической математике, но эта двойственность не распространяется на предложения, относящиеся к бесконечным коллекциям.

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

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

С исключением закона исключенного третьего в качестве аксиомы, оставшаяся логическая система обладает свойством существования , которого нет у классической логики: всякий раз, когда доказывается конструктивно, фактически доказывается конструктивно (по крайней мере) для одной конкретной , часто называемой свидетель. Таким образом, доказательство существования математического объекта связано с возможностью его построения.

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

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

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

так что с увеличением 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 года « Основы конструктивного анализа» работал над тем, чтобы развеять эти опасения, развивая большую часть традиционного анализа в конструктивных рамках.

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

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

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

ветви

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

Примечания

использованная литература

внешние ссылки