# Tagged Questions

0answers
38 views

### Existence of a basis in constructive vector spaces

As I was trying to review forgotten knowledge on Vector Spaces in wikipedia, I read that the existence of a basis follows from Zorn lemma, hence equivalently from the axiom of choice. Actually, the ...
1answer
105 views

### Decidable & Recursive predicates

Let $C$ be a decidable predicate in the language of arithmetic HA, that is $$\vdash (\forall \underline x)\: C(x) \vee \neg C(x).$$ $C$ is recursive if there exists a computable characteristic ...
1answer
217 views

### How to compute isomorphism $V \simeq V^{**}$ (in Haskell)?

Since there is a canonical isomorphism between vector space $V$ and his dual dual space $V^{**}$, $\dim V \in \mathbb N \;$, I want to write it as a Haskell function. This function is going to have a ...
0answers
109 views

4answers
361 views

### Are the computable reals finitary?

In the comment thread of an answer, I said: The computable numbers are based on the intuitionistic continuum, and are not finitary. To which T.. replied: Computable numbers are not based on ...