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

Эта статья о взглядах на философию математики. Чтобы узнать о других значениях этого термина, см. Конструктивизм .

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

Существует множество форм конструктивизма. программа интуиционизма, Брауэром , финитизм Гильберта и К ним относятся Бернейса , конструктивная рекурсивная математика Шанина основанная и Маркова , Бишопа программа конструктивного анализа . Конструктивизм также включает изучение конструктивных теорий множеств, таких как CZF , и изучение теории топоса .

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

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

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

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

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

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

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

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

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

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

$\forall n\ \forall i,j\geq g(n)\quad |f(i)-f(j)|\leq {1 \over n}$

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

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

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

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

$\forall n:\exists m:\forall i,j\geq m:|f(i)-f(j)|\leq {1 \over n}$

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

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

Кардинальность

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

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

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

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

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

В интуиционистских теориях теории типов (особенно в арифметике высших типов) разрешены многие формы аксиомы выбора. Например, аксиому AC ₁₁ можно перефразировать так, что для любого отношения R на множестве действительных чисел, если вы доказали, что для каждого действительного числа x существует действительное число y такое, что выполняется R ( x , y ), тогда на самом деле существует функция F такая, что R ( x , F ( x )) выполняется для всех действительных чисел. Аналогичные принципы выбора принимаются для всех конечных типов. Мотивацией принятия этих, казалось бы, неконструктивных принципов является интуиционистское понимание доказательства того, что «для каждого действительного числа x существует такое действительное число y , что выполняется R ( x , y )». Согласно интерпретации БХК функцией F. , это доказательство само по себе является искомой Принципы выбора, которые принимают интуиционисты, не подразумевают закон исключенного третьего .

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

Теория меры

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

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

Традиционно некоторые математики с подозрением, если не враждебно, относились к математическому конструктивизму, главным образом из-за ограничений, которые, по их мнению, он накладывал на конструктивный анализ.Эти взгляды были ярко выражены Давидом Гильбертом в 1928 году, когда он писал в «Основах математики» : «Принять принцип исключенного третьего у математика было бы то же самое, что, скажем, запретить телескоп астроному или боксёру использовать его кулаки».

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

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

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

внесшие большой вклад в

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

Филиалы

• Конструктивная логика
• Конструктивная теория типов
• Конструктивный анализ
• Конструктивный нестандартный анализ

См. также

• Теория вычислимости - Исследование вычислимых функций и степеней Тьюринга.
• Конструктивное доказательство - Метод доказательства в математике.
• Финитизм - философия математики, признающая существование только конечных математических объектов.
• Семантика игры – подход к формальной семантике. Страницы, отображающие описания викиданных в качестве запасного варианта.
• Обитаемое множество - свойство множеств, используемых в конструктивной математике.
• Интуиционизм - подход в философии математики и логики.
• Интуиционистская теория типов - Альтернативные основы математики

Ссылки

• Бисон, Майкл Дж. (1985). Основы конструктивной математики: метаматематические исследования . 9783540121732. ISBN  9783540121732 .

• Бишоп, Эрретт (1967). Основы конструктивного анализа . Нью-Йорк: Академическая пресса. ISBN  4-87187-714-0 .

• Бриджес, Дуглас ; Ричман, Фред (1987). Разновидности конструктивной математики . Издательство Кембриджского университета. дои : 10.1017/CBO9780511565663 .

• Эдвардс, Гарольд Мортимер (2005). Очерки по конструктивной математике . Спрингер-Верлаг. ISBN  0-387-21978-1 .

• Феферман, Соломон (1997). Отношения между конструктивными, предикативными и классическими системами анализа (PDF) .

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

• Троэльстра, Энн Шерп (1977a). «Аспекты конструктивной математики». Справочник по математической логике . 90 : 973–1052. дои : 10.1016/S0049-237X(08)71127-3 .

• Троэльстра, Энн Шерп (1977b). Последовательности выбора: глава интуиционистской математики . Издательство Оксфордского университета. ISBN  0-19-853163-Х .

• Троэльстра, Энн Шерп ; Ван Дален, Дирк (1988a). Конструктивизм в математике: Введение, Том 1 . ElsevierScience. ISBN  9780444702661 .

• Троэльстра, Энн Шерп ; Ван Дален, Дирк (1988b). Конструктивизм в математике: Введение, Том 2 . ElsevierScience. ISBN  9780444703583 .

• Троэльстра, Энн Шерп (1991). История конструктивизма в 20 веке (PDF) . Амстердамский университет, серия предварительных публикаций ITLI ML-91-05. Архивировано из оригинала 9 февраля 2006 г. Проверено 9 июля 2019 г. {{cite book}}: CS1 maint: bot: исходный статус URL неизвестен ( ссылка )

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

• «Конструктивная математика» . Интернет-энциклопедия философии .
• Статья в Стэнфордской энциклопедии философии