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

[Mikhail_K]

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

Mikhail_K - к вопросу о лженаучности, уж не Гейтинговские ли "свободно становящиеся последовательности" Вы вспомнили?

Да-да, именно их я и вспомнил.

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

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

У меня сложилось такое же впечатление.

[george66]

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

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

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

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

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

-- 23.06.2017, 22:09 --

Что касается свободно становящихся последовательностей, то сейчас это называют "коиндуктивные типы данных".

[epros]

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

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

А чем не устраивают фундаментальные последовательности рациональных чисел?

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

Что касается свободно становящихся последовательностей, то сейчас это называют "коиндуктивные типы данных".

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

[george66]

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

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

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

А чем не устраивают фундаментальные последовательности рациональных чисел?

Классически мы определяем действительные числа как полное упорядоченное поле. Затем доказываем существование такого поля одним из нескольких равносильных методов: дедекиндовы сечения, фундаментальные последовательности, бесконечные десятичные дроби и т.п. Если логика интуиционистская, эти методы не равносильны и обычно не дают полное упорядоченное поле (фундаментальные последовательности не дают -- представьте, что существуют только вычислимые последовательности и поймёте, почему). Кроме того, даже если есть полное упорядоченное поле, мы не всё можем доказать, если логика интуиционистская. Например, плотность рациональных чисел среди действительных хочется выразить так
$\forall x,y\in R(x<y\Rightarrow\exists r\in Q(x\leqslant r\leqslant y))$
и это не доказать интуиционистски, если я ничего не путаю (потому что торчит сильный квантор существования). Тут могу и напутать, давно не занимался. Брауэр предлагал вместо действительных чисел работать с открытыми интервалами с рациональными концами, они порождают полную решётку всех открытых подмножеств (каждое открытое подмножество есть объединение интервалов с рациональными концами). Непрерывная функция определяется заданием прообраза каждого интервала. При сильном желании попробуйте почитать вот это
http://gen.lib.rus.ec/search.php?req=st ... column=def

-- 24.06.2017, 00:22 --

И ещё на русском языке есть книга Мартин-Лёф "Очерки конструктивной математики", там именно Брауэровский подход, несмотря на слово "конструктивный"

[epros]

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

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

Разумеется вычислимые последовательности. И разумеется КДЧ (конструктивные действительные числа, определённые таким образом) не дают полного упорядоченного поля. Хотя бы потому, что отсутствует упорядоченность. И причина здесь отнюдь не в логике, а в том, что есть примеры чисел, алгоритмическая различимость которых под вопросом. Конструктивизм как раз подстраивает логику под эту ситуацию (если нечто не удаётся алгоритмически различить, значит мы не вправе утверждать, что они различны) вместо декларации того, что реальные числа составляют полное упорядоченное поле ("а если Вы этого не видите, то это Ваши проблемы"). Марков об этом писал примерно в этом ключе.

[george66]

Тут, философски мысля, можно предложить два способа оценки:
1) Что плодотворнее?
2) Что является правдой и отражает реальность?
И вот по поводу 2) надо быть осторожнее. Никто не поручится, что реальный натуральный ряд хотя бы бесконечный. А может, он бесконечный, но не фундированный и прав проклятый Есенин-Вольпин! Однажды, будучи студентом, я спросил профессора В.А.Успенского, существуют ли в природе невычислимые функции, на что Успенский сказал "Всё, что я вижу, вообще конечное".
А по поводу 1) сомнений нет, топологический подход Брауэра гораздо больше породил в современном интуиционизме-конструктивизме, чем Марковский. Брауэр -- это не только философия, но и много удачных технических идей.

[Someone]

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

Никто не поручится, что реальный натуральный ряд хотя бы бесконечный. А может, он бесконечный, но не фундированный

Что такое "реальный натуральный ряд"?

[george66]

Someone в сообщении #1229101 писал(а):

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

Никто не поручится, что реальный натуральный ряд хотя бы бесконечный. А может, он бесконечный, но не фундированный

Что такое "реальный натуральный ряд"?

Ряд километров, уходящий в космос.

[Someone]

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

Ряд километров, уходящий в космос.

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

[george66]

Вот, Вы Брауэр.
Реальность есть, но современная математика её не изучает (Евклид изучал). Современная математика -- наука инженерная, она создаёт полезные инструменты. Хорошо бы, например, иметь такие числа, которые не надо постоянно расширять. А пусть у нас будет полное упорядоченное поле! Притом, никто не видел в природе такого поля (аксиома полноты никаким опытом не проверяется) и непротиворечивость этих аксиом тоже никак не доказана.

[Someone]

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

Реальность есть, но современная математика её не изучает (Евклид изучал).

Ну да, ещё во времена Н. И. Лобачевского геометрию считали скорее частью физики, чем частью математики. За что Лобачевский и огрёб по полной программе. А Гаусс даже заикнуться побоялся о своих исследованиях.

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

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

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

[george66]

А вот свежая статья Андрея Бауэра о принципах конструктивной математики