For fun, I've been looking at the interpretation of linear logic in terms of finite-dimensional vector spaces, and ran into an interesting question about the interpretation of double-negation-elimination in this category.
As is well-known, vector spaces have a natural notion of dual space -- given a vector space $V$,(over a field $R$) the dual space $V^\ast$ is just the set of linear functions into $V \multimap R$. Furthemore, it is well-known (indeed, so well-known that I don't know who proved it) that every finite-dimensional vector space is isomorphic to its double-dual.
One direction of the isomorphism $V \to V^{\ast\ast}$ is easy (it's just the map $f : V \to V^{\ast\ast} \triangleq v \mapsto \lambda k.\;k(v)$). The other direction is trickier. The usual proof goes something like this:
- The dimension of a dual space $V^\ast$ is the same as the original space $V$.
- So the double-dual $V^{\ast\ast}$ has the same dimension as the original space $V$.
- So if we can show that $f$ has a zero kernel, then we know that $f$ has a range of all of $V^{\ast\ast}$, and so is (one half of) an isomorphism.
But the only way I know of actually computing the inverse $f^{-1}$ requires choosing a basis and then inverting the matrix.
What I'd really like is an algebraic or categorial account of Gauss-Jordan matrix inversion (or Gaussian elimination or LU decomposition or whatever), so that I can give a syntactic theory of inversion (and hence an operational semantics for double-negation elimination in FD vector spaces).
This seems like the sort of thing that must have been studied before, but my Google skills are apparently not up to the task....