人間や計算機が実際に扱うような理論は、有限個の記号しか扱わないから
論理式を整列できるし、選択公理も別に要らない。
だから認識論的なことを話題にする限りは別に問題にはならなくて、
選択公理が問題になるのは、そもそも理論で使う基本的な記号の集まり自体が
基数を持たない、みたいな場合なので、別に問題ないんじゃないかと。