Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
    
$\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
add comment

1 Answer

up vote 4 down vote accepted

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.

share|improve this answer
    
+1 in particular for linear logic. –  Henning Makholm Dec 22 '12 at 18:23
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.