3 ms·

Constructivism is not mainstream mathematics. The theorem that every vector space has a basis, something that is used fairly often, is actually equivalent to t

Constructivism is not mainstream mathematics. The theorem that every vector space has a basis, something that is used fairly often, is actually equivalent to the axiom of choice, something that isn't valid in constructive logic. For many vector spaces you won't be able to write down a basis. And there are other examples, e.g. almost none of the automorphisms of C can be written down (only the identity and the conjugate map).

naasking 2y ago
I'm aware that constructivism is not mainstream. What you've described are that such constructions are not available at this time (not comparable ones), but is there any evidence that comparable constructions are not possible even in principle?
- Tainnor 2y ago
  Yes because the existence of a basis for arbitrary vector spaces is equivalent to the axiom of choice.
  - naasking 2y ago
    A derivation of the axiom of choice in Martin-Löf Type Theory, which is constructive: https://plato.stanford.edu/entries/axiom-choice/choice-and-type-theory.html https://plato.stanford.edu/entries/axiom-choice/choice-and-t... 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.

naasking 2y ago

I'm aware that constructivism is not mainstream. What you've described are that such constructions are not available at this time (not comparable ones), but is there any evidence that comparable constructions are not possible even in principle?

Tainnor 2y ago
Yes because the existence of a basis for arbitrary vector spaces is equivalent to the axiom of choice.
- naasking 2y ago
  A derivation of the axiom of choice in Martin-Löf Type Theory, which is constructive: https://plato.stanford.edu/entries/axiom-choice/choice-and-type-theory.html https://plato.stanford.edu/entries/axiom-choice/choice-and-t... 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.