undefined | Better HN

0 pointsnaasking1y ago0 comments

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?

0 comments

2 comments · 1 top-level

Tainnor1y ago· 1 in thread

Yes because the existence of a basis for arbitrary vector spaces is equivalent to the axiom of choice.

naaskingOP1y 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-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.

j / k navigate · click thread line to collapse