# Connection between dual space V* and negation P^c

Notice the following similarity between the vector space dual and negation in propositional logic:

$$V^* \equiv V \rightarrow F$$ $$P^c \equiv P \rightarrow \bot$$

Is there some general notion of duality behind this?

Also, a tensor is known to be of type $V \times \cdots \times V \times V^* \times \cdots \times V^* \rightarrow F$ or perhaps more suggestively $V \rightarrow \cdots \rightarrow V \rightarrow V^* \rightarrow \cdots \rightarrow V^* \rightarrow F$.

Does this give an equivalent notion of a "tensor" in propositional logic? Perhaps through Curry-Howard?

-
$\bot$ corresponds more to $0$ than $F$, I think. –  Zhen Lin Dec 22 '12 at 9:06
@Zhen: yes, I noticed this after writing my answer, but dualizing objects are as dualizing objects do... for example, for locally compact abelian groups the dualizing object is $S^1$. –  Qiaochu Yuan Dec 22 '12 at 9:45
Ah, I suppose I'm thinking more in terms of universal properties than dualisation. Interesting. –  Zhen Lin Dec 22 '12 at 9:50

The construction you describe can be carried out in any closed monoidal category. The ones relevant to propositional logic are the ones where $\otimes$ denotes "and" and $\Rightarrow$ denotes "implies." See also compact closed category, Heyting algebra, and linear logic.