В качестве примера конструктивизма можно рассмотреть советскую школу конструктивизма — конструктивный рекурсивный анализ (надо сказать, что рекурсивный анализ, то есть, теория алгоритмически вычислимых функций, существует и в неконструктивном варианте). Конструктивное действительное число (КДЧ) — это либо рациональное число, либо пара алгоритмов, из которых первый определяет фундаментальную последовательность рациональных чисел
,
, а второй по заданному натуральному
определяет такой номер
, что для всех
, удовлетворяющих условиям
и
, выполняется неравенство
. Далее речь идёт только о таких вычислимых числах. Что там у интуиционистов, я не в курсе, но они не считают, что вычислимость сводится к алгоритмической вычислимости.
Подробности можно посмотреть в книге
Б. А. Кушнер. Лекции по конструктивному математическому анализу. "Наука", Москва, 1973.
То, что при этом найдутся всякие "по обычному" счетные множества, но про которые мы не можем (или нам сильно затруднительно) доказать их "конструктивную счетность", я не сомневаюсь.
Хуже: множество конструктивных действительных чисел эффективно несчётно: существует алгоритм, который каждую конструктивную последовательность КДЧ перерабатывает в КДЧ, не принадлежащее этой последовательности. Доказательство этого повторяет одно из доказательств Кантора теоремы о несчётности
(диагональный метод не используется), естественно, с конструктивистскими заморочками. В книге Кушнера это доказывается в § 4 главы 3.
Я и аксиому выбора люблю
Я тоже не понимаю, чего к ней прицепились. По-моему, большинство математиков, не вникающих в теорию множеств, этой аксиомой пользуются, даже не подозревая об этом. А без неё происходят ещё более крутые "чудеса", чем с ней. Например, без аксиомы выбора может оказаться, что в отображении
не выполняется неравенство
. И в конструктивной математике аксиома выбора также может выполняться: если у нас конструктивно определено семейство конструктивных множеств, непустых в конструктивном смысле (это означает, что в каждом множестве из этого семейства можно конструктивно указать некоторый элемент), то почему бы не существовать конструктивно определённой функции выбора? Об этом можно прочесть, например, в главе 5 книги
Справочная книга по математической логике. Часть IV. Теория доказательств и конструктивная математика. Москва, "Наука", 1983.
Но у меня есть смутное подозрение, что у них проблемы не с конструктивизмом, а прямо непосредственно с логикой.
Ага. Особенно умиляет частое использование двойных отрицаний (типа "не может не существовать"). Некоторых математиков перепугало обнаружение противоречий в системе Фреге, возникающих из-за того, что он постулировал, что каждому свойству соответствует множество всех объектов, обладающих этим свойством.
Но, с моей точки зрения, разработка всевозможных конструктивистских направлений в математике была полезной для развития математической логики и математики. Однако замена классической математики одним из конструктивных вариантов — шаг чересчур радикальный и не оправданный с практической точки зрения. В тех случаях, когда действительно требуется конструктивность, классическая математика, как правило, оказывается достаточно конструктивной.