Конструктивная логика, матанализ и проч. (продолжение)

[epros]

Someone писал(а):

Не говорите ерунду. Новая теория (в данном случае - теория множеств) является "основанием" классического математического анализа в том смысле, что...

Опять же, ерунда. Птолемеевская модель - это просто система координат, связанная с Землёй...

А зачем? Зачем уничтожать теорию, которая за века доказала свою полезность?

Из всего вышесказанного прокомментирую одно:

Someone писал(а):

Вообще, физика не отвергает теории, которые хорошо работают в своей области. Классическая механика не исчезла после появления СТО и квантовой механики.

Факт заключается в том, что понятие об "абсолютном времени" исчезло. Как и многие другие понятия до него.

В остальном речь идёт скорее о философии, чем о математике. И хотя у меня есть много что сказать по этим вопросам, но здесь я воздержусь от этого. Тем более, что я, как Вы полагаете:

Someone писал(а):

...производите впечатление фанатика, абсолютно невосприимчивого к доводам, не согласующимся с Вашими представлениями

а

Someone писал(а):

...спорить с фанатиком бессмысленно

Печально, конечно, поскольку "мои представления" о конструктивном анализе для меня отнюдь не являются предметом слепой фанатичной веры. Они почерпнуты из сопоставления двух точек зрения (классической и конструктивистской) и я искренне хотел бы найти кого-то, кто внятно объяснит мне (с классической точки зрения) почему мы должны некритично принимать такие вещи, как закон исключённого третьего (в широком смысле - утверждение о том, что всякое утверждение либо истинно, либо ложно и никак иначе), существование внетеоретической "истинности", которую невозможно объяснить доказуемостью в теории и которая вообще непонятно откуда взялась, неконструктивные аксиомы, которые приняты не потому, что формализуют свойства каких-либо объектов, а просто для получения "интересных" кому-то следствий. И.т.п. Увы, пока не нашёл. Как только возникают подобные вопросы, вместо внятных и точных объяснений я почему-то сталкиваюсь с фанатичной убеждённостью в том, что все эти вещи "обязательно нужны", "на них стоит всё математическое знание" и "отказ от них означает отказ от массы невероятно ценных результатов". И с какой стороны тут фанатизм?

Someone писал(а):

Также хотел бы обратить Ваше внимание на то, что Вы не можете запретить кому-либо изучать конструктивную логику и вообще конструктивные теории средствами классической математики, в частности, с применением классической логики.

И не собираюсь. Например, утверждение о существовании для интуиционистской логики бесконечного множества логических значений - это классическая теорема. Я её не пытаюсь "запретить", а наоборот - указываю на неё (хотя для конструктивизма она ничего не значит).

Someone писал(а):

Точно так же конструктивисты могут изучать своими средствами классическую логику и основанные на ней математические теории (но, кажется, конструктивистам пока не до этого).

На самом деле вполне "до этого". Любые неконструктивные теории могут анализироваться методами конструктивной логики, что конструктивисты частенько и делают.

Someone писал(а):

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

Разумеется свойства в конструктивном анализе есть. Например, есть такое свойство, как "является натуральным числом". И есть соответствующая процедура, которая реализует проверку предъявляемых ей объектов на наличие этого свойства. При желании, её можно даже расписать через соответствующие аксиомы Пеано. Конструктивисты не будут даже возражать, если Вы захотите записать соответствующий одноместный предикат как $\ldots \in \mathbb{N}$. Непонимание возникнет только тогда, когда Вы часть этой символической записи ($\mathbb{N}$) захотите использовать как отдельное понятие.

[Someone]

epros в сообщении #145302 писал(а):

Факт заключается в том, что понятие об "абсолютном времени" исчезло.

Куда? Классическая механика как была с абсолютным временем, так с ним и осталась. "Исчезли" некоторые ненужные сущности (теплород, светоносный эфир), но соответствующие физические теории (термодинамика, электродинамика) никуда не делись.

