数理論理学的にはちょっと違うけどね。
たとえば選択公理を認めても選択函数はdefinableなもの
(上で言うところの「具体的」な函数)になるとは
限らないけど、ブルバキのτ(ι記号とも言う)を使。うなら
必ず論理式で具体的に書けるような関数になる

集合論は「明らか」だと思われるようなことに
実は数学的・論理学的にすごく微妙subtleな点があるのが面白さの一つだと思う