Как я понял, ненужность аксиомы выбора
аргументируется тем, что можно написать некую (мета)формулу, определяющую
. Однако, если нумерация не задана конструктивно, такую формулу мы вряд ли напишем.
Мне по-прежнему кажется, что для доказательства существования максимального расширения такая формула не требуется. Достаточно существования биекции
, из которого все дальше и выводится. При этом, пожалуй, единственным неочевидным моментом является существование рекурсивно определяемой последовательности
. Ее существование следует из принципа рекурсии, который, в свою очередь, опирается на аксиому подстановки. Множества
определяются посредством
, но, к счастью, аксиома подстановки допускает использование формул «с параметрами» (т.е. с дополнительными свободными переменными). Вот наше
и используется в качестве параметра.
Я хочу подчеркнуть следующее: для рекурсивного определения функции (в нашем случае — последовательности) не обязательно задавать рекурсивное правило формулой без параметров. Наличие параметров лишает определяемую функцию «конструктивности» (определимости без параметров), но не лишает ее существования (коль скоро параметры с нужными свойствами существуют).
P.S. Извините за сумбур. Просто нет времени все четко расписать через аксиомы.