"Как только" - это когда именно?
Знаете, как с договорами. "Договор вступает в силу сразу после подписания." Тоже будете спрашивать: "Сразу - это когда именно?"
А я вот предложу такой вариант ответа на свой вопрос: "Никогда без особой на то необходимости".
Это значит, что если особой необходимости нет, то пусть читатель сам когда угодно выберет (если захочет), какую модель действительных чисел использовать. А "особая необходимость", это, например, когда я хочу что-то сказать именно про Дедекиндовы сечения.
Устроит?
Но как только(с) присвоите название новому множеству, потеряете пласт теорем, которые были справедливы до этого присвоения.
Это как?
Мне всё же кажется полезным иметь возможность отличать изоморфные структуры от совпадающих.
Конечно же их нужно отличать всегда. Потому что если мы скажем, что
изоморфно
и
изоморфно
, то это не означает, что
совпадает с
. А если мы скажем, что
совпадает с
и
совпадает
, то получим совершенно иную ситуацию:
и
совпадают.
Но если закапываться до уровня теории множеств, то нужно всё же проверять, является ли
вещественным числом или нет.
- объект самой теории множеств, в ней есть утверждение о его существовании, а этот символ - константа, присвоенная этому существующему объекту в качестве названия. Строго говоря, конечно, мы должны консервативно расширить теорию множеств, добавив в сигнатуру этот символ, а в аксиоматику - аксиому, утверждающую, что
равен тому множеству, у которого нет элементов. Но этот шаг можно считать автоматически подразумеваемым.
- другое дело. Прежде, чем что-то сказать об этом объекте, его нужно как-то определить. Если определением будут добавленные аксиом непрерывного упорядоченного поля (для данного
), то вывести отсюда
(или
), как я понимаю, не получится. Но если определить его как булеан минимального бесконечного множества, с добавлением соответствующих аксиом упорядоченного поля, то
будет следовать из определения. Потому что фактически последнее определение - это готовая модель для
, построенная в рамках той же теории множеств.