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

[danielZU]

Здравствуйте! Сажусь за чтение конструктивного математического анализа Кушнера (1973). Для меня эта область новая.

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

Спасибо!

[george66]

Как выразился Николай Макарович Нагорный "Зачем пинать мёртвого осла" (передаю со слов Ю.Ш.Гуревича, который его как раз об этом спрашивал) Советская школа конструктивизма умерла. Конструктивная математика сейчас -- это интуиционистская теория типов. Соответственно, почитайте Гейтинга "Интуиционизм"
Гейтинг
почитайте Драгалина "Математический интуиционизм"
Драгалин
и попробуйте вот это
Введение в теорию типов, по-английски
А.А.Марков младший, кстати, начинал как геофизик, занимался магнитной разведкой руды. Затем увлёкся математикой, доказал интересные теоремы о свободных топологических группах. Затем увлёкся основаниями математики, создал школу советского конструктивизма и возглавил кафедру математической логики МГУ. И вот он стремился приблизить математику к наблюдаемой реальности. И, как видно теперь, перегнул. Брауэр гораздо современнее, многие его идеи прямо вошли в эту самую интуиционистскую теорию типов.

[danielZU]

george66, cпасибо за ответ. Обязательно все посмотрю.
Я правильно Вас понял, что математический интуиционизм, это продолжение конструктивизма, а математиков-конструктивистов сейчас нет? Почему, кстати? Эта область оказалась неактуальной, непринятой?
И еще вопрос: нужно ли, прежде чем взяться за перечисленных Вами авторов, почитать о конструктивизме? Вообще ценность у конструктивизма есть для современной математики? Извините за обилие вопросов.

[george66]

Интуиционизм возник раньше (в трудах Брауэра и Гейтинга). "Конструктивизмом" называют именно более позднюю советскую школу, которая подчёркивала свою близость к физической реальности в отличии от идеализма (это было ругательное слово) Брауэра. Тем не менее, подход Брауэра оказался математически гораздо интереснее. Самое неожиданное вот что: и Брауэр, и Марков отвергали теорию множеств (Марков на слово "множество" говорил "не понимаю"), тем не менее оказалось, что множества и интуиционистская логика прекрасно работают вместе (тут ключевое слово "топос", читайте мой учебник по теории категорий, который в соседней теме лежит). Топосы -- это, грубо говоря, модели теории множеств с интуиционистской логикой. Математики их охотно изучают. Что касается практических приложений, то была надежда применить всё это к программированию. Надежда в целом не оправдалась, но типы в языки программирования ввели. Если знакомы с Haskell, поставьте себе программу Agda (если нет, сначала почитайте статью по третьей ссылке).

[Mikhail_K]

(Оффтоп)

Как странно.
Читал я Гейтинга несколько лет назад, мне он показался откровенной лженаукой и ничем иным.
А конструктивизм показался значительно серьёзнее.
Не помню уже сейчас почему, но впечатление было отчётливое.

[george66]

Mikhail_K в сообщении #1221934 писал(а):

(Оффтоп)

Как странно.
Читал я Гейтинга несколько лет назад, мне он показался откровенной лженаукой и ничем иным.
А конструктивизм показался значительно серьёзнее.
Не помню уже сейчас почему, но впечатление было отчётливое.

Вот посмотрите, как сейчас излагают теорию алгоритмов
http://math.andrej.com/data/synthetic.pdf
Максимально абстрактно, по образцу теории множеств. Никакого конкретного определения алгоритма в этой работе вообще нет.

[danielZU]

george66, спасибо за прояснения. Раньше думал, что теория категорий - это что-то из области алгебры, а оказывается и для логиков полезная штука. Или это "другая" теория категорий?
Mikhail_K
А можете, пожалуйста, напрячься вспомнить, что конкретно Вам там показалось лженаукой? А конструктивизм показался еще более лженаучным? Для меня важно услышать разные мнения, а то не особо хочется тратить время на лженауку (если она действительно такой является).

[arseniiv]

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

[Mikhail_K]

(Оффтоп)

danielZU в сообщении #1222012 писал(а):

Mikhail_K
А можете, пожалуйста, напрячься вспомнить, что конкретно Вам там показалось лженаукой? А конструктивизм показался еще более лженаучным? Для меня важно услышать разные мнения, а то не особо хочется тратить время на лженауку (если она действительно такой является).

Ну, прочитайте "Интуиционизм" Гейтинга и составите впечатление о нём сами.
Книжка не такая уж большая и её можно прочитать быстро.
Мне показалось, что конструктивизм гораздо в большей степени удовлетворяет принятым в математике критериям строгости, чем интуиционизм.
Но я не буду делать здесь категоричных заявлений. Может оказаться, что я не прав.

[Someone]

danielZU в сообщении #1222012 писал(а):

А можете, пожалуйста, напрячься вспомнить, что конкретно Вам там показалось лженаукой? А конструктивизм показался еще более лженаучным? Для меня важно услышать разные мнения, а то не особо хочется тратить время на лженауку (если она действительно такой является).

Конструктивное направление в математике — это не лженаука.

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

Могу порекомендовать обзорную статью: А. Трулстра. Аспекты конструктивной математики. В сборнике "Справочная книга по математической логике. Часть IV. Теория доказательств и конструктивная математика." Москва, "Наука", 1983.

[george66]

Да, вижу книжку Мартин-Лёфа "Очерки конструктивной математики". Так что некоторые западные логики тоже употребляли слово "конструктивный". Мартин-Лёф, кстати учился в аспирантуре в МГУ у Колмогорова.

[pi991]

Приводит ли конструктивизм к новым результатам в каких-то областях математики? Или это скорее философское направление не влияющее на конкретные результаты.

Напоминает другую концепцию: предикативизм в логике. Тоже скорее философское отношение чем что-либо конкретное.

[Someone]

pi991 в сообщении #1227975 писал(а):

Приводит ли конструктивизм к новым результатам в каких-то областях математики? Или это скорее философское направление не влияющее на конкретные результаты.

В "каких-то областях" — нет. В самом начале действительно были какие-то философские концепции, но потом это превратилось в ряд новых направлений в математике. Естественно, со своими результатами.
Для примера можете почитать книгу
Б. А. Кушнер. Лекции по конструктивному математическому анализу. "Наука", Москва, 1973.
В предыдущих сообщениях также рекомендуется некоторая литература.

[george66]

Если именно к другим областям математики, то интуиционистская логика естественно возникает при изучении пучков (пучки это как бы "множества с неклассической логикой"). Если инженерные приложения, то написано множество программ-пруфчекеров и некоторые даже опробованы в деле. Классический пример - фирма Nicta, которая писала кусочек операционной системы (микроядро), используя предусловия и постусловия (в программе на C там и тут вставляются логические утверждения, которые должны быть выполнены в данной точке программы, если она правильно работает), затем доказывала пруфчекером, что всё работает как надо. На 7500 строк проверенного кода им пришлось написать 200 тысяч строк доказательств (общий объём писанины вырос в 28 раз), пруфчекер нашёл 144 ошибки. Вряд ли все смогут так писать, так что перспективы неясны.

[epros]

george66 в сообщении #1221915 писал(а):

Тем не менее, подход Брауэра оказался математически гораздо интереснее.

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