Thanks for the tips, mathphysicist. The first sentence of that Springer Encyclopedia reference gives the same definition as wikipedia (so maybe that definition is perfectly adequate after all), but then a little later it says, "The most interesting case is that in which is $\Phi$ [my $S$] is a nuclear space." Then they cite a spectral theorem, but I can't tell if they mean to include the nuclear hypothesis in the theorem or not.

By syntactic implication you mean formal proofs? Proofs (or more carefully, Lambek-equivalence classes of proofs) can be viewed as morphisms in free structures such as the free bicartesian closed category on a set of variables you mentioned (and of course this will be much richer than just the free Heyting algebra on the set of variables). Is that the kind of thing you mean? In that case one can talk about completeness theorems by associating them with embedding theorems a la Freyd.

Cool! The business about $S^\infty$ I gave above was my own response to a problem Paul Halmos mentions in his autobiography: does there exist a nontrivial connected Hausdorff topological group of exponent 2? (This problem is one of fifteen on a take-home final he once gave.) Ever since I found this solution, I've enjoyed trotting it out on odd occasions, and I'm happy that MO provided me with an opportunity to do so again!

I agree: I don't see any real question here that Pete hasn't already addressed.

identification of a point with its antipode = negation is the same as identifying a point $x$ with $1+x$ in the topological Boolean ring, which is the same as modding out by the subspace $\{0, 1\}$. This is one way of making precise an argument behind one of the claims in my answer.

Whuh, you don't believe me? :-) The answer anyhow is yes; it's another way of describing the standard Milgram construction of the classifying bundle, viz., the realization of the nerve applied to the groupoid map $K\mathbb{Z}_2 \to B\mathbb{Z}_2$ (that '$B$' being our nLab notation for the 1-object category attached to the group), and that's homeomorphic to the projection $S^\infty \to \mathbb{RP}^\infty$. Incidentally, the same Lawvere theory line of argument I'm using here shows that $S^\infty$ is a topological Boolean algebra for which negation is the antipodal map, and the (cont.)

Well, if you like, but the way I said it is fine. The '1' is traditional notation for the group identity. It becomes the 0 element of a vector space structure if we assume the axiom $x^2 = 1$.

The 3 x 3 lemma proper involves nine objects $X_{ij}$, where $i, j = 1, 2, 3$, and rows and columns which are coequalizer forks, commuting in parallel, where for each parallel pair the two morphisms have a common right inverse. If this formulation isn't at the Lab, it should be. It applies to the case $X_{ij} = X_i \times X_{j}'$ if we have that separate preservation, which holds in case of cartesian closure (or regularity if these are coequalizers of kernel pairs). If you are in Top then it holds for certain quotients as described by Day-Kelly; were you able to access any of that?

@David: well, then your wish is granted! If you have separate preservation of reflective coequalizers, then you have joint preservation by this result. (I had a sneaking suspicion that your intended applications were topological or smooth, so that the regularity hypothesis wouldn't be all that apt for your purposes, but that hypothesis did address some of the other queries I believe.)

Wait, I thought David was asking for the joint preservation of quotients. And I was trying to establish that: first, in a regular category, $X \times -$ does preserve quotient maps = regular epis (since the pullback of a regular epi $Y \to Z$ along the projection $X \times Z \to Z$ is a regular epi), and second, since regular epis are reflexive coequalizers, the 3 x 3 lemma in Johnstone's book guarantees that the fork down the diagonal is also a coequalizer; the corollary is the joint preservation. Have I made a stupid mistake?

I was. If OP meant to consider infinite-dimensional $V$ as well (and it seems there's no indication he doesn't), then I'd have to rethink the problem. The Morita business I had in mind does assume finite-dimensionality.

I agree with Andrew. Giving good references are among the best types of answers, even if they mean you have to do some work yourself. The book by Adams is in any case fantastic and is well worth reading.