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