epros в сообщении #145302 писал(а):

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

Это и есть фанатизм. Вы приемлете только одну точку зрения, априорно считая другую совершенно вздорной.

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

Я вообще не пойму: Вы ищете эффективную теорию или "абсолютную истину"? Ведь все эти "обоснования", как в случае классического анализа, так и в случае конструктивного, лежат за пределами математики. Поэтому для самой математики они не имеют существенного значения.

epros в сообщении #145302 писал(а):

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

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

epros в сообщении #145302 писал(а):

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

И какие результаты?

Скорее это гильбертовский финитизм. Финитизм относится к конструктивному направлению математики, но он накладывает более жёсткие ограничения на используемые средства, чем любое другое из существующих конструктивных направлений. Впрочем, настаивать не буду. Вдруг то, что Вы встречали, и в самом деле не финитизм.

epros в сообщении #145302 писал(а):

Конструктивисты не будут даже возражать, если Вы захотите записать соответствующий одноместный предикат как $\ldots\in\mathbb N$. Непонимание возникнет только тогда, когда Вы часть этой символической записи ($N$) захотите использовать как отдельное понятие.

Это пустяки, это просто вопрос расширения языка. Причём, несущественного, которое не приводит ни к каким новым доказуемым утверждениям и, следовательно, вполне допустимо.

epros в сообщении #144736 писал(а):

Этот закон позволяет доказать известную теорему о том, что любое утверждение классической теории, будучи одето в двойное отрицание, становится конструктивно доказуемым.

Это можно рассматривать как модель классической теории внутри конструктивной. Своего рода доказательство непротиворечивости классической теории относительно конструктивной.

epros в сообщении #145038 писал(а):

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

Нет. Построение модели даёт доказательство относительной непротиворечивости. Если теория противоречива, то моделей у неё нет. Для построения моделей дествительно обычно используется теория множеств, поскольку эта теория очень хорошо приспособлена для этого.

epros в сообщении #144904 писал(а):

Последователи Брауэра развивали существовавший к этому времени матанализ

Они не развивали существовавший анализ. Они строили свой.

epros в сообщении #144904 писал(а):

Математика оперирует только со строками символов, значит в рамках математики представлением множества должна быть некая строка символов. Это значит, что Вы имеете право строить множество не только "по одному элементу", а например, по десять (если определите процедуру добавления 10-ти элементов). Или, если хотите, можете определить процедуру добавления по 10 элементов, через которую определите процедуру добавления по 10^10 элементов, через которую определите процедуру добавления по 10^10^10 элементов... Но в итоге должна получиться процедура с конечным описанием, имеющая точку останова, в которой она предъявит Вам в качестве результата искомое множество.

Всё равно я этого не понимаю. Что значит - "предъявить множество"? Для меня это означает предъявить свойство, выделяющее элементы множества среди всех возможных элементов. Классическая математика от всех проблем с проверкой этого свойства для конкретного элемента абстрагируется, считая, что "как-нибудь да проверим". В конструктивной, естественно, возникают проблемы, и появляются множества разрешимые, неразрешимые, перечислимые, неперечислимые и т.п. Это не мои термины, они употребляются в книге Кушнера.

epros в сообщении #144904 писал(а):

Я не знаю, откуда Вы взяли такую "конструктивную" интерпретацию понятия "ложно".

Е.Расёва, Р.Сикорский. Математическая логика и основания математики. Математика метаматематики. "Наука", Москва, 1972.

Глава IX, § 1 писал(а):

Утверждение $-\alpha$ считается истинным, если принятие предложения $\alpha$ ведёт нас к противоречию.

После некоторых размышлений, я пришёл к выводу, что это неправильно. Скорее всего, следствие некорректного перевода.

luitzen в сообщении #145216 писал(а):

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

Да. Доказывали существование и сокрушались: "Какая досада! Никакого конкретного объекта не получилось."

Философствования на этот счёт к математике не относятся.

