Я могу рассказать, в чём формальная разница "степеней неконструктивности".
Боюсь, Вы не совсем меня поняли. Вы мне говорите, что в некоторых случаях мы можем каким-то способом выделить конкретный элемент, если это нам зачем-то нужно. Пусть даже и не конструктивно. Я не об этом. Да и почему Вы думаете, что этот способ не может работать в случае аксиомы выбора? Аксиома выбора сообщает нам, что функции выбора существуют, и мы конструируем формулу, которой удовлетворяет единственная функция выбора. И, кстати, это не отменит обвинений в неконструктивности.
В одном случае у нас есть множество функций выбора, про которое аксиома выбора говорит, что оно не пусто. Пользуясь этим мы говорим "пусть

— некоторая функция выбора".
В другом случае у нас есть некоторое множество

, про которое мы знаем, что оно непустое, но не знаем ни одного конкретного его элемента, или нам всё равно, что это за элемент, и мы говорим "пусть

— какой-нибудь элемент".
По-моему, никакой разницы нет.