Конструктивизм в математике: подходы и принципы

Введение

Математическая точка зрения, согласно которой доказательства существования должны быть конструктивными.

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

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

Большая часть конструктивной математики использует интуиционистскую логику, которая по сути является классической логикой без закона исключённого третьего. Этот закон утверждает, что для любого высказывания верно либо само это высказывание, либо его отрицание. Это не означает, что закон исключённого третьего полностью отрицается; частные случаи этого закона могут быть доказаны. Просто общий закон не принимается как аксиома. Закон непротиворечия (утверждающий, что противоречивые утверждения не могут быть истинными одновременно) остаётся в силе. Например, в арифметике Гейтинга можно доказать, что для любого высказывания *p*, не содержащего кванторов, является теоремой (где *x*, *y*, *z* – свободные переменные в высказывании *p*). В этом смысле высказывания, ограниченные конечными множествами, по-прежнему считаются либо истинными, либо ложными, как и в классической математике, но эта бивалентность не распространяется на высказывания, относящиеся к бесконечным множествам. Фактически, Л. Е. Й. Брауэр, основатель интуиционистской школы, рассматривал закон исключённого третьего как абстрагированный из конечного опыта и затем необоснованно применённый к бесконечности. Например, гипотеза Гольдбаха утверждает, что каждое чётное число, большее 2, является суммой двух простых чисел. Можно проверить для любого конкретного чётного числа, является ли оно суммой двух простых чисел (например, полным перебором), поэтому каждое из них либо является суммой двух простых чисел, либо не является. И до сих пор каждое проверенное таким образом число действительно оказалось суммой двух простых чисел. Однако нет известных доказательств того, что все числа обладают этим свойством, и нет известных доказательств того, что не все числа обладают этим свойством; даже не известно, должно ли существовать доказательство или опровержение гипотезы Гольдбаха (гипотеза может быть неразрешимой в традиционной теории множеств ZF). Таким образом, по мнению Брауэра, мы не имеем права утверждать: «либо гипотеза Гольдбаха истинна, либо она ложна». И хотя однажды эта гипотеза может быть решена, этот аргумент применим к аналогичным нерешённым задачам. Для Брауэра закон исключённого третьего равносилен предположению, что у каждой математической задачи есть решение. С исключением закона исключённого третьего как аксиомы, оставшаяся логическая система обладает свойством существования, которого нет у классической логики: всякий раз, когда доказано конструктивно, то на самом деле доказано конструктивно для (по крайней мере) одного конкретного значения, часто называемого свидетелем. Таким образом, доказательство существования математического объекта связано с возможностью его построения.

Much constructive mathematics uses intuitionistic logic, which is essentially classical logic without the law of the excluded middle. This law states that, for any proposition, either that proposition is true or its negation is. This is not to say that the law of the excluded middle is denied entirely; special cases of the law will be provable. It is just that the general law is not assumed as an axiom. The law of non contradiction (which states that contradictory statements cannot both be true at the same time) is still valid. For instance, in Heyting arithmetic, one can prove that for any proposition p that does not contain quantifiers, is a theorem (where x, y, z are the free variables in the proposition p). In this sense, propositions restricted to the finite are still regarded as being either true or false, as they are in classical mathematics, but this bivalence does not extend to propositions that refer to infinite collections. In fact, L. E. J. Brouwer, founder of the intuitionist school, viewed the law of the excluded middle as abstracted from finite experience, and then applied to the infinite without justification. For instance, Goldbach's conjecture is the assertion that every even number greater than 2 is the sum of two prime numbers. It is possible to test for any particular even number whether it is the sum of two primes (for instance by exhaustive search), so any one of them is either the sum of two primes or it is not. And so far, every one thus tested has in fact been the sum of two primes. But there is no known proof that all of them are so, nor any known proof that not all of them are so; nor is it even known whether either a proof or a disproof of Goldbach's conjecture must exist (the conjecture may be undecidable in traditional ZF set theory). Thus to Brouwer, we are not justified in asserting "either Goldbach's conjecture is true, or it is not." And while the conjecture may one day be solved, the argument applies to similar unsolved problems. To Brouwer, the law of the excluded middle is tantamount to assuming that every mathematical problem has a solution. With the omission of the law of the excluded middle as an axiom, the remaining logical system has an existence property that classical logic does not have: whenever is proven constructively, then in fact is proven constructively for (at least) one particular , often called a witness. Thus the proof of the existence of a mathematical object is tied to the possibility of its construction.

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

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

To take the algorithmic interpretation above would seem at odds with classical notions of cardinality. By enumerating algorithms, we can show that the computable numbers are classically countable. And yet Cantor's diagonal argument here shows that real numbers have uncountable cardinality. To identify the real numbers with the computable numbers would then be a contradiction. Furthermore, the diagonal argument seems perfectly constructive. Indeed Cantor's diagonal argument can be presented constructively, in the sense that given a bijection between the natural numbers and real numbers, one constructs a real number not in the functions range, and thereby establishes a contradiction. One can enumerate algorithms to construct a function T, about which we initially assume that it is a function from the natural numbers onto the reals. But, to each algorithm, there may or may not correspond a real number, as the algorithm may fail to satisfy the constraints, or even be non terminating (T is a partial function), so this fails to produce the required bijection. In short, one who takes the view that real numbers are (individually) effectively computable interprets Cantor's result as showing that the real numbers (collectively) are not recursively enumerable. Still, one might expect that since T is a partial function from the natural numbers onto the real numbers, that therefore the real numbers are no more than countable. And, since every natural number can be trivially represented as a real number, therefore the real numbers are no less than countable. They are, therefore exactly countable. However this reasoning is not constructive, as it still does not construct the required bijection. The classical theorem proving the existence of a bijection in such circumstances, namely the Cantor–Bernstein–Schroeder theorem, is non constructive. It has recently been shown that the Cantor–Bernstein–Schroeder theorem implies the law of the excluded middle, hence there can be no constructive proof of the theorem.

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