luitzen в сообщении #145216 писал(а):

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

Да. Гильбертовская программа обоснования классической математики состояла в доказательстве её непротиворечивости финитными средствами, которые являются серьёзным ограничением даже по сравнению с теми, которые считают "несомненными" интуиционисты и конструктивисты. Деталей я не знаю, но так пишет, например, А.Трулстра (Справочная книга по математической логике. Часть IV. Теория доказательств и конструктивная математика. Москва, "Наука", 1983). К "сожалению", эта программа провалилась.

luitzen в сообщении #145216 писал(а):

Не очень понял Вас, Someone. Ведь вроде бы есть результат об отсутствии у интуиционистской пропозициональной логики точной конечной модели.

Да бог с ней, с точностью. Вопрос был о количестве логических значений. Ответ состоит в том, что для интуиционистского пропозиционального исчисления оно может быть любым, о чём Новиков и пишет.

luitzen в сообщении #145216 писал(а):

Иначе создаётся впечатление, что Вы сами пытаетесь натянуть на конструктивную логику эту самую двузначную оценочную функцию.

Натягивается же. Но вообще, то что я написал насчёт отрицания - это недоразумение.

epros в сообщении #144904 писал(а):

Someone писал(а):

Конструктивность, кстати сказать, понимается в весьма разных смыслах.

Только не самими конструктивистами! Конструктивисты понимают её в строгом формализуемом смысле.

А.Трулстра. Аспекты конструктивной математики. (В указанной выше "Справочной книге по математической логике".)
Перечисляются следующие направления конструктивизма, понимающие конструктивность по-своему:
(a) финитизм (Гильберт и др.);
(b) конструктивный рекурсивный анализ CRA (Шанин, Марков и др.);
(c) интуиционизм (Брауэр, Гейтинг, Трулстра и др.);
(d) конструктивизм в узком смысле, под которым понимается интуиционизм без свободно становящихся последовательностей и без тезиса Чёрча (Бишоп и др.).
Впрочем, тезис Чёрча принят только в CRA. Интуиционизм не считает, что эффективная вычислимость сводится к механической вычислимости.
Понятие конструктивности в достаточно разных смыслах используется и в классической математике: предикативизм (Вейль), классический рекурсивный анализ RA; даже в (мета)теории множеств есть понятие конструктивного множества, но это от обсуждаемого конструктивизма находится бесконечно далеко.

[epros]

Someone писал(а):

epros в сообщении #145302 писал(а):

Факт заключается в том, что понятие об "абсолютном времени" исчезло.

Куда? Классическая механика как была с абсолютным временем, так с ним и осталась. "Исчезли" некоторые ненужные сущности (теплород, светоносный эфир), но соответствующие физические теории (термодинамика, электродинамика) никуда не делись.

Вот смотрите, Вы тоже соглашаетесь с тем, что "некоторые сущности" исчезли. Я об этом и говорю.

Someone писал(а):

epros в сообщении #145302 писал(а):

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

Это и есть фанатизм. Вы приемлете только одну точку зрения, априорно считая другую совершенно вздорной.

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

Someone писал(а):

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

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

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

Someone писал(а):

Вы мне поверите? Вы ведь опять будете твердить, что неконструктивные методы абсолютно неприемлемы (а если и не скажете вслух, то "про себя" подумаете).

Нет, я не скажу, что "неконструктивные методы абсолютно неприемлемы". Но я надеюсь, что безусловная вера - это всё-таки не то, чего Вы от меня на самом деле ожидаете. Моё отношение к "неконструктивным методам" примерно такое: "Пустая трата времени, если не согласны - продемонстрируйте обратное (хотя бы на одном примере)".

Someone писал(а):

Я вообще не пойму: Вы ищете эффективную теорию или "абсолютную истину"? Ведь все эти "обоснования", как в случае классического анализа, так и в случае конструктивного, лежат за пределами математики. Поэтому для самой математики они не имеют существенного значения.

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

