В философии математики конструктивизм утверждает, что необходимо найти (или «построить») конкретный пример математического объекта, чтобы доказать, что пример существует. Напротив, в классической математике можно доказать существование математического объекта , не «находя» этот объект явно, предполагая его несуществование и затем выводя противоречие из этого предположения. Такое доказательство от противного можно назвать неконструктивным, и конструктивист может его отвергнуть. Конструктивная точка зрения включает в себя проверочную интерпретацию квантора существования , которая противоречит его классической интерпретации.
Существует множество форм конструктивизма. [1] К ним относятся программа интуиционизма , основанная Брауэром , финитизм Гильберта и Бернайса , конструктивная рекурсивная математика Шанина и Маркова и программа конструктивного анализа Бишопа . [2] Конструктивизм также включает изучение конструктивных теорий множеств, таких как CZF , и изучение теории топосов .
Конструктивизм часто отождествляют с интуиционизмом, хотя интуиционизм — это лишь одна из конструктивистских программ. Интуиционизм утверждает, что основы математики лежат в интуиции отдельного математика, тем самым превращая математику в изначально субъективную деятельность. [3] Другие формы конструктивизма не основаны на этой точке зрения на интуицию и совместимы с объективной точкой зрения на математику.
Большая часть конструктивной математики использует интуиционистскую логику , которая по сути является классической логикой без закона исключенного третьего . Этот закон гласит, что для любого предложения либо это предложение истинно, либо его отрицание истинно. Это не означает, что закон исключенного третьего полностью отрицается; особые случаи закона будут доказуемы. Просто общий закон не принимается как аксиома . Закон непротиворечивости (который гласит, что противоречивые утверждения не могут быть оба истинными одновременно) по-прежнему действителен.
Например, в арифметике Гейтинга можно доказать, что для любого предложения p , не содержащего квантификаторов , является теоремой (где x , y , z ... — свободные переменные в предложении p ). В этом смысле предложения, ограниченные конечным, по -прежнему считаются либо истинными, либо ложными, как в классической математике, но эта двузначность не распространяется на предложения, которые относятся к бесконечным наборам.
Фактически, LEJ Brouwer , основатель школы интуиционистов, рассматривал закон исключенного третьего как абстрагированный от конечного опыта, а затем примененный к бесконечному без обоснования . Например, гипотеза Гольдбаха — это утверждение, что каждое четное число, большее 2, является суммой двух простых чисел . Можно проверить для любого конкретного четного числа, является ли оно суммой двух простых чисел (например, с помощью исчерпывающего поиска), поэтому любое из них либо является суммой двух простых чисел, либо нет. И до сих пор каждое проверенное таким образом число фактически было суммой двух простых чисел.
Но нет известных доказательств того, что все они таковы, и нет никаких известных доказательств того, что не все они таковы; и даже неизвестно, должно ли существовать доказательство или опровержение гипотезы Гольдбаха (гипотеза может быть неразрешимой в традиционной теории множеств ZF). Таким образом, по Брауэру, мы не имеем права утверждать «либо гипотеза Гольдбаха верна, либо нет». И хотя гипотеза может быть однажды решена, аргумент применим к похожим нерешенным проблемам. По Брауэру, закон исключенного третьего равносилен предположению, что каждая математическая задача имеет решение.
При исключении закона исключенного третьего в качестве аксиомы оставшаяся логическая система имеет свойство существования , которого нет в классической логике: всякий раз, когда доказывается конструктивно, то фактически доказывается конструктивно для (по крайней мере) одного конкретного , часто называемого свидетелем . Таким образом, доказательство существования математического объекта связано с возможностью его построения.
В классическом вещественном анализе одним из способов определения вещественного числа является определение его как класса эквивалентности последовательностей Коши рациональных чисел .
В конструктивной математике одним из способов построения действительного числа является использование функции ƒ, которая принимает положительное целое число и выводит рациональное число ƒ ( n ), вместе с функцией g , которая принимает положительное целое число n и выводит положительное целое число g ( n ), такое что
так что по мере увеличения n значения ƒ ( n ) становятся все ближе и ближе друг к другу. Мы можем использовать ƒ и g вместе, чтобы вычислить настолько близкое рациональное приближение, насколько нам нужно, к действительному числу, которое они представляют.
Согласно этому определению, простое представление действительного числа e имеет вид:
Это определение соответствует классическому определению с использованием последовательностей Коши, за исключением конструктивного поворота: для классической последовательности Коши требуется, чтобы для любого заданного расстояния существовал (в классическом смысле) член последовательности, после которого все члены оказываются ближе друг к другу, чем это расстояние. В конструктивной версии требуется, чтобы для любого заданного расстояния можно было фактически указать точку в последовательности, где это происходит (эта требуемая спецификация часто называется модулем сходимости ). Фактически, стандартная конструктивная интерпретация математического утверждения
как раз и есть существование функции, вычисляющей модуль сходимости. Таким образом, разницу между двумя определениями действительных чисел можно рассматривать как разницу в интерпретации утверждения "для всех... существует..."
Это затем открывает вопрос о том, какой вид функции из счетного множества в счетное множество, такое как f и g выше, может быть фактически построен. Различные версии конструктивизма расходятся в этом вопросе. Конструкции могут быть определены так широко, как последовательности свободного выбора , что является интуиционистским взглядом, или так узко, как алгоритмы (или более технически, вычислимые функции ), или даже оставлены неопределенными. Если, например, принять алгоритмический взгляд, то действительные числа, как построено здесь, по сути, являются тем, что классически называлось бы вычислимыми числами .
Принятие алгоритмической интерпретации выше, казалось бы, противоречит классическим представлениям о мощности . Перечисляя алгоритмы, мы можем показать, что вычислимые числа являются классически счетными. И все же диагональный аргумент Кантора здесь показывает, что действительные числа имеют несчетную мощность. Отождествление действительных чисел с вычислимыми числами тогда было бы противоречием. Более того, диагональный аргумент кажется совершенно конструктивным.
Действительно, диагональный аргумент Кантора может быть представлен конструктивно, в том смысле, что при заданной биекции между натуральными числами и действительными числами строится действительное число, не входящее в область значений функции, и тем самым устанавливается противоречие. Можно перечислить алгоритмы для построения функции T , о которой мы изначально предполагаем, что она является функцией от натуральных чисел к действительным числам. Но каждому алгоритму может соответствовать действительное число, а может и не соответствовать, поскольку алгоритм может не удовлетворять ограничениям или даже быть незавершающим ( T — частичная функция ), так что это не даст требуемой биекции. Короче говоря, тот, кто придерживается точки зрения, что действительные числа (по отдельности) эффективно вычислимы, интерпретирует результат Кантора как показывающий, что действительные числа (в совокупности) не являются рекурсивно перечислимыми .
Тем не менее, можно было бы ожидать, что поскольку T является частичной функцией от натуральных чисел к действительным числам, то действительные числа не более чем счетны. И поскольку каждое натуральное число может быть тривиально представлено как действительное число, то действительные числа не менее чем счетны. Поэтому они являются точно счетными. Однако это рассуждение не является конструктивным, поскольку оно все еще не строит требуемую биекцию. Классическая теорема, доказывающая существование биекции в таких обстоятельствах, а именно теорема Кантора–Бернштейна–Шредера , является неконструктивной. Недавно было показано, что теорема Кантора–Бернштейна–Шредера влечет закон исключенного третьего , поэтому не может быть конструктивного доказательства теоремы. [4]
Статус аксиомы выбора в конструктивной математике осложняется различными подходами различных конструктивистских программ. Одно тривиальное значение слова «конструктивный», неформально используемое математиками, — «доказуемый в теории множеств ZF без аксиомы выбора». Однако сторонники более ограниченных форм конструктивной математики утверждают, что сама ZF не является конструктивной системой.
В интуиционистских теориях теории типов (особенно в арифметике высших типов) допускаются многие формы аксиомы выбора. Например, аксиому AC 11 можно перефразировать так, что для любого отношения R на множестве действительных чисел, если вы доказали, что для каждого действительного числа x существует действительное число y такое, что R ( x , y ) выполняется, то на самом деле существует функция F такая, что R ( x , F ( x )) выполняется для всех действительных чисел. Аналогичные принципы выбора принимаются для всех конечных типов. Мотивацией принятия этих, казалось бы, неконструктивных принципов является интуиционистское понимание доказательства того, что «для каждого действительного числа x существует действительное число y такое, что R ( x , y ) выполняется». Согласно интерпретации BHK , это доказательство само по себе по сути является желаемой функцией F. Принципы выбора, которые принимают интуиционисты, не подразумевают закон исключенного третьего .
Однако в некоторых системах аксиом для конструктивной теории множеств аксиома выбора подразумевает закон исключенного третьего (при наличии других аксиом), как показано в теореме Диаконеску-Гудмана-Майхилла . Некоторые конструктивные теории множеств включают в себя более слабые формы аксиомы выбора, такие как аксиома зависимого выбора в теории множеств Майхилла.
Классическая теория меры принципиально неконструктивна, поскольку классическое определение меры Лебега не описывает никакого способа вычисления меры множества или интеграла функции. Фактически, если думать о функции просто как о правиле, которое «вводит действительное число и выводит действительное число», то не может быть никакого алгоритма для вычисления интеграла функции, поскольку любой алгоритм мог бы вызывать только конечное число значений функции за раз, а конечного числа значений недостаточно для вычисления интеграла с любой нетривиальной точностью. Решение этой головоломки, впервые реализованное в Bishop (1967), состоит в том, чтобы рассматривать только функции, которые записаны как поточечный предел непрерывных функций (с известным модулем непрерывности), с информацией о скорости сходимости. Преимущество конструктивизации теории меры заключается в том, что если можно доказать, что множество конструктивно имеет полную меру, то существует алгоритм для нахождения точки в этом множестве (снова см. Bishop (1967)).
Традиционно некоторые математики с подозрением, если не антагонистически, относились к математическому конструктивизму, в основном из-за ограничений, которые, по их мнению, он накладывал на конструктивный анализ. Эти взгляды были убедительно выражены Давидом Гильбертом в 1928 году, когда он написал в Grundlagen der Mathematik : «Отнять у математика принцип исключенного третьего было бы тем же самым, что, скажем, запретить астроному телескоп или боксёру использовать кулаки». [5]
Эрретт Бишоп в своей работе 1967 года «Основы конструктивного анализа » [2] стремился развеять эти страхи, развив значительную часть традиционного анализа в конструктивной форме.
Хотя большинство математиков не принимают тезис конструктивистов о том, что только математика, выполненная на основе конструктивных методов, является обоснованной, конструктивные методы вызывают все больший интерес по неидеологическим причинам. Например, конструктивные доказательства в анализе могут гарантировать извлечение свидетельств, таким образом, работа в рамках ограничений конструктивных методов может сделать поиск свидетельств теорий проще, чем при использовании классических методов. Приложения для конструктивной математики также были найдены в типизированных лямбда-исчислениях , теории топосов и категориальной логике , которые являются заметными предметами в фундаментальной математике и информатике . В алгебре для таких сущностей, как топосы и алгебры Хопфа , структура поддерживает внутренний язык , который является конструктивной теорией; работа в рамках ограничений этого языка часто более интуитивна и гибка, чем работа извне такими средствами, как рассуждения о множестве возможных конкретных алгебр и их гомоморфизмов .
Физик Ли Смолин пишет в своей книге «Три пути к квантовой гравитации» , что теория топоса — «правильная форма логики для космологии» (стр. 30) и «В своих первых формах она называлась «интуиционистской логикой»» (стр. 31). «В этом виде логики утверждения, которые наблюдатель может сделать о вселенной, делятся по крайней мере на три группы: те, которые мы можем оценить как истинные, те, которые мы можем оценить как ложные, и те, об истинности которых мы не можем судить в настоящее время» (стр. 28).
{{cite book}}: CS1 maint: бот: исходный статус URL неизвестен ( ссылка )