La conexión entre el espacio dual de V* y la negación de P^c

Question

Observa la siguiente similitud entre el espacio vectorial dual y la negación en lógica proposicional:

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

Hay una noción general de la dualidad detrás de esto?

También, un tensor es conocido por ser de tipo $V \times \cdots \times V \times V^* \times \cdots \times V^* \rightarrow F$ o tal vez más sugestivamente $V \rightarrow \cdots \rightarrow V \rightarrow V^* \rightarrow \cdots \rightarrow V^* \rightarrow F$.

Hace esto para dar un equivalente de la noción de "tensor" en lógica proposicional? Quizás a través de Curry-Howard?

Answer 1

La construcción de describir puede llevarse a cabo en cualquier cerrada categoría monoidal. Los únicos relevantes para la lógica proposicional son aquellos donde la $\otimes$ denota "y" e $\Rightarrow$ denota "implica." Véase también compacto cerrado categoría, álgebra de Heyting, y la lógica lineal.

Una buena introducción general a estas ideas se pueden encontrar en Báez de la Física, la Topología, la Lógica y el Cálculo: Una Piedra de Rosetta.