Статус аксиомы выбора в конструктивной математике осложняется различными подходами различных конструктивистских программ. Одно из тривиальных значений термина "конструктивный", используемое математиками в неформальном контексте, означает "доказуемый в теории множеств ZF без аксиомы выбора". Однако сторонники более строгих форм конструктивной математики утверждают, что сама ZF не является конструктивной системой. В интуиционистских теориях теории типов (особенно в арифметике высших типов) допускается множество форм аксиомы выбора. Например, аксиому AC11 можно перефразировать следующим образом: для любого отношения R на множестве вещественных чисел, если доказано, что для каждого вещественного числа x существует вещественное число y, такое что R(x, y) истинно, то существует функция F, такая что R(x, F(x)) истинно для всех вещественных чисел. Аналогичные принципы выбора принимаются для всех конечных типов. Мотивацией для принятия этих, на первый взгляд, неконструктивных принципов является интуиционистское понимание доказательства утверждения "для каждого вещественного числа x существует вещественное число y, такое что R(x, y) истинно". Согласно интерпретации BHK, само это доказательство по сути и является искомой функцией F. Принципы выбора, принимаемые интуиционистами, не подразумевают закон исключённого третьего. Однако в некоторых аксиоматических системах конструктивной теории множеств аксиома выбора действительно подразумевает закон исключённого третьего (в присутствии других аксиом), что было показано теоремой Диаконеску — Гудмана — Майхилла. Некоторые конструктивные теории множеств включают более слабые формы аксиомы выбора, такие как аксиома зависимого выбора в теории множеств Майхилла.

Теория измерения

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

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

Традиционно некоторые математики относились к математическому конструктивизму с подозрением, если не с враждебностью, главным образом из-за ограничений, которые, по их мнению, он накладывает на конструктивный анализ. Эти взгляды были резко выражены Давидом Гильбертом в 1928 году, когда он писал в «Grundlagen der Mathematik»: «Лишение математика принципа исключённого среднего было бы тем же самым, что запретить астроному телескоп или боксёру – использовать кулаки». Эрретт Бишоп в своей работе 1967 года «Основы конструктивного анализа» стремился развеять эти опасения, развивая значительную часть традиционного анализа в конструктивном контексте. Несмотря на то, что большинство математиков не принимают конструктивистский тезис о том, что только математика, основанная на конструктивных методах, является надёжной, конструктивные методы вызывают всё больший интерес по неидеологическим причинам. Например, конструктивные доказательства в анализе могут обеспечивать извлечение свидетельств, и работа в рамках ограничений конструктивных методов может облегчить поиск свидетельств теорий по сравнению с использованием классических методов. Области применения конструктивной математики также были найдены в типизированных лямбда-исчислениях, теории топосов и категорной логике, которые являются важными областями фундаментальной математики и информатики. В алгебре, для таких объектов, как топосы и алгебры Хопфа, структура поддерживает внутренний язык, который является конструктивной теорией; работа в рамках ограничений этого языка часто более интуитивна и гибка, чем работа вне его, например, рассуждения о множестве возможных конкретных алгебр и их гомоморфизмов. Физик Ли Смолин в книге «Три пути к квантовой гравитации» пишет, что теория топосов является «правильной формой логики для космологии» (страница 30) и «В своих первых формах она называлась «интуиционистской логикой»» (страница 31). «В этом виде логики утверждения, которые наблюдатель может делать об Вселенной, делятся как минимум на три группы: те, которые мы можем считать истинными, те, которые мы можем считать ложными, и те, истинность которых мы не можем определить на данный момент» (страница 28).

Traditionally, some mathematicians have been suspicious, if not antagonistic, towards mathematical constructivism, largely because of limitations they believed it to pose for constructive analysis. These views were forcefully expressed by David Hilbert in 1928, when he wrote in Grundlagen der Mathematik, "Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists". Errett Bishop, in his 1967 work Foundations of Constructive Analysis, worked to dispel these fears by developing a great deal of traditional analysis in a constructive framework. Even though most mathematicians do not accept the constructivist's thesis that only mathematics done based on constructive methods is sound, constructive methods are increasingly of interest on non ideological grounds. For example, constructive proofs in analysis may ensure witness extraction, in such a way that working within the constraints of the constructive methods may make finding witnesses to theories easier than using classical methods. Applications for constructive mathematics have also been found in typed lambda calculi, topos theory and categorical logic, which are notable subjects in foundational mathematics and computer science. In algebra, for such entities as topoi and Hopf algebras, the structure supports an internal language that is a constructive theory; working within the constraints of that language is often more intuitive and flexible than working externally by such means as reasoning about the set of possible concrete algebras and their homomorphisms. Physicist Lee Smolin writes in Three Roads to Quantum Gravity that topos theory is "the right form of logic for cosmology" (page 30) and "In its first forms it was called 'intuitionistic logic'" (page 31). "In this kind of logic, the statements an observer can make about the universe are divided into at least three groups: those that we can judge to be true, those that we can judge to be false and those whose truth we cannot decide upon at the present time" (page 28).