О плодотворности интуиционистского подхода в математике.

[melnikoff]

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

[mihailm]

melnikoff в сообщении #821621 писал(а):

Регулярно слышу про интуиционистскую математику...

А вы не слушайте, а почитайте, что вы прочитали прежде чем этот вопрос задать?

[Aritaborian]

melnikoff в сообщении #821621 писал(а):

Регулярно слышу

А я регулярно слышу шансон в маршрутках.

[Joker_vD]

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

Сама интуиционистская логика оказалась изоморфной т.н. "простой системе типов" для лямбда-исчисления (simply-typed lambda calculus), что опять же как-то там подстегнуло развитие автоматических систем доказательства — особенно AUTOMATH.

[Xaositect]

Полуавтоматические пруверы типа Coq ее используют.

[Joker_vD]

Да классический вариант (с исключенным третьим) логики вообще не очень понятно, как закодировать. Хотя вот есть целые диссертации типа Chetan R. Murthy, "Extracting Constructive Content from Classical Proofs". В этой, например, показывается, как классические доказательства формул из класса $\Pi_{2}^{0}$ можно превратить в конструктивные, используя алгоритм, который, в сущности, не что иное, как преобразование в continuation-passing style.

[Yuri Gendelman]

Joker_vD в сообщении #821649 писал(а):

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

Е.Расёва, Р.Сикорский. Математика метаматематики. 1972

[epros]

Joker_vD в сообщении #821649 писал(а):

Если я не ошибаюсь, то не особо.

А по-моему, сама постановка вопроса о какой-то там "плодотворности" оснований математики не вполне корректна. Любая "плодотворность" которую мы сейчас тут наизмеряем, будет определяться скорее всего только количеством вовлечённых в тему математиков, чему мы скорее всего обязаны традиции, и ничему более. В конце концов, традиционная двузначная логика "более удобна" уже хотя бы в силу привычки и массового нежелания народа переучиваться. Примерно как десятичная система счисления: Известно, что 12-ричная система объективно лучше уже тем, что имеет относительно больше делителей, так что больший процент операций деления имеют простые и красивые результаты. А количество пальцев на руках, понятное дело, в современном мире вряд ли как-либо влияет на удобство расчётов. Тем не менее, никто не собирается переходить на 12-ричную систему.

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