К вопросу о равенстве чисел в конструктивном анализе

[epros]

Xaositect в сообщении #405580 писал(а):

Что происходит с конструктивным анализом, если разрешить использовать оракул, говорящий, равны два числа или нет, или добавить аксиому $\forall x y (x = y \vee \neg x = y)$ (и одно ли это и то же)? Понятно, что появляются разрывные функции и вроде бы теорема о промежуточном значении. Насколько все хорошо становится?

Выскажу своё мнение:

По первой части вопроса: Использовать оракул или добавить аксиому - это не одно и то же. Оракул сразу ответит на некоторые нерешённые вопросы чистого существования, например, существует ли нечётное совершенное число, есть ли двадцать троек подряд в десятичной записи числа $\pi$ и т.п. А с помощью данной аксиомы мы сможем получить на такие вопросы только обычный невразумительный ответ, что это "либо верно, либо нет". Но такой же ответ классическая математика получает и с использованием закона исключённого третьего.

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

[Xaositect]

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

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

Это-то я понимаю, но где все закончится? Теорему о промежуточном значении можно будет доказать? А существование неборелевских множеств?

-- Пт янв 28, 2011 15:17:22 --

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

Но такой же ответ классическая математика получает и с использованием закона исключённого третьего.

Я хочу узнать, есть ли где-нибудь исследования анализа с не совсем убранным, а ограниченным законом исключенного третьего?

[epros]

Xaositect в сообщении #405847 писал(а):

Теорему о промежуточном значении можно будет доказать? А существование неборелевских множеств?

Сильно не уверен. Подозреваю, что тут меньше, чем аксиомой выбора, не обойтись.

Xaositect в сообщении #405847 писал(а):

Я хочу узнать, есть ли где-нибудь исследования анализа с не совсем убранным, а ограниченным законом исключенного третьего?

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

[Someone]

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

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

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

Есть ещё принцип Маркова...

[epros]

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

Есть ещё принцип Маркова...

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

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

(Гейтинг определяет отделимость действительных чисел $a \# b$, как существование положительного рационального числа, меньшего модуля их разности. Равенство действительных чисел определяется через отрицание: как их НЕотделимость, т.е. $a=b \leftrightarrow \neg a \# b$. Неравенство действительных чисел определяется ещё раз через отрицание: $a \ne b \leftrightarrow \neg a=b$. Получается двойное отрицание: $a \ne b \leftrightarrow \neg \neg a \# b$, которое, как известно, в конструктивной логике слабее утверждения, т.е. в общем случае неравенство не влечёт отделимость.)

Но с моей точки зрения эквивалентность этих двух типов неравенства отнюдь не очевидна.

Да и вообще, если я правильно понимаю, можно привести пример арифметической формулы $\varphi(n)$, такой, что в определённом расширении арифметики Гейтинга можно будет с помощью принципа Маркова доказать $\exists n ~ \varphi(n)$, однако это доказательство будет совершенно контринтуитивным.