En la página de Wikipedia sobre lógica intuicionista Se afirma que el medio excluido y la eliminación de la doble negación no son axiomas. ¿Significa esto que las leyes de De Morgan, enunciadas $$ \lnot (p \land q) \iff \lnot p \lor \lnot q \\ \lnot (p \lor q) \iff \lnot p \land \lnot q,$$ no se puede demostrar en la lógica intuicionista proposicional?
Respuestas
¿Demasiados anuncios?La respuesta es "tres cuartos sí, un cuarto no".
El que es válido es el que tiene la disyunción dentro de la negación: $$\lnot p \land \lnot q \dashv \vdash \lnot (p \lor q)$$ Para la otra ley, sólo es válida una implicación: $$\lnot p \lor \lnot q \vdash \lnot (p \land q)$$
Las pruebas se dejan como ejercicio para el lector.
Para demostrar que la última implicación no es válida, necesitamos conocer alguna teoría de modelos para la lógica proposicional intuicionista. Recordemos que las reglas de inferencia de la lógica proposicional intuicionista son sólidas cuando se interpretan en un álgebra de Heyting: es decir, si $p \vdash q$ en la lógica intuicionista, y $[p]$ y $[q]$ son las interpretaciones correspondientes en alguna álgebra de Heyting $\mathfrak{A}$ entonces $[p] \le [q]$ .
Ahora bien, existe una rica y fructífera fuente de álgebras de Heyting en matemáticas: el marco de conjuntos abiertos de cualquier espacio topológico es automáticamente un álgebra de Heyting, con la implicación de Heyting definida por $$(U \Rightarrow V) = \bigcup_{W \cap U \le V} W$$ Por lo tanto, la negación de $U$ es el interior del complemento de $U$ . Ahora, considere $X = (0, 2)$ y que $U = (0, 1)$ y $V = (1, 2)$ . Entonces, $\lnot U = (1, 2)$ y $\lnot V = (0, 1)$ Así que $\lnot U \cup \lnot V = X \setminus \{ 1 \}$ . Por otro lado, $U \cap V = \emptyset$ Así que $\lnot (U \cap V) = X$ . Así, $\lnot U \cup \lnot V \le \lnot (U \cap V)$ como se esperaba, pero $\lnot (U \cap V) \nleq \lnot U \cup \lnot V$ . Concluimos que $$\lnot (p \land q) \nvdash \lnot p \lor \lnot q$$
Parece que he conseguido demostrar tres implicaciones utilizando el isomorfismo de Curry-Howard, pero la cuarta parece ser falsa.
$\neg(p \lor q) \Rightarrow \neg p \land \neg q$ : $$ f = \lambda g.\ \langle \lambda x.\ g\ (\mathtt{Left}\ x), \lambda y.\ g\ (\mathtt{Right}\ y) \rangle $$ $\neg(p \lor q) \Leftarrow \neg p \land \neg q$ :
\begin{align*} f &= \lambda (g, h).\ \lambda (\mathtt{Left}\ x).\ g\ x \\\ f &= \lambda (g, h).\ \lambda (\mathtt{Right}\ x).\ h\ x \end{align*}
$\neg(p \land q) \Leftarrow \neg p \lor \neg q$ :
\begin{align*} f &= \lambda (\mathtt{Left}\ g).\ \lambda (x, y).\ g\ x \\\ f &= \lambda (\mathtt{Right}\ h).\ \lambda (x, y).\ h\ y \end{align*}
Para demostrar $$\neg(p \land q) \Rightarrow \neg p \lor \neg q$$ Necesitaría transformar una función $p \times q \to \alpha$ a uno de los $p \to \alpha$ ou $q \to \alpha$ pero es imposible obtener dos de ellos (ambos $p$ y $q$ ) a la vez. Esta es la intuición, pero necesitaría algo más para la prueba.
Editar 1: Enlace relevante: http://ncatlab.org/nlab/show/de+Morgan+dualidad .
Editar 2: Aquí hay un intento de prueba (pero no estoy seguro de que sea correcta, si alguien puede decirlo, por favor, hágalo):
Supongamos que existe una función $$F : \forall \alpha, p, q.\ (p \times q \to \alpha) \to (p \to \alpha) + (q \to \alpha).$$ Entonces, por la naturalidad de $F$ tenemos que siempre devuelve $\mathtt{Left}$ o siempre devuelve $\mathtt{Right}$ . Sin pérdida de generalidad, supongamos que $F(f) = \mathtt{Left}\ g$ para cualquier $f$ . Entonces se deduce que existe $$ F_1 : \forall \alpha, p, q.\ (p \times q \to \alpha) \to (p \to \alpha). $$ Sin embargo, $F_1(\lambda x.\ \lambda y.\ y) : \forall \alpha, \beta.\ \beta \to \alpha$ qué significa $\forall \beta.\ \beta \to \bot$ y así concluye la prueba.
Aquí hay un ejemplo finito que básicamente reproduce lo que ocurre en la respuesta/contraejemplo de Zhen Lin:
Tomemos un entramado booleano de 4 elementos (etiquetado arriba como 1-2-3-4) y una "supercapa" del mismo (etiquetado como 5, arriba). Los elementos de la anticadena de esta red (2 y 3) siguen siendo pseudocomplementos entre sí, aunque ya no son complementos, lo que va unido a que la red "enriquecida" ya no es booleana. (Se puede comprobar que, por ejemplo $2\land x \le1$ [tiene la mayor solución 3). También es fácil ver que este entramado sigue siendo distributivo (porque tiene exactamente 5 elementos que es un Comprobación fácil ), por lo que una red de Heyting porque es finita y distributiva.
Ahora, el encuentro de los dos elementos de la anticadena sigue siendo el elemento inferior, pero como hemos añadido el nuevo "supertop" 5, el psedocomplemento del inferior (etiquetado como 1) va a ser 5 en esta red enriquecida (porque $1 \land x \le 1$ admite ahora una solución mayor (5) que 4, que era el tope de la red booleana con la que empezamos, por lo que $\neg (2 \land 3) = 5$ ahora, mientras que el "supertop" no hace nada por la unión de los preudocomplentes de los elementos de la anticadena, es decir $\neg 2 \lor \neg 3= 3 \lor 2 = 4$ .
Esto es para no es una prueba, pero tenga en cuenta que este supertop no afecta a la otra ley de Mogran: $\neg (2 \lor 3) = \neg 4 = 1$ y $\neg 2 \land \neg 3 = 3 \land 2 = 1$ .
(Disculpas por utilizar el 1 como elemento inferior, ahora esto puede ser ligeramente confuso).
La parte siguiente (también) no es una prueba de nada, pero da una intuición adicional de por qué sólo una de las leyes de De Mogran se rompe en un álgebra de Heyting... y por qué he añadido un supertop arriba, en lugar de un superbottom, etiquetado como 0 abajo:
Entonces, "no pasa nada" en lo que respecta a las leyes de De Morgan porque la definición de un pseudocomplemento es relativa al (nuevo) (super)fondo. Así que $\neg (2 \land 3) = \neg 1 = 0$ pero $\neg 2 \lor \neg 3 = 0 \lor 0 = 0$ ahora también porque al añadir este superfondo (0) en realidad cambiaron los pseudocomplementos de 2 y 3 (así como el de 1).
Del mismo modo, este entramado de superfondos no rompe la otra ley de De Morgan: $\neg (2 \lor 3) = \neg 4 = 0$ y $\neg 2 \land \neg 3 = 0 \land 0 = 0$ .