Some time ago, I've heard that there was a relationship between intuitionistic logic and infinite dimensional vector spaces.
More precisely, the fact that $\neg \neg \phi \to \phi$ may not be "true" in intuitionistic logic could be related to the fact that an infinite dimensional vector space $V$ is not isomorphic to its bidual (see Erdős-Kaplansky theorem), whereas the fact that $\phi \to \neg \neg \phi$ is "true" in intuitionistic logic could be similar to the fact that any vector space $V$ embeds in its bidual.
Does anyone have already heard about this, or could develop this idea (i.e. is it possible to make it more precise)? Is there any reference about it?
Thank you in advance!