¿Cuál es el doble de la implicación?

Question

Usted puede dividir Intuitionistic Lógica Proposicional en los positivos y los negativos de los fragmentos. El fragmento negativo incluye la verdad, conjunción, implicación y mientras que el positivo fragmento incluye la falsedad y la disyunción. Es evidente que existe una dualidad entre (la verdad, la conjunción) y (falsedad, la disyunción), pero la implicación carece de un doble. Hay un doble a implicación?

Tomado como una categoría que puede hacer el (la verdad, la conjunción)/(la falsedad, la disyunción) la dualidad explícita como final (producto)/(inicial, subproducto) pero nunca he visto un doble a la exponencial objeto. Es allí una manera significativa a dualize la exponencial objeto?

Como medida de seguimiento no puede haber ninguna forma de dualize implicación/exponencial. Si ese es el caso, ¿por qué es la implicación de pensamiento para estar contenidos en el fragmento negativo de IPL?

Answer 1

Primer vistazo a cómo obtener la exponencial. En una categoría de productos, el exponencial functor $B \Rightarrow (-)$ puede ser definido como derecho-medico adjunto del functor $(-) \times B$. Así que en este caso, $b \Rightarrow (-)$ es derecho-adjoint a $(-) \wedge b$, es decir, satisface la regla $$a \wedge b \vdash c \quad \text{if and only if} \quad a \vdash b \Rightarrow c$$ En el caso de la lógica clásica, por lo tanto, podemos definir a $b \Rightarrow c = (\neg b) \vee c$, aunque en la lógica constructiva $\Rightarrow$ necesita ser tomada como primitivo. Pero esto está bien: la verdad de los valores en IPL vivir en un álgebra de Heyting, y todas las álgebras de Heyting han exponenciales!

Doblemente, consigue un coexponential objeto, para que no conozco la notación así que voy a escribir $A \Rightarrow^{\text{op}} (-)$, el cual puede ser definido en una categoría con co-productos como de izquierda medico adjunto del functor $(-)+A$. Así que en este caso, $a \Rightarrow^{\text{op}} (-)$ es de izquierda adjunto a $(-) \vee a$, es decir, satisface la regla $$a \Rightarrow^{\text{op}} b \vdash c \quad \text{if and only if} \quad b \vdash c \vee a$$ En el caso de la lógica clásica, por lo tanto, podemos definir a $a \Rightarrow^{\text{op}} b = (\neg a) \wedge b$.

Sin embargo, un álgebra de Heyting no puede, en general, se espera que tenga coexponentials, que es la razón por la implicación parece no tener doble en la lógica constructiva (porque no!)