Правда, я думаю, что проверить, можно ли какой-то текст переписать в формализованном виде, это очень трудоемко.
Не всё так плохо. Аксиоматика распространённых теорий множеств (ZFC, NBG) специально выбрана так, чтобы обычно применяемые математические рассуждения были формализуемы. В частности, аксиома выбора включена как раз по этой причине: математики часто применяют рассуждения, для формализации которых нужна аксиома выбора. Для людей проблема с формализацией в том, что формализованные доказательства сколько-нибудь нетривиальных утверждений совершенно необозримы и трудно воспринимаемы. Хотя с последним, наверное, можно натренироваться. Но читать десятки и сотни страниц тривиальных рассуждений в доказательстве несложного утверждения… Вот полюбуйтесь:
http://us.metamath.org/mpeuni/mmset.html#trivia (обсуждается доказательство того, что в поле комплексных чисел
).
В действительности причиной неконструктивности является вовсе не аксиома выбора, которая всего лишь утверждает непустоту некоторого множества (а именно, множества функций выбора для каждого семейства непустых множеств). Источником неконструктивности в данном случае является также широко применяемое рассуждение "поскольку множество непусто, в нём содержится некоторый элемент
; возьмём этот элемент
и сделаем с ним то, что нам нужно". При этом никакого конкретного элемента
не указывается, есть только его обозначение. Это рассуждение чаще используется само по себе, без всякой аксиомы выбора. Кроме этого рассуждения, в классической математике есть и другие неконструктивные рассуждения, например, доказательства от противного; или доказывается формула вида
, но не указывается, что именно доказано:
или
.
Кстати, в конструктивной математике аксиома выбора вполне может быть истинной (с каким-то ограничением на определение семейства множеств, к которому она применяется; я в детали не вникал, потому что это далеко от того, чем я интересовался). Резон такой: если у нас есть конструктивно определённое семейство конструктивных множеств, которые все являются конструктивно непустыми (последнее означает, что в каждом из этих множеств мы можем конструктивно указать некоторый элемент), то почему бы нам не построить конструктивную функцию выбора? На надо сказать, что существует много вариантов конструктивизма, в которых эта конструктивность понимается по-разному.
Что касается "парадокса" Банаха–Тарского, то, наверное, достаточно понимать, что абстрактный шар, существующий исключительно в нашем воображении, и реальный апельсин — немного разные вещи, и что по крайней мере в некоторых случаях абстрактный шар может оказаться плохой моделью реального апельсина.