Someone писал(а):

epros в сообщении #145302 писал(а):

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

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

Вот, - всё дело в том, что точная модель не является конечной. (Попробую как-нибудь на досуге поискать в литературе что-нибудь про "модели Крипке").

Someone писал(а):

luitzen в сообщении #145216 писал(а):

Не очень понял Вас, Someone. Ведь вроде бы есть результат об отсутствии у интуиционистской пропозициональной логики точной конечной модели.

Да бог с ней, с точностью. Вопрос был о количестве логических значений. Ответ состоит в том, что для интуиционистского пропозиционального исчисления оно может быть любым, о чём Новиков и пишет.

А зачем нам "неточные" модели?

Someone писал(а):

epros в сообщении #145302 писал(а):

Конструктивисты не будут даже возражать, если Вы захотите записать соответствующий одноместный предикат как $\ldots\in\mathbb N$. Непонимание возникнет только тогда, когда Вы часть этой символической записи ($N$) захотите использовать как отдельное понятие.

Это пустяки, это просто вопрос расширения языка. Причём, несущественного, которое не приводит ни к каким новым доказуемым утверждениям и, следовательно, вполне допустимо.

Не думаю, что когда из семантически целостной конструкции $\ldots\in\mathbb N$ выщепляется $\mathbb N$ и начинает использоваться в качестве самостоятельного понятия, имеющего право участвовать не только в указанном отношении, то это "несущественное" расширение языка. По-моему, очень даже существенное.

Someone писал(а):

epros в сообщении #144736 писал(а):

Этот закон позволяет доказать известную теорему о том, что любое утверждение классической теории, будучи одето в двойное отрицание, становится конструктивно доказуемым.

Это можно рассматривать как модель классической теории внутри конструктивной. Своего рода доказательство непротиворечивости классической теории относительно конструктивной.

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

Someone писал(а):

epros в сообщении #145038 писал(а):

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

Нет. Построение модели даёт доказательство относительной непротиворечивости. Если теория противоречива, то моделей у неё нет. Для построения моделей дествительно обычно используется теория множеств, поскольку эта теория очень хорошо приспособлена для этого.

Вы просто слегка формализовали то, что я сказал. "Непротиворечивая теория" - "теория, которая хоть что-то описывает" (с точки зрения теории множеств).

Someone писал(а):

epros в сообщении #144904 писал(а):

Последователи Брауэра развивали существовавший к этому времени матанализ

Они не развивали существовавший анализ. Они строили свой.

Зря Вы так категорично. Все понятия - числа (натурального, рационального, действительного и т.д.), функции, и т.п. - были взяты конструктивной математикой из традиционных представлений. Просто их определения были перепроверены на предмет конструктивности. Да, кое-что проверку не прошло. Но это не значит, что конструктивный анализ стал с нуля изобретать собственные понятия. Очевидно, что рассматриваются в первую очередь те понятия, которые нужны прикладным наукам.

Someone писал(а):

epros в сообщении #144904 писал(а):

Математика оперирует только со строками символов, значит в рамках математики представлением множества должна быть некая строка символов. Это значит, что Вы имеете право строить множество не только "по одному элементу", а например, по десять (если определите процедуру добавления 10-ти элементов). Или, если хотите, можете определить процедуру добавления по 10 элементов, через которую определите процедуру добавления по 10^10 элементов, через которую определите процедуру добавления по 10^10^10 элементов... Но в итоге должна получиться процедура с конечным описанием, имеющая точку останова, в которой она предъявит Вам в качестве результата искомое множество.

Всё равно я этого не понимаю. Что значит - "предъявить множество"?

Математический объект - это строка символов. Предъявить его - это значит предъявить строку. Если не можете сделать это буквально - на листке бумаги (бумаги или чернил не хватает) - продемонстрируйте способ (процедуру) построения этой строки, который завершился бы успехом, если бы не ограничения в бумаге и чернилах.

Someone писал(а):

Для меня это означает предъявить свойство, выделяющее элементы множества среди всех возможных элементов.

Предполагаю у Вас здесь неточность: Множество ординалов не строится, хотя свойство, выделяющее элемент из всех возможных, имеется.

Someone писал(а):

Классическая математика от всех проблем с проверкой этого свойства для конкретного элемента абстрагируется, считая, что "как-нибудь да проверим".

В конструктивной математике всё наоборот: Сначала давайте проверим, а потом уже будем говорить, что оно существует. Предположить, что "когда-нибудь проверится", конечно, можно, но утверждать при этом ничего нельзя.

Someone писал(а):

В конструктивной, естественно, возникают проблемы, и появляются множества разрешимые, неразрешимые, перечислимые, неперечислимые и т.п. Это не мои термины, они употребляются в книге Кушнера.

Конструктивизм на самом деле способен говорить о многих неконструктивных объектах. Наример, функция Дирихле. Или ещё проще: функция sign(x), заданная на действительных аргументах. Казалось бы, в силу известной теоремы о том, что всякая конструктивная функция действительного аргумента непрерывна в области своего определения, эти функции не имеют "права на существование". Но это не значит, что их определения невозможно сформулировать! Предикаты "является рациональным числом", "больше нуля" и "меньше нуля" определимы. А это означает, что чисто формально мы можем определить указанные функции, вплоть до того, что можем написать процедуру вычисления их значения. Однако мы всё равно не можем конструктивно утверждать их существование по одной "незначительной" причине: при некоторых обстоятельствах эти процедуры не будут иметь точки останова. (Классическая математика от этой трудности, конечно же, "абстрагируется"). Так что вот: налицо объекты, формальное (но не конструктивное) определение которых мы в состоянии записать, и о которых мы в состоянии судить в том плане, что "их нельзя считать конструктивными".

Someone писал(а):

epros в сообщении #144904 писал(а):

Someone писал(а):

Конструктивность, кстати сказать, понимается в весьма разных смыслах.

Только не самими конструктивистами! Конструктивисты понимают её в строгом формализуемом смысле.

А.Трулстра. Аспекты конструктивной математики. (В указанной выше "Справочной книге по математической логике".)
Перечисляются следующие направления конструктивизма, понимающие конструктивность по-своему:
(a) финитизм (Гильберт и др.);
(b) конструктивный рекурсивный анализ CRA (Шанин, Марков и др.);
(c) интуиционизм (Брауэр, Гейтинг, Трулстра и др.);
(d) конструктивизм в узком смысле, под которым понимается интуиционизм без свободно становящихся последовательностей и без тезиса Чёрча (Бишоп и др.).
Впрочем, тезис Чёрча принят только в CRA. Интуиционизм не считает, что эффективная вычислимость сводится к механической вычислимости.
Понятие конструктивности в достаточно разных смыслах используется и в классической математике: предикативизм (Вейль), классический рекурсивный анализ RA; даже в (мета)теории множеств есть понятие конструктивного множества, но это от обсуждаемого конструктивизма находится бесконечно далеко.

Я следую линии Маркова (b). Интуиционизм, например, совершенно конструктивизмом не является, хотя он по отношению к нему "прародитель". Но "интуитивные" понятия вроде "свободно становящейся последовательности" для конструктивизма неприемлемы, ибо неформализуемы. Интуиционисты утверждают, что о существовании объекта можно говорить только когда указан способ его построения, но когда дело доходит до ССП, почему-то об этом забывают и на первый план выходит пресловутая "математическая интуиция". Конструктивный подход другой: сказав "способ", мы должны формализовать это понятие. Отсюда, например, появляется "нормальный алгорифм" Маркова или эквивалентная ему "рекурсивная функция".

Поэтому когда я говорю о том, что конструктивисты понимают конструктивность в строго формализуемом смысле, я имею в виду формализацию до конкретных алгоритмов - по Маркову или типа того.