Connection between dual space V* and negation P^c

Question

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?

Answer 1

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.

A good general introduction to these ideas can be found in Baez's Physics, Topology, Logic, and Computation: A Rosetta Stone.