This is exactly what I'm talking about, "every vector space has a basis" is not a provable statement in constructive mathematics because that ranges over non-constructive objects, but it can prove constructive equivalents like "every finite-dimensional or countable vector space has a basis".
I'm just not persuaded that this is not sufficient for any realizable mathematical construction. In my view, some non-constructive objects are non-realizable and so must ultimately serve only as convenient shortcuts that are ultimately eliminated when the math manifests in a real construction, either physical or computational. So if such things are merely artifacts of a particular formalism, then it should be possible to dispense with them entirely with a constructive or intuitionistic formalism.
That's why I'm looking for something that truly, fundamentally impossible for constructive mathematics, but that we know to exist, be true, valid, etc. that would contradict this position.
