4
$\begingroup$

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?

  • 0
    Ah, I suppose I'm thinking more in terms of universal properties than dualisation. Interesting.2012-12-22

1 Answers 1

5

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.