Many of the “pathologies” when rejecting choice have similar computational problems as choice does, so bringing them up doesn’t really disrupt this argument.
Example: Let P be some proposition. Theorem: If every vector space has a basis, then P∨¬P. Proof: Define a vector space V=Q/∼ where x∼y⟺(P∨x=y). Let B be a basis over V. Express 1=∑ni=1bici in this basis. If n≥1, we have a basis element bi≁0, and thus ¬P. Otherwise, we know 1∼0 and thus P.
Example: Let P be some proposition. Theorem: If every vector space has a basis, then P∨¬P. Proof: Define a vector space V=Q/∼ where x∼y⟺(P∨x=y). Let B be a basis over V. Express 1=∑ni=1bici in this basis. If n≥1, we have a basis element bi≁0, and thus ¬P. Otherwise, we know 1∼0 and thus P.
Ah yeah, this is a Hamel basis version of Diaconescu’s theorem (a very cool theorem)! Lovely